Theorem kmlem13 4701

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

Hypothesis

Ref	Expression
kmlem9.1	|- A = {u | E.t e. x u = (t \ U.(x \ {t}))}

Assertion

Ref	Expression
kmlem13	|- (A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)) <-> A.x(-. E.z e. x A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y))))

Distinct variable groups:   x,y,z,w,v,u,t   y,A,z,w,v

Proof of Theorem kmlem13

Step	Hyp	Ref	Expression
1		kmlem1 4689	. . 3 |- (A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)) -> A.x(A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/)) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y))))
2		raleq1 1762	. . . . . . 7 |- (x = h -> (A.w e. x (z =/= w -> (z i^i w) = (/)) <-> A.w e. h (z =/= w -> (z i^i w) = (/))))
3	2	raleqd 1767	. . . . . 6 |- (x = h -> (A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/)) <-> A.z e. h A.w e. h (z =/= w -> (z i^i w) = (/))))
4		raleq1 1762	. . . . . . 7 |- (x = h -> (A.z e. x (z =/= (/) -> E!v v e. (z i^i y)) <-> A.z e. h (z =/= (/) -> E!v v e. (z i^i y))))
5	4	exbidv 1261	. . . . . 6 |- (x = h -> (E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y)) <-> E.yA.z e. h (z =/= (/) -> E!v v e. (z i^i y))))
6	3, 5	imbi12d 624	. . . . 5 |- (x = h -> ((A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/)) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y))) <-> (A.z e. h A.w e. h (z =/= w -> (z i^i w) = (/)) -> E.yA.z e. h (z =/= (/) -> E!v v e. (z i^i y)))))
7	6	cbvalv 1296	. . . 4 |- (A.x(A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/)) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y))) <-> A.h(A.z e. h A.w e. h (z =/= w -> (z i^i w) = (/)) -> E.yA.z e. h (z =/= (/) -> E!v v e. (z i^i y))))
8		kmlem9.1	. . . . . . 7 |- A = {u | E.t e. x u = (t \ U.(x \ {t}))}
9	8	kmlem10 4698	. . . . . 6 |- (A.h(A.z e. h A.w e. h (z =/= w -> (z i^i w) = (/)) -> E.yA.z e. h (z =/= (/) -> E!v v e. (z i^i y))) -> E.yA.z e. A (z =/= (/) -> E!v v e. (z i^i y)))
10		ineq2 2182	. . . . . . . . . . . 12 |- (y = g -> (z i^i y) = (z i^i g))
11	10	eleq2d 1517	. . . . . . . . . . 11 |- (y = g -> (v e. (z i^i y) <-> v e. (z i^i g)))
12	11	eubidv 1363	. . . . . . . . . 10 |- (y = g -> (E!v v e. (z i^i y) <-> E!v v e. (z i^i g)))
13	12	imbi2d 610	. . . . . . . . 9 |- (y = g -> ((z =/= (/) -> E!v v e. (z i^i y)) <-> (z =/= (/) -> E!v v e. (z i^i g))))
14	13	ralbidv 1639	. . . . . . . 8 |- (y = g -> (A.z e. A (z =/= (/) -> E!v v e. (z i^i y)) <-> A.z e. A (z =/= (/) -> E!v v e. (z i^i g))))
15	14	cbvexv 1297	. . . . . . 7 |- (E.yA.z e. A (z =/= (/) -> E!v v e. (z i^i y)) <-> E.gA.z e. A (z =/= (/) -> E!v v e. (z i^i g)))
16	8	kmlem12 4700	. . . . . . . . . . 11 |- (A.z e. x (z \ U.(x \ {z})) =/= (/) -> (A.z e. A (z =/= (/) -> E!v v e. (z i^i g)) -> A.z e. x (z =/= (/) -> E!v v e. (z i^i (g i^i U.A)))))
17		visset 1788	. . . . . . . . . . . . 13 |- g e. V
18	17	inex1 2684	. . . . . . . . . . . 12 |- (g i^i U.A) e. V
19		ineq2 2182	. . . . . . . . . . . . . . . 16 |- (y = (g i^i U.A) -> (z i^i y) = (z i^i (g i^i U.A)))
20	19	eleq2d 1517	. . . . . . . . . . . . . . 15 |- (y = (g i^i U.A) -> (v e. (z i^i y) <-> v e. (z i^i (g i^i U.A))))
21	20	eubidv 1363	. . . . . . . . . . . . . 14 |- (y = (g i^i U.A) -> (E!v v e. (z i^i y) <-> E!v v e. (z i^i (g i^i U.A))))
22	21	imbi2d 610	. . . . . . . . . . . . 13 |- (y = (g i^i U.A) -> ((z =/= (/) -> E!v v e. (z i^i y)) <-> (z =/= (/) -> E!v v e. (z i^i (g i^i U.A)))))
23	22	ralbidv 1639	. . . . . . . . . . . 12 |- (y = (g i^i U.A) -> (A.z e. x (z =/= (/) -> E!v v e. (z i^i y)) <-> A.z e. x (z =/= (/) -> E!v v e. (z i^i (g i^i U.A)))))
24	18, 23	cla4ev 1842	. . . . . . . . . . 11 |- (A.z e. x (z =/= (/) -> E!v v e. (z i^i (g i^i U.A))) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y)))
25	16, 24	syl6 22	. . . . . . . . . 10 |- (A.z e. x (z \ U.(x \ {z})) =/= (/) -> (A.z e. A (z =/= (/) -> E!v v e. (z i^i g)) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y))))
26	25	19.23adv 1198	. . . . . . . . 9 |- (A.z e. x (z \ U.(x \ {z})) =/= (/) -> (E.gA.z e. A (z =/= (/) -> E!v v e. (z i^i g)) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y))))
27	26	com12 11	. . . . . . . 8 |- (E.gA.z e. A (z =/= (/) -> E!v v e. (z i^i g)) -> (A.z e. x (z \ U.(x \ {z})) =/= (/) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y))))
28		kmlem3 4691	. . . . . . . . . . 11 |- ((z \ U.(x \ {z})) =/= (/) <-> E.v e. z A.w e. x (z =/= w -> -. v e. (z i^i w)))
29		ralinexa 1659	. . . . . . . . . . . 12 |- (A.w e. x (z =/= w -> -. v e. (z i^i w)) <-> -. E.w e. x (z =/= w /\ v e. (z i^i w)))
30	29	rexbii 1644	. . . . . . . . . . 11 |- (E.v e. z A.w e. x (z =/= w -> -. v e. (z i^i w)) <-> E.v e. z -. E.w e. x (z =/= w /\ v e. (z i^i w)))
31		rexnal 1630	. . . . . . . . . . 11 |- (E.v e. z -. E.w e. x (z =/= w /\ v e. (z i^i w)) <-> -. A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)))
32	28, 30, 31	3bitr 177	. . . . . . . . . 10 |- ((z \ U.(x \ {z})) =/= (/) <-> -. A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)))
33	32	ralbii 1643	. . . . . . . . 9 |- (A.z e. x (z \ U.(x \ {z})) =/= (/) <-> A.z e. x -. A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)))
34		ralnex 1629	. . . . . . . . 9 |- (A.z e. x -. A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)) <-> -. E.z e. x A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)))
35	33, 34	bitr 173	. . . . . . . 8 |- (A.z e. x (z \ U.(x \ {z})) =/= (/) <-> -. E.z e. x A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)))
36	27, 35	syl5ibr 207	. . . . . . 7 |- (E.gA.z e. A (z =/= (/) -> E!v v e. (z i^i g)) -> (-. E.z e. x A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y))))
37	15, 36	sylbi 199	. . . . . 6 |- (E.yA.z e. A (z =/= (/) -> E!v v e. (z i^i y)) -> (-. E.z e. x A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)) -> E.yA.z e. x (z =/= (/) -> E!v v e. (z i^i y))))
38	9, 37	syl 10	. . . . 5 |- (A.h(A.z e. h A.w e. h (z =/= w -> (z i^i w) = (/)) -> E.yA.z e. h (z =/= (/) -> E!v v e. (z i^i y))) -> (-. E.z e. x A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)) -> E.yA.z e. x (z =/= (/)