Theorem kmlem11 3590

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

Hypothesis

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

Assertion

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

Proof of Theorem kmlem11

Step	Hyp	Ref	Expression
1		difeq1 1582	. . . . . . . . 9 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {t})))
2		sneq 1816	. . . . . . . . . . . 12 |- (t = z -> {t} = {z})
3	2	difeq2d 1588	. . . . . . . . . . 11 |- (t = z -> (x \ {t}) = (x \ {z}))
4	3	unieqd 1929	. . . . . . . . . 10 |- (t = z -> U.(x \ {t}) = U.(x \ {z}))
5	4	difeq2d 1588	. . . . . . . . 9 |- (t = z -> (z \ U.(x \ {t})) = (z \ U.(x \ {z})))
6	1, 5	eqtrd 1128	. . . . . . . 8 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {z})))
7	6	cleq1d 1109	. . . . . . 7 |- (t = z -> ((t \ U.(x \ {t})) = (/) <-> (z \ U.(x \ {z})) = (/)))
8	7	negbid 463	. . . . . 6 |- (t = z -> (-. (t \ U.(x \ {t})) = (/) <-> -. (z \ U.(x \ {z})) = (/)))
9	8	cbvralv 1333	. . . . 5 |- (A.t e. x -. (t \ U.(x \ {t})) = (/) <-> A.z e. x -. (z \ U.(x \ {z})) = (/))
10	6	ineq1d 1644	. . . . . . . 8 |- (t = z -> ((t \ U.(x \ {t})) i^i y) = ((z \ U.(x \ {z})) i^i y))
11	10	eleq2d 1156	. . . . . . 7 |- (t = z -> (v e. ((t \ U.(x \ {t})) i^i y) <-> v e. ((z \ U.(x \ {z})) i^i y)))
12	11	bieudv 1013	. . . . . 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)))
13	12	cbvralv 1333	. . . . 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))
14	9, 13	imbi12i 163	. . . 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)))
15		kmlem8.1	. . . . . . . . . . . 12 |- A = {u | E.t e. x u = (t \ U.(x \ {t}))}
16	15	kmlem10 3589	. . . . . . . . . . 11 |- (z e. x -> (z i^i U.A) = (z \ U.(x \ {z})))
17	16	ineq1d 1644	. . . . . . . . . 10 |- (z e. x -> ((z i^i U.A) i^i y) = ((z \ U.(x \ {z})) i^i y))
18		in12 1651	. . . . . . . . . . 11 |- (z i^i (y i^i U.A)) = (y i^i (z i^i U.A))
19		incom 1636	. . . . . . . . . . 11 |- (y i^i (z i^i U.A)) = ((z i^i U.A) i^i y)
20	18, 19	eqtr 1119	. . . . . . . . . 10 |- (z i^i (y i^i U.A)) = ((z i^i U.A) i^i y)
21	17, 20	syl5req 1137	. . . . . . . . 9 |- (z e. x -> ((z \ U.(x \ {z})) i^i y) = (z i^i (y i^i U.A)))
22	21	eleq2d 1156	. . . . . . . 8 |- (z e. x -> (v e. ((z \ U.(x \ {z})) i^i y) <-> v e. (z i^i (y i^i U.A))))
23	22	bieudv 1013	. . . . . . 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))))
24		ax-1 3	. . . . . . 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))))
25	23, 24	syl6bi 187	. . . . . 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)))))
26	25	r19.20i 1253	. . . . 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))))
27	26	syl3 18	. . . 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)))))
28	14, 27	sylbi 174	. . 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)))))
29	28	com12 13	. 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)))))
30		raleq 1324	. . . . 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))))
31	15, 30	ax-mp 6	. . . 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)))
32		df-ral 1205	. . . 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))))
33		visset 1350	. . . . . . . . 9 |- z e. V
34		cleq1 1107	. . . . . . . . . 10 |- (u = z -> (u = (t \ U.(x \ {t})) <-> z = (t \ U.(x \ {t}))))
35	34	birexdv 1220	. . . . . . . . 9 |- (u = z -> (E.t e. x u = (t \ U.(x \ {t})) <-> E.t e. x z = (t \ U.(x \ {t}))))
36	33, 35	elab 1415	. . . . . . . 8 |- (z e. {u | E.t e. x u = (t \ U.(x \ {t}))} <-> E.t e. x z = (t \ U.(x \ {t})))
37	36	imbi1i 161	. . . . . . 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))))
38		r19.23v 1282	. . . . . . 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))))
39	37, 38	bitr4 154	. . . . . 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))))
40	39	bial 695	. . . . 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))))
41		ralcom4 1360	. . . . . 6 |- (A.t e. x A.z(z = (t \ U.(x \ {t})) -> (-. z = (/) -> E!v v e. (z i^i y))) <-> A.zA.t