Theorem kmlem12 4786

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

Hypothesis

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

Assertion

Ref	Expression
kmlem12	|- (A.z e. x (z \ U.(x \ {z})) =/= (/) -> (A.z e. A (z =/= (/) -> E!v v e. (z i^i y)) -> A.z e. x (z =/= (/) -> E!v v e. (z i^i (y i^i U.A)))))

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

Proof of Theorem kmlem12

Step	Hyp	Ref	Expression
1		difeq1 2156	. . . . . . . 8 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {t})))
2		sneq 2421	. . . . . . . . . . 11 |- (t = z -> {t} = {z})
3	2	difeq2d 2162	. . . . . . . . . 10 |- (t = z -> (x \ {t}) = (x \ {z}))
4	3	unieqd 2516	. . . . . . . . 9 |- (t = z -> U.(x \ {t}) = U.(x \ {z}))
5	4	difeq2d 2162	. . . . . . . 8 |- (t = z -> (z \ U.(x \ {t})) = (z \ U.(x \ {z})))
6	1, 5	eqtrd 1510	. . . . . . 7 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {z})))
7	6	neeq1d 1597	. . . . . 6 |- (t = z -> ((t \ U.(x \ {t})) =/= (/) <-> (z \ U.(x \ {z})) =/= (/)))
8	7	cbvralv 1803	. . . . 5 |- (A.t e. x (t \ U.(x \ {t})) =/= (/) <-> A.z e. x (z \ U.(x \ {z})) =/= (/))
9	6	ineq1d 2219	. . . . . . . 8 |- (t = z -> ((t \ U.(x \ {t})) i^i y) = ((z \ U.(x \ {z})) i^i y))
10	9	eleq2d 1544	. . . . . . 7 |- (t = z -> (v e. ((t \ U.(x \ {t})) i^i y) <-> v e. ((z \ U.(x \ {z})) i^i y)))
11	10	eubidv 1388	. . . . . 6 |- (t = z -> (E!v v e. ((t \ U.(x \ {t})) i^i y) <-> E!v v e. ((z \ U.(x \ {z})) i^i y)))
12	11	cbvralv 1803	. . . . 5 |- (A.t e. x E!v v e. ((t \ U.(x \ {t})) i^i y) <-> A.z e. x E!v v e. ((z \ U.(x \ {z})) i^i y))
13	8, 12	imbi12i 188	. . . 4 |- ((A.t e. x (t \ U.(x \ {t})) =/= (/) -> A.t e. x E!v v e. ((t \ U.(x \ {t})) i^i y)) <-> (A.z e. x (z \ U.(x \ {z})) =/= (/) -> A.z e. x E!v v e. ((z \ U.(x \ {z})) i^i y)))
14		kmlem9.1	. . . . . . . . . . . 12 |- A = {u | E.t e. x u = (t \ U.(x \ {t}))}
15	14	kmlem11 4785	. . . . . . . . . . 11 |- (z e. x -> (z i^i U.A) = (z \ U.(x \ {z})))
16	15	ineq1d 2219	. . . . . . . . . 10 |- (z e. x -> ((z i^i U.A) i^i y) = ((z \ U.(x \ {z})) i^i y))
17		in12 2227	. . . . . . . . . . 11 |- (z i^i (y i^i U.A)) = (y i^i (z i^i U.A))
18		incom 2211	. . . . . . . . . . 11 |- (y i^i (z i^i U.A)) = ((z i^i U.A) i^i y)
19	17, 18	eqtr 1498	. . . . . . . . . 10 |- (z i^i (y i^i U.A)) = ((z i^i U.A) i^i y)
20	16, 19	syl5req 1523	. . . . . . . . 9 |- (z e. x -> ((z \ U.(x \ {z})) i^i y) = (z i^i (y i^i U.A)))
21	20	eleq2d 1544	. . . . . . . 8 |- (z e. x -> (v e. ((z \ U.(x \ {z})) i^i y) <-> v e. (z i^i (y i^i U.A))))
22	21	eubidv 1388	. . . . . . 7 |- (z e. x -> (E!v v e. ((z \ U.(x \ {z})) i^i y) <-> E!v v e. (z i^i (y i^i U.A))))
23		ax-1 4	. . . . . . 7 |- (E!v v e. (z i^i (y i^i U.A)) -> (z =/= (/) -> E!v v e. (z i^i (y i^i U.A))))
24	22, 23	syl6bi 214	. . . . . 6 |- (z e. x -> (E!v v e. ((z \ U.(x \ {z})) i^i y) -> (z =/= (/) -> E!v v e. (z i^i (y i^i U.A)))))
25	24	r19.20i 1707	. . . . 5 |- (A.z e. x E!v v e. ((z \ U.(x \ {z})) i^i y) -> A.z e. x (z =/= (/) -> E!v v e. (z i^i (y i^i U.A))))
26	25	imim2i 17	. . . 4 |- ((A.z e. x (z \ U.(x \ {z})) =/= (/) -> A.z e. x E!v v e. ((z \ U.(x \ {z})) i^i y)) -> (A.z e. x (z \ U.(x \ {z})) =/= (/) -> A.z e. x (z =/= (/) -> E!v v e. (z i^i (y i^i U.A)))))
27	13, 26	sylbi 199	. . 3 |- ((A.t e. x (t \ U.(x \ {t})) =/= (/) -> A.t e. x E!v v e. ((t \ U.(x \ {t})) i^i y)) -> (A.z e. x (z \ U.(x \ {z})) =/= (/) -> A.z e. x (z =/= (/) -> E!v v e. (z i^i (y i^i U.A)))))
28	27	com12 11	. 2 |- (A.z e. x (z \ U.(x \ {z})) =/= (/) -> ((A.t e. x (t \ U.(x \ {t})) =/= (/) -> A.t e. x E!v v e. ((t \ U.(x \ {t})) i^i y)) -> A.z e. x (z =/= (/) -> E!v v e. (z i^i (y i^i U.A)))))
29		raleq1 1789	. . . . 5 |- (A = {u | E.t e. x u = (t \ U.(x \ {t}))} -> (A.z e. A (z =/= (/) -> E!v v e. (z i^i y)) <-> A.z e. {u | E.t e. x u = (t \ U.(x \ {t}))} (z =/= (/) -> E!v v e. (z i^i y))))
30	14, 29	ax-mp 7	. . . 4 |- (A.z e. A (z =/= (/) -> E!v v e. (z i^i y)) <-> A.z e. {u | E.t e. x u = (t \ U.(x \ {t}))} (z =/= (/) -> E!v v e. (z i^i y)))
31		df-ral 1652	. . . 4 |- (A.z e. {u | E.t e. x u = (t \ U.(x \ {t}))} (z =/= (/) -> E!v v e. (z i^i y)) <-> A.z(z e. {u | E.t e. x u = (t \ U.(x \ {t}))} -> (z =/= (/) -> E!v v e. (z i^i y))))
32		visset 1816	. . . . . . . . 9 |- z e. V
33		eqeq1 1484	. . . . . . . . . 10 |- (u = z -> (u = (t \ U.(x \ {t})) <-> z = (t \ U.(x \ {t}))))
34	33	rexbidv 1667	. . . . . . . . 9 |- (u = z -> (E.t e. x u = (t \ U.(x \ {t})) <-> E.t e. x z = (t \ U.(x \ {t}))))
35	32, 34	elab 1900	. . . . . . . 8 |- (z e. {u | E.t e. x u = (t \ U.(x \ {t}))} <-> E.t e. x z = (t \ U.(x \ {t})))
36	35	imbi1i 186	. . . . . . 7 |- ((z e. {u | E.t e. x u = (t \ U.(x \ {t}))} -> (z =/= (/) -> E!v v e. (z i^i y))) <-> (E.t e. x z = (t \ U.(x \ {t})) -> (z =/= (/) -> E!v v e. (z i^i y))))
37		r19.23v 1744	. . . . . . 7 |- (A.t e. x (z = (t \ U.(x \ {t})) -> (z =/= (/) -> E!v v e. (z i^i y))) <-> (E.t e. x z = (t \ U.(x \ {t})) -> (z =/= (/) -> E!v v e. (z i^i y))))
38	36, 37	bitr4 176	. . . . . 6 |- ((z e. {u | E.t e. x u = (t \ U.(x \ {t}))} -> (z =/= (/) -> E!v v e. (z i^i y))) <-> A.t e. x (z = (t \ U.(x \ {t})) -> (z =/= (/) -> E!v v e. (z i^i y))))
39	38	albii 1001	. . . . 5 |- (A.z(z e. {u | E.t e. x u = (t \ U.(x \ {t}))} -> (z =/= (/) -> E!v v e. (z i^i y))) <-> A.zA.t e. x (z = (t \ U.(x \ {t})) -> (z =/= (/) -> E!v v e. (z i^i y))))
40		ralcom4 1826	. . . . 5 |- (A.t e. x A.z(z = (t \ U.(x \ {t})) -> (z =/= (/) -> E!v v e. (z i^i y))) <-> A.zA.t e. x (z = (t \ U.(x \ {t})) -> (z =/= (/) -> E!v v e. (z i^i