Theorem kmlem2 4746

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

Assertion

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

Distinct variable groups:   x,y,ph   x,w,y,z

Proof of Theorem kmlem2

Step	Hyp	Ref	Expression
1		ineq2 2207	. . . . . . . 8 |- (y = v -> (z i^i y) = (z i^i v))
2	1	eleq2d 1538	. . . . . . 7 |- (y = v -> (w e. (z i^i y) <-> w e. (z i^i v)))
3	2	eubidv 1384	. . . . . 6 |- (y = v -> (E!w w e. (z i^i y) <-> E!w w e. (z i^i v)))
4	3	imbi2d 611	. . . . 5 |- (y = v -> ((ph -> E!w w e. (z i^i y)) <-> (ph -> E!w w e. (z i^i v))))
5	4	ralbidv 1660	. . . 4 |- (y = v -> (A.z e. x (ph -> E!w w e. (z i^i y)) <-> A.z e. x (ph -> E!w w e. (z i^i v))))
6	5	cbvexv 1313	. . 3 |- (E.yA.z e. x (ph -> E!w w e. (z i^i y)) <-> E.vA.z e. x (ph -> E!w w e. (z i^i v)))
7		visset 1809	. . . . . . 7 |- x e. V
8	7	uniex 2865	. . . . . 6 |- U.x e. V
9		eleq2 1532	. . . . . . . 8 |- (y = U.x -> (u e. y <-> u e. U.x))
10	9	negbid 610	. . . . . . 7 |- (y = U.x -> (-. u e. y <-> -. u e. U.x))
11	10	exbidv 1277	. . . . . 6 |- (y = U.x -> (E.u -. u e. y <-> E.u -. u e. U.x))
12		nalset 2707	. . . . . . . 8 |- -. E.yA.u u e. y
13		alexn 1042	. . . . . . . 8 |- (A.yE.u -. u e. y <-> -. E.yA.u u e. y)
14	12, 13	mpbir 190	. . . . . . 7 |- A.yE.u -. u e. y
15	14	a4i 980	. . . . . 6 |- E.u -. u e. y
16	8, 11, 15	vtocl 1838	. . . . 5 |- E.u -. u e. U.x
17		elssuni 2521	. . . . . . . . . . . . . . . . . . 19 |- (z e. x -> z (_ U.x)
18	17	sseld 2063	. . . . . . . . . . . . . . . . . 18 |- (z e. x -> (u e. z -> u e. U.x))
19	18	con3d 95	. . . . . . . . . . . . . . . . 17 |- (z e. x -> (-. u e. U.x -> -. u e. z))
20		disjsn 2437	. . . . . . . . . . . . . . . . 17 |- ((z i^i {u}) = (/) <-> -. u e. z)
21	19, 20	syl6ibr 213	. . . . . . . . . . . . . . . 16 |- (z e. x -> (-. u e. U.x -> (z i^i {u}) = (/)))
22	21	impcom 351	. . . . . . . . . . . . . . 15 |- ((-. u e. U.x /\ z e. x) -> (z i^i {u}) = (/))
23	22	uneq2d 2180	. . . . . . . . . . . . . 14 |- ((-. u e. U.x /\ z e. x) -> ((z i^i v) u. (z i^i {u})) = ((z i^i v) u. (/)))
24		un0 2293	. . . . . . . . . . . . . 14 |- ((z i^i v) u. (/)) = (z i^i v)
25	23, 24	syl6eq 1520	. . . . . . . . . . . . 13 |- ((-. u e. U.x /\ z e. x) -> ((z i^i v) u. (z i^i {u})) = (z i^i v))
26		indi 2247	. . . . . . . . . . . . 13 |- (z i^i (v u. {u})) = ((z i^i v) u. (z i^i {u}))
27	25, 26	syl5req 1517	. . . . . . . . . . . 12 |- ((-. u e. U.x /\ z e. x) -> (z i^i v) = (z i^i (v u. {u})))
28	27	eleq2d 1538	. . . . . . . . . . 11 |- ((-. u e. U.x /\ z e. x) -> (w e. (z i^i v) <-> w e. (z i^i (v u. {u}))))
29	28	eubidv 1384	. . . . . . . . . 10 |- ((-. u e. U.x /\ z e. x) -> (E!w w e. (z i^i v) <-> E!w w e. (z i^i (v u. {u}))))
30	29	imbi2d 611	. . . . . . . . 9 |- ((-. u e. U.x /\ z e. x) -> ((ph -> E!w w e. (z i^i v)) <-> (ph -> E!w w e. (z i^i (v u. {u})))))
31	30	ralbidva 1656	. . . . . . . 8 |- (-. u e. U.x -> (A.z e. x (ph -> E!w w e. (z i^i v)) <-> A.z e. x (ph -> E!w w e. (z i^i (v u. {u})))))
32		visset 1809	. . . . . . . . . . . . . 14 |- u e. V
33	32	snid 2431	. . . . . . . . . . . . 13 |- u e. {u}
34	33	olci 271	. . . . . . . . . . . 12 |- (u e. v \/ u e. {u})
35		elun 2169	. . . . . . . . . . . 12 |- (u e. (v u. {u}) <-> (u e. v \/ u e. {u}))
36	34, 35	mpbir 190	. . . . . . . . . . 11 |- u e. (v u. {u})
37		elssuni 2521	. . . . . . . . . . . 12 |- ((v u. {u}) e. x -> (v u. {u}) (_ U.x)
38	37	sseld 2063	. . . . . . . . . . 11 |- ((v u. {u}) e. x -> (u e. (v u. {u}) -> u e. U.x))
39	36, 38	mpi 44	. . . . . . . . . 10 |- ((v u. {u}) e. x -> u e. U.x)
40	39	con3i 98	. . . . . . . . 9 |- (-. u e. U.x -> -. (v u. {u}) e. x)
41	40	biantrurd 726	. . . . . . . 8 |- (-. u e. U.x -> (A.z e. x (ph -> E!w w e. (z i^i (v u. {u}))) <-> (-. (v u. {u}) e. x /\ A.z e. x (ph -> E!w w e. (z i^i (v u. {u}))))))
42	31, 41	bitrd 527	. . . . . . 7 |- (-. u e. U.x -> (A.z e. x (ph -> E!w w e. (z i^i v)) <-> (-. (v u. {u}) e. x /\ A.z e. x (ph -> E!w w e. (z i^i (v u. {u}))))))
43		visset 1809	. . . . . . . . 9 |- v e. V
44		snex 2745	. . . . . . . . 9 |- {u} e. V
45	43, 44	unex 2867	. . . . . . . 8 |- (v u. {u}) e. V
46		eleq1 1531	. . . . . . . . . 10 |- (y = (v u. {u}) -> (y e. x <-> (v u. {u}) e. x))
47	46	negbid 610	. . . . . . . . 9 |- (y = (v u. {u}) -> (-. y e. x <-> -. (v u. {u}) e. x))
48		ineq2 2207	. . . . . . . . . . . . 13 |- (y = (v u. {u}) -> (z i^i y) = (z i^i (v u. {u})))
49	48	eleq2d 1538	. . . . . . . . . . . 12 |- (y = (v u. {u}) -> (w e. (z i^i y) <-> w e. (z i^i (v u. {u}))))
50	49	eubidv 1384	. . . . . . . . . . 11 |- (y = (v u. {u}) -> (E!w w e. (z i^i y) <-> E!w w e. (z i^i (v u. {u}))))
51	50	imbi2d 611	. . . . . . . . . 10 |- (y = (v u. {u}) -> ((ph -> E!w w e. (z i^i y)) <-> (ph -> E!w w e. (z i^i (v u. {u})))))
52	51	ralbidv 1660	. . . . . . . . 9 |- (y = (v u. {u}) -> (A.z e. x (ph -> E!w w e. (z i^i y)) <-> A.z e. x (ph -> E!w w e. (z i^i (v u. {u})))))
53	47, 52	anbi12d 627	. . . . . . . 8 |- (y = (v u. {u}) -> ((-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y))) <-> (-. (v u. {u}) e. x /\ A.z e. x (ph -> E!w w e. (z i^i (v u. {u}))))))
54	45, 53	cla4ev 1865	. . . . . . 7 |- ((-. (v u. {u}) e. x /\ A.z e. x (ph -> E!w w e. (z i^i (v u. {u})))) -> E.y(-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y))))
55	42, 54	syl6bi 214	. . . . . 6 |- (-. u e. U.x -> (A.z e. x (ph -> E!w w e. (z i^i v)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y)))))
56	55	19.23aiv 1293	. . . . 5 |- (E.u -. u e. U.x -> (A.z e. x (ph -> E!w w e. (z i^i v)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y)))))
57	16, 56	ax-mp 7	. . . 4 |- (A.z e. x (ph -> E!w w e. (z i^i v)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y))))
58	57	19.23aiv 1293	. . 3 |- (E.vA.z e. x (ph -> E!w w e. (z i^i v)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y))))
59	6, 58	sylbi 199	. 2 |- (E.yA.z e. x (ph -> E!w w e. (z i^i y)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y))))
60		pm3.27 323	. . 3 |- ((-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y))) -> A.z e. x (ph -> E!w w e. (z i^i y)))
61	60	19.22i 1038	. 2 |- (E.y(-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y))) -> E.yA.z e. x (ph -> E!w w e. (z i^i y)))
62	59, 61	impbi 157	1 |- (E.yA.z e. x (ph -> E!w w e. (z i^i y)) <-> E.y(-. y e. x /\ A.z e. x (ph -> E!w w e. (z i^i y))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956  E.wex 978  E!weu 1378  A.wral 1642   u. cun 2041   i^i cin 2042  (/)c0 2276  {csn 2405  U.cuni 2498

This theorem is referenced by:  kmlem8 4752

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960