Theorem kmlem10 3589

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
kmlem10	|- (z e. x -> (z i^i U.A) = (z \ U.(x \ {z})))

Distinct variable group(s):   x,z,u,t   z,A

Proof of Theorem kmlem10

Step	Hyp	Ref	Expression
1		snssi 1851	. . . . . . 7 |- (z e. x -> {z} (_ x)
2		ssequn1 1628	. . . . . . 7 |- ({z} (_ x <-> ({z} u. x) = x)
3	1, 2	sylib 173	. . . . . 6 |- (z e. x -> ({z} u. x) = x)
4		undif2 1762	. . . . . 6 |- ({z} u. (x \ {z})) = ({z} u. x)
5	3, 4	syl5req 1137	. . . . 5 |- (z e. x -> x = ({z} u. (x \ {z})))
6		iuneq1 2003	. . . . 5 |- (x = ({z} u. (x \ {z})) -> U.t e. x (z i^i (t \ U.(x \ {t}))) = U.t e. ({z} u. (x \ {z}))(z i^i (t \ U.(x \ {t}))))
7	5, 6	syl 12	. . . 4 |- (z e. x -> U.t e. x (z i^i (t \ U.(x \ {t}))) = U.t e. ({z} u. (x \ {z}))(z i^i (t \ U.(x \ {t}))))
8		kmlem4 3583	. . . . . . . . . . . 12 |- ((z e. x /\ -. t = z) -> ((t \ U.(x \ {t})) i^i z) = (/))
9		incom 1636	. . . . . . . . . . . 12 |- (z i^i (t \ U.(x \ {t}))) = ((t \ U.(x \ {t})) i^i z)
10	8, 9	syl5eq 1136	. . . . . . . . . . 11 |- ((z e. x /\ -. t = z) -> (z i^i (t \ U.(x \ {t}))) = (/))
11	10	exp 291	. . . . . . . . . 10 |- (z e. x -> (-. t = z -> (z i^i (t \ U.(x \ {t}))) = (/)))
12		eldifn 1592	. . . . . . . . . . 11 |- (t e. (x \ {z}) -> -. t e. {z})
13		elsn 1820	. . . . . . . . . . . 12 |- (t e. {z} <-> t = z)
14	13	negbii 162	. . . . . . . . . . 11 |- (-. t e. {z} <-> -. t = z)
15	12, 14	sylib 173	. . . . . . . . . 10 |- (t e. (x \ {z}) -> -. t = z)
16	11, 15	syl5 22	. . . . . . . . 9 |- (z e. x -> (t e. (x \ {z}) -> (z i^i (t \ U.(x \ {t}))) = (/)))
17	16	r19.21aiv 1259	. . . . . . . 8 |- (z e. x -> A.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = (/))
18		iuneq2 2006	. . . . . . . 8 |- (A.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = (/) -> U.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = U.t e. (x \ {z})(/))
19	17, 18	syl 12	. . . . . . 7 |- (z e. x -> U.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = U.t e. (x \ {z})(/))
20		iun0 2028	. . . . . . 7 |- U.t e. (x \ {z})(/) = (/)
21	19, 20	syl6eq 1140	. . . . . 6 |- (z e. x -> U.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = (/))
22	21	uneq2d 1611	. . . . 5 |- (z e. x -> ((z i^i (z \ U.(x \ {z}))) u. U.t e. (x \ {z})(z i^i (t \ U.(x \ {t})))) = ((z i^i (z \ U.(x \ {z}))) u. (/)))
23		iunxun 2035	. . . . . 6 |- U.t e. ({z} u. (x \ {z}))(z i^i (t \ U.(x \ {t}))) = (U.t e. {z} (z i^i (t \ U.(x \ {t}))) u. U.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))))
24		visset 1350	. . . . . . . 8 |- z e. V
25		difeq1 1582	. . . . . . . . . 10 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {t})))
26		sneq 1816	. . . . . . . . . . . . 13 |- (t = z -> {t} = {z})
27	26	difeq2d 1588	. . . . . . . . . . . 12 |- (t = z -> (x \ {t}) = (x \ {z}))
28	27	unieqd 1929	. . . . . . . . . . 11 |- (t = z -> U.(x \ {t}) = U.(x \ {z}))
29	28	difeq2d 1588	. . . . . . . . . 10 |- (t = z -> (z \ U.(x \ {t})) = (z \ U.(x \ {z})))
30	25, 29	eqtrd 1128	. . . . . . . . 9 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {z})))
31	30	ineq2d 1645	. . . . . . . 8 |- (t = z -> (z i^i (t \ U.(x \ {t}))) = (z i^i (z \ U.(x \ {z}))))
32	24, 31	iunxsn 2034	. . . . . . 7 |- U.t e. {z} (z i^i (t \ U.(x \ {t}))) = (z i^i (z \ U.(x \ {z})))
33	32	uneq1i 1607	. . . . . 6 |- (U.t e. {z} (z i^i (t \ U.(x \ {t}))) u. U.t e. (x \ {z})(z i^i (t \ U.(x \ {t})))) = ((z i^i (z \ U.(x \ {z}))) u. U.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))))
34	23, 33	eqtr 1119	. . . . 5 |- U.t e. ({z} u. (x \ {z}))(z i^i (t \ U.(x \ {t}))) = ((z i^i (z \ U.(x \ {z}))) u. U.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))))
35	22, 34	syl5eq 1136	. . . 4 |- (z e. x -> U.t e. ({z} u. (x \ {z}))(z i^i (t \ U.(x \ {t}))) = ((z i^i (z \ U.(x \ {z}))) u. (/)))
36	7, 35	eqtrd 1128	. . 3 |- (z e. x -> U.t e. x (z i^i (t \ U.(x \ {t}))) = ((z i^i (z \ U.(x \ {z}))) u. (/)))
37		un0 1721	. . . 4 |- ((z i^i (z \ U.(x \ {z}))) u. (/)) = (z i^i (z \ U.(x \ {z})))
38		difss 1596	. . . . 5 |- (z \ U.(x \ {z})) (_ z
39		sseqin2 1656	. . . . 5 |- ((z \ U.(x \ {z})) (_ z <-> (z i^i (z \ U.(x \ {z}))) = (z \ U.(x \ {z})))
40	38, 39	mpbi 164	. . . 4 |- (z i^i (z \ U.(x \ {z}))) = (z \ U.(x \ {z}))
41	37, 40	eqtr 1119	. . 3 |- ((z i^i (z \ U.(x \ {z}))) u. (/)) = (z \ U.(x \ {z}))
42	36, 41	syl6eq 1140	. 2 |- (z e. x -> U.t e. x (z i^i (t \ U.(x \ {t}))) = (z \ U.(x \ {z})))
43		kmlem8.1	. . . . . 6 |- A = {u | E.t e. x u = (t \ U.(x \ {t}))}
44	43	unieqi 1928	. . . . 5 |- U.A = U.{u | E.t e. x u = (t \ U.(x \ {t}))}
45		visset 1350	. . . . . . 7 |- t e. V
46		difexg 1703	. . . . . . 7 |- (t e. V -> (t \ U.(x \ {t})) e. V)
47	45, 46	ax-mp 6	. . . . . 6 |- (t \ U.(x \ {t})) e. V
48	47	dfiun2 2014	. . . . 5 |- U.t e. x (t \ U.(x \ {t})) = U.{u | E.t e. x u = (t \ U.(x \ {t}))}
49	44, 48	eqtr4 1122	. . . 4 |- U.A = U.t e. x (t \ U.(x \ {t}))
50	49	ineq2i 1642	. . 3 |- (z i^i U.A) = (z i^i U.t e. x (t \ U.(x \ {t})))
51		iunin2 2030	. . 3 |- U.t e. x (z i^i (t \ U.(x \ {t}))) = (z i^i U.t e. x (t \ U.(x \ {t})))
52	50, 51	eqtr4 1122	. 2 |- (z i^i U.A) = U.t e. x (z i^i (t \ U.(x \ {t})))
53	42, 52	syl5eq 1136	1 |- (z e. x -> (z i^i U.A) = (z \ U.(x \ {z})))

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196   = weq 797   e. wel 803  {cab 1090   = wceq 1091   e. wcel 1092  A.wral 1201  E.wrex 1202  Vcvv 1348   \ cdif 1484   u. cun 1485   i^i cin 1486   (_ wss 1487  (/)c0 1707  {csn 1808  U.cuni 1919  U.ciun 1994

This theorem is referenced by:  kmlem11 3590

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-sn 1811  df-uni 1920  df-iun 1996

metamath.org