Theorem kmlem11 4758

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 2463	. . . . . . 7 |- (z e. x -> {z} (_ x)
2		ssequn1 2197	. . . . . . 7 |- ({z} (_ x <-> ({z} u. x) = x)
3	1, 2	sylib 198	. . . . . 6 |- (z e. x -> ({z} u. x) = x)
4		undif2 2338	. . . . . 6 |- ({z} u. (x \ {z})) = ({z} u. x)
5	3, 4	syl5req 1518	. . . . 5 |- (z e. x -> x = ({z} u. (x \ {z})))
6		iuneq1 2571	. . . . 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 4751	. . . . . . . . . . . 12 |- ((z e. x /\ t =/= z) -> ((t \ U.(x \ {t})) i^i z) = (/))
9		incom 2205	. . . . . . . . . . . 12 |- (z i^i (t \ U.(x \ {t}))) = ((t \ U.(x \ {t})) i^i z)
10	8, 9	syl5eq 1517	. . . . . . . . . . 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 2459	. . . . . . . . . . 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 1711	. . . . . . . 8 |- (z e. x -> A.t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = (/))
16		iuneq2 2574	. . . . . . . 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 2600	. . . . . . 7 |- U_t e. (x \ {z})(/) = (/)
19	17, 18	syl6eq 1521	. . . . . 6 |- (z e. x -> U_t e. (x \ {z})(z i^i (t \ U.(x \ {t}))) = (/))
20	19	uneq2d 2181	. . . . 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 2610	. . . . . 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 1810	. . . . . . . 8 |- z e. V
23		difeq1 2150	. . . . . . . . . 10 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {t})))
24		sneq 2414	. . . . . . . . . . . . 13 |- (t = z -> {t} = {z})
25	24	difeq2d 2156	. . . . . . . . . . . 12 |- (t = z -> (x \ {t}) = (x \ {z}))
26	25	unieqd 2508	. . . . . . . . . . 11 |- (t = z -> U.(x \ {t}) = U.(x \ {z}))
27	26	difeq2d 2156	. . . . . . . . . 10 |- (t = z -> (z \ U.(x \ {t})) = (z \ U.(x \ {z})))
28	23, 27	eqtrd 1505	. . . . . . . . 9 |- (t = z -> (t \ U.(x \ {t})) = (z \ U.(x \ {z})))
29	28	ineq2d 2214	. . . . . . . 8 |- (t = z -> (z i^i (t \ U.(x \ {t}))) = (z i^i (z \ U.(x \ {z}))))
30	22, 29	iunxsn 2608	. . . . . . 7 |- U_t e. {z} (z i^i (t \ U.(x \ {t}))) = (z i^i (z \ U.(x \ {z})))
31	30	uneq1i 2177	. . . . . 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 1493	. . . . 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 1517	. . . 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 1505	. . 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 2294	. . . 4 |- ((z i^i (z \ U.(x \ {z}))) u. (/)) = (z i^i (z \ U.(x \ {z})))
36		indif 2247	. . . 4 |- (z i^i (z \ U.(x \ {z}))) = (z \ U.(x \ {z}))
37	35, 36	eqtr 1493	. . 3 |- ((z i^i (z \ U.(x \ {z}))) u. (/)) = (z \ U.(x \ {z}))
38	34, 37	syl6eq 1521	. 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 2507	. . . . 5 |- U.A = U.{u | E.t e. x u = (t \ U.(x \ {t}))}
41		visset 1810	. . . . . . 7 |- t e. V
42		difexg 2718	. . . . . . 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 2583	. . . . 5 |- U_t e. x (t \ U.(x \ {t})) = U.{u | E.t e. x u = (t \ U.(x \ {t}))}
45	40, 44	eqtr4 1496	. . . 4 |- U.A = U_t e. x (t \ U.(x \ {t}))
46	45	ineq2i 2211	. . 3 |- (z i^i U.A) = (z i^i U_t e. x (t \ U.(x \ {t})))
47		iunin2 2604	. . 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 1496	. 2 |- (z i^i U.A) = U_t e. x (z i^i (t \ U.(x \ {t})))
49	38, 48	syl5eq 1517	1 |- (z e. x -> (z i^i U.A) = (z \ U.(x \ {z})))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 955   e. wcel 957  {cab 1462   =/= wne 1583  A.wral 1643  E.wrex 1644  Vcvv 1808   \ cdif 2041   u. cun 2042   i^i cin 2043   (_ wss 2044  (/)c0 2277  {csn 2406  U.cuni 2499  U_ciun 2562

This theorem is referenced by:  kmlem12 4759

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-sn 2409  df-pr 2410  df-uni 2500  df-iun 2564

Copyright terms: Public domain