Theorem kmlem12 3591

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

Hypothesis

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

Assertion

Ref	Expression
kmlem12	|- (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 group(s):   x,y,z,w,v,u,t   y,A,z,w,v

Proof of Theorem kmlem12

Step	Hyp	Ref	Expression
1		kmlem1 3580	. . 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		pm4.2 148	. . . 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.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))))
3		raleq 1324	. . . . . . . 8 |- (x = h -> (A.w e. x (-. z = w -> (z i^i w) = (/)) <-> A.w e. h (-. z = w -> (z i^i w) = (/))))
4	3	raleqd 1327	. . . . . . 7 |- (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) = (/))))
5		raleq 1324	. . . . . . . 8 |- (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))))
6	5	biexdv 936	. . . . . . 7 |- (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))))
7	4, 6	imbi12d 474	. . . . . 6 |- (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)))))
8	7	cbvalv 972	. . . . 5 |- (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))))
9		kmlem8.1	. . . . . . . 8 |- A = {u | E.t e. x u = (t \ U.(x \ {t}))}
10	9	kmlem9 3588	. . . . . . 7 |- (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)))
11		ineq2 1639	. . . . . . . . . . . . 13 |- (y = g -> (z i^i y) = (z i^i g))
12	11	eleq2d 1156	. . . . . . . . . . . 12 |- (y = g -> (v e. (z i^i y) <-> v e. (z i^i g)))
13	12	bieudv 1013	. . . . . . . . . . 11 |- (y = g -> (E!v v e. (z i^i y) <-> E!v v e. (z i^i g)))
14	13	imbi2d 464	. . . . . . . . . 10 |- (y = g -> ((-. z = (/) -> E!v v e. (z i^i y)) <-> (-. z = (/) -> E!v v e. (z i^i g))))
15	14	biraldv 1219	. . . . . . . . 9 |- (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))))
16	15	cbvexv 973	. . . . . . . 8 |- (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)))
17	9	kmlem11 3590	. . . . . . . . . . . 12 |- (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)))))
18		visset 1350	. . . . . . . . . . . . . 14 |- g e. V
19	18	inex1 1697	. . . . . . . . . . . . 13 |- (g i^i U.A) e. V
20		ineq2 1639	. . . . . . . . . . . . . . . . 17 |- (y = (g i^i U.A) -> (z i^i y) = (z i^i (g i^i U.A)))
21	20	eleq2d 1156	. . . . . . . . . . . . . . . 16 |- (y = (g i^i U.A) -> (v e. (z i^i y) <-> v e. (z i^i (g i^i U.A))))
22	21	bieudv 1013	. . . . . . . . . . . . . . 15 |- (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))))
23	22	imbi2d 464	. . . . . . . . . . . . . 14 |- (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)))))
24	23	biraldv 1219	. . . . . . . . . . . . 13 |- (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)))))
25	19, 24	cla4ev 1401	. . . . . . . . . . . 12 |- (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)))
26	17, 25	syl6 23	. . . . . . . . . . 11 |- (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))))
27	26	19.23adv 954	. . . . . . . . . 10 |- (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))))
28	27	com12 13	. . . . . . . . 9 |- (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))))
29		kmlem3 3582	. . . . . . . . . . . 12 |- (-. (z \ U.(x \ {z})) = (/) <-> E.v e. z A.w e. x (-. z = w -> -. v e. (z i^i w)))
30		imnan 207	. . . . . . . . . . . . . . 15 |- ((-. z = w -> -. v e. (z i^i w)) <-> -. (-. z = w /\ v e. (z i^i w)))
31	30	biral 1223	. . . . . . . . . . . . . 14 |- (A.w e. x (-. z = w -> -. v e. (z i^i w)) <-> A.w e. x -. (-. z = w /\ v e. (z i^i w)))
32		ralnex 1209	. . . . . . . . . . . . . 14 |- (A.w e. x -. (-. z = w /\ v e. (z i^i w)) <-> -. E.w e. x (-. z = w /\ v e. (z i^i w)))
33	31, 32	bitr 151	. . . . . . . . . . . . 13 |- (A.w e. x (-. z = w -> -. v e. (z i^i w)) <-> -. E.w e. x (-. z = w /\ v e. (z i^i w)))
34	33	birex 1224	. . . . . . . . . . . 12 |- (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)))
35		rexnal 1210	. . . . . . . . . . . 12 |- (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)))
36	29, 34, 35	3bitr 155	. . . . . . . . . . 11 |- (-. (z \ U.(x \ {z})) = (/) <-> -. A.v e. z E.w e. x (-. z = w /\ v e. (z i^i w)))
37	36	biral 1223	. . . . . . . . . 10 |- (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)))
38		ralnex 1209	. . . . . . . . . 10 |- (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)))
39	37, 38	bitr 151	. . . . . . . . 9 |- (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