Theorem kmlem11 4775

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

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

Proof of Theorem kmlem11

Step	Hyp	Ref	Expression
1		snssi 2466	. . . . . . 7 |- (z e. x -> {z} (_ x)
2		ssequn1 2200	. . . . . . 7 |- ({z} (_ x <-> ({z} u. x) = x)
3	1, 2	sylib 198	. . . . . 6 |- (z e. x -> ({z} u. x) = x)
4		undif2 2341	. . . . . 6 |- ({z} u. (x \ {z})) = ({z} u. x)
5	3, 4	syl5req 1520	. . . . 5 |- (z e. x -> x = ({z} u. (x \ {z})))
6		iuneq1 2575	. . . . 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 10	. . . 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 4768	. . . . . . . . . . . 12 |- ((z e. x /\ t =/= z) -> ((t \ U.(x \ {t})) i^i z) = (/))
9		incom 2208	. . . . . . . . . . . 12 |- (z i^i (t \ U.(x \ {t}))) = ((t \ U.(x \ {t})) i^i z)
10	8, 9	syl5eq 1519	. . . . . . . . . . 11 |- ((z e. x /\ t =/= z) -> (z i^i (t \ U.(x \ {t}))) = (/))
11	10	ex 373	. . . . . . . . . 10 |- (z e. x -> (t =/= z -> (z i^i (t \ U.(x \ {t}))) = (/)))
12		eldifsn 2462	. . . . . . . . . . 11 |- (t e. (x \ {z}) <-> (t e. x /\ t =/= z))
13	12	pm3.27bi 326	. . . . . . . . . 10 |- (t e. (x \ {z}) -> t =/= z)
14	11, 13	syl5 21	. . . . . . . . 9 |- (z e. x -> (t e. (x \ {z}) -> (z i^i (t \ U.(x \ {t}))) = (/)))
15	14	r19.21aiv 1713	. . . . . . . 8 |- (z e. x -> A.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = (/))
16		iuneq2 2578	. . . . . . . 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})(/))
17	15, 16	syl 10	. . . . . . 7 |- (z e. x -> U_t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = U_t e. (x \ {z})(/))
18		iun0 2604	. . . . . . 7 |- U_t e. (x \ {z})(/) = (/)
19	17, 18	syl6eq 1523	. . . . . 6 |- (z e. x -> U_t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = (/))
20	19	uneq2d 2184	. . . . 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. (/)))
21		iunxun 2614	. . . . . 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}))))
22		visset 1813	. . . . . . . 8 |- z e. V
23		difeq1 2153	. . . . . . . . . 10 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {t})))
24		sneq 2417	. . . . . . . . . . . . 13 |- (t = z -> {t} = {z})
25	24	difeq2d 2159	. . . . . . . . . . . 12 |- (t = z -> (x \ {t}) = (x \ {z}))
26	25	unieqd 2512	. . . . . . . . . . 11 |- (t = z -> U.(x \ {t}) = U.(x \ {z}))
27	26	difeq2d 2159	. . . . . . . . . 10 |- (t = z -> (z \ U.(x \ {t})) = (z \ U.(x \ {z})))
28	23, 27	eqtrd 1507	. . . . . . . . 9 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {z})))
29	28	ineq2d 2217	. . . . . . . 8 |- (t = z -> (z i^i (t \ U.(x \ {t}))) = (z i^i (z \ U.(x \ {z}))))
30	22, 29	iunxsn 2612	. . . . . . 7 |- U_t e. {z} (z i^i (t \ U.(x \ {t}))) = (z i^i (z \ U.(x \ {z})))
31	30	uneq1i 2180	. . . . . 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}))))
32	21, 31	eqtr 1495	. . . . 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}))))
33	20, 32	syl5eq 1519	. . . 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. (/)))
34	7, 33	eqtrd 1507	. . 3 |- (z e. x -> U_t e. x (z i^i (t \ U.(x \ {t}))) = ((z i^i (z \ U.(x \ {z}))) u. (/)))
35		un0 2297	. . . 4 |- ((z i^i (z \ U.(x \ {z}))) u. (/)) = (z i^i (z \ U.(x \ {z})))
36		indif 2250	. . . 4 |- (z i^i (z \ U.(x \ {z}))) = (z \ U.(x \ {z}))
37	35, 36	eqtr 1495	. . 3 |- ((z i^i (z \ U.(x \ {z}))) u. (/)) = (z \ U.(x \ {z}))
38	34, 37	syl6eq 1523	. 2 |- (z e. x -> U_t e. x (z i^i (t \ U.(x \ {t}))) = (z \ U.(x \ {z})))
39		kmlem9.1	. . . . . 6 |- A = {u | E.t e. x u = (t \ U.(x \ {t}))}
40	39	unieqi 2511	. . . . 5 |- U.A = U.{u | E.t e. x u = (t \ U.(x \ {t}))}
41		visset 1813	. . . . . . 7 |- t e. V
42		difexg 2722	. . . . . . 7 |- (t e. V -> (t \ U.(x \ {t})) e. V)
43	41, 42	ax-mp 7	. . . . . 6 |- (t \ U.(x \ {t})) e. V
44	43	dfiun2 2587	. . . . 5 |- U_t e. x (t \ U.(x \ {t})) = U.{u | E.t e. x u = (t \ U.(x \ {t}))}
45	40, 44	eqtr4 1498	. . . 4 |- U.A = U_t e. x (t \ U.(x \ {t}))
46	45	ineq2i 2214	. . 3 |- (z i^i U.A) = (z i^i U_t e. x (t \ U.(x \ {t})))
47		iunin2 2608	. . 3 |- U_t e. x (z i^i (t \ U.(x \ {t}))) = (z i^i U_t e. x (t \ U.(x \ {t})))
48	46, 47	eqtr4 1498	. 2 |- (z i^i U.A) = U_t e. x (z i^i (t \ U.(x \ {t})))
49	38, 48	syl5eq 1519	1 |- (z e. x -> (z i^i U.A) = (z \ U.(x \ {z})))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958  {cab 1463   =/= wne 1585  A.wral 1645  E.wrex 1646  Vcvv 1811   \ cdif 2044   u. cun 2045   i^i cin 2046   (_ wss 2047  (/)c0 2280  {csn 2409  U.cuni 2503  U_ciun 2566

This theorem is referenced by:  kmlem12 4776

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-sn 2412  df-pr 2413  df-uni 2504  df-iun 2568

Copyright terms: Public domain