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∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))}

Assertion

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

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196   = weq 797   ∈ wel 803  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  Vcvv 1348   ∖ cdif 1484   ∪ cun 1485   ∩ cin 1486   ⊆ wss 1487  ∅c0 1707  {csn 1808  ∪cuni 1919  ∪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