Theorem kmlem15 4789

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4.

Hypotheses

Ref	Expression
kmlem14.1	|- (ph <-> (z e. y -> ((v e. x /\ y =/= v) /\ z e. v)))
kmlem14.2	|- (ps <-> (z e. x -> ((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
kmlem14.3	|- (ch <-> A.z e. x E!v v e. (z i^i y))

Assertion

Ref	Expression
kmlem15	|- ((-. y e. x /\ ch) <-> A.zE.vA.u(-. y e. x /\ ps))

Distinct variable groups:   x,y,z,v,u   ph,u

Proof of Theorem kmlem15

Step	Hyp	Ref	Expression
1		kmlem14.3	. . . 4 |- (ch <-> A.z e. x E!v v e. (z i^i y))
2		ax-17 973	. . . . . . 7 |- (v e. (z i^i y) -> A.u v e. (z i^i y))
3	2	eu1 1394	. . . . . 6 |- (E!v v e. (z i^i y) <-> E.v(v e. (z i^i y) /\ A.u([u / v]v e. (z i^i y) -> v = u)))
4		elin 2210	. . . . . . . . 9 |- (v e. (z i^i y) <-> (v e. z /\ v e. y))
5		ax-17 973	. . . . . . . . . . . . 13 |- (u e. (z i^i y) -> A.v u e. (z i^i y))
6		eleq1 1537	. . . . . . . . . . . . 13 |- (v = u -> (v e. (z i^i y) <-> u e. (z i^i y)))
7	5, 6	sbie 1198	. . . . . . . . . . . 12 |- ([u / v]v e. (z i^i y) <-> u e. (z i^i y))
8		elin 2210	. . . . . . . . . . . 12 |- (u e. (z i^i y) <-> (u e. z /\ u e. y))
9	7, 8	bitr 173	. . . . . . . . . . 11 |- ([u / v]v e. (z i^i y) <-> (u e. z /\ u e. y))
10		eqcom 1480	. . . . . . . . . . 11 |- (v = u <-> u = v)
11	9, 10	imbi12i 188	. . . . . . . . . 10 |- (([u / v]v e. (z i^i y) -> v = u) <-> ((u e. z /\ u e. y) -> u = v))
12	11	albii 1001	. . . . . . . . 9 |- (A.u([u / v]v e. (z i^i y) -> v = u) <-> A.u((u e. z /\ u e. y) -> u = v))
13	4, 12	anbi12i 484	. . . . . . . 8 |- ((v e. (z i^i y) /\ A.u([u / v]v e. (z i^i y) -> v = u)) <-> ((v e. z /\ v e. y) /\ A.u((u e. z /\ u e. y) -> u = v)))
14		19.28v 1301	. . . . . . . 8 |- (A.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)) <-> ((v e. z /\ v e. y) /\ A.u((u e. z /\ u e. y) -> u = v)))
15	13, 14	bitr4 176	. . . . . . 7 |- ((v e. (z i^i y) /\ A.u([u / v]v e. (z i^i y) -> v = u)) <-> A.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)))
16	15	exbii 1053	. . . . . 6 |- (E.v(v e. (z i^i y) /\ A.u([u / v]v e. (z i^i y) -> v = u)) <-> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)))
17	3, 16	bitr 173	. . . . 5 |- (E!v v e. (z i^i y) <-> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)))
18	17	ralbii 1670	. . . 4 |- (A.z e. x E!v v e. (z i^i y) <-> A.z e. x E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)))
19		df-ral 1652	. . . . 5 |- (A.z e. x E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)) <-> A.z(z e. x -> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
20		kmlem14.2	. . . . . . . . . 10 |- (ps <-> (z e. x -> ((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
21	20	albii 1001	. . . . . . . . 9 |- (A.ups <-> A.u(z e. x -> ((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
22		19.21v 1287	. . . . . . . . 9 |- (A.u(z e. x -> ((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))) <-> (z e. x -> A.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
23	21, 22	bitr 173	. . . . . . . 8 |- (A.ups <-> (z e. x -> A.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
24	23	exbii 1053	. . . . . . 7 |- (E.vA.ups <-> E.v(z e. x -> A.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
25		19.37v 1305	. . . . . . 7 |- (E.v(z e. x -> A.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))) <-> (z e. x -> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
26	24, 25	bitr 173	. . . . . 6 |- (E.vA.ups <-> (z e. x -> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
27	26	albii 1001	. . . . 5 |- (A.zE.vA.ups <-> A.z(z e. x -> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
28	19, 27	bitr4 176	. . . 4 |- (A.z e. x E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)) <-> A.zE.vA.ups)
29	1, 18, 28	3bitr 177	. . 3 |- (ch <-> A.zE.vA.ups)
30	29	anbi2i 482	. 2 |- ((-. y e. x /\ ch) <-> (-. y e. x /\ A.zE.vA.ups))
31		19.28v 1301	. 2 |- (A.z(-. y e. x /\ E.vA.ups) <-> (-. y e. x /\ A.zE.vA.ups))
32		19.28v 1301	. . . . 5 |- (A.u(-. y e. x /\ ps) <-> (-. y e. x /\ A.ups))
33	32	exbii 1053	. . . 4 |- (E.vA.u(-. y e. x /\ ps) <-> E.v(-. y e. x /\ A.ups))
34		19.42v 1310	. . . 4 |- (E.v(-. y e. x /\ A.ups) <-> (-. y e. x /\ E.vA.ups))
35	33, 34	bitr2 174	. . 3 |- ((-. y e. x /\ E.vA.ups) <-> E.vA.u(-. y e. x /\ ps))
36	35	albii 1001	. 2 |- (A.z(-. y e. x /\ E.vA.ups) <-> A.zE.vA.u(-. y e. x /\ ps))
37	30, 31, 36	3bitr2 179	1 |- ((-. y e. x /\ ch) <-> A.zE.vA.u(-. y e. x /\ ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 956   = wceq 958   e. wcel 960  E.wex 982  [wsbc 1172  E!weu 1382   =/= wne 1588  A.wral 1648   i^i cin 2049

This theorem is referenced by:  kmlem16 4790

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815  df-in 2054

Copyright terms: Public domain