Theorem kmlem11 10269

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.)

Hypothesis

Ref	Expression
kmlem9.1	⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}

Assertion

Ref	Expression
kmlem11	⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ ∪ 𝐴) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))

Distinct variable groups:   𝑥,𝑧,𝑢,𝑡   𝑧,𝐴

Allowed substitution hints:   𝐴(𝑥, 𝑢, 𝑡)

Proof of Theorem kmlem11

Step	Hyp	Ref	Expression
1		kmlem9.1	. . . . . 6 ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}
2	1	unieqi 4882	. . . . 5 ⊢ ∪ 𝐴 = ∪ {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}
3		vex 3458	. . . . . . 7 ⊢ 𝑡 ∈ V
4	3	difexi 5297	. . . . . 6 ⊢ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∈ V
5	4	dfiun2 4993	. . . . 5 ⊢ ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = ∪ {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}
6	2, 5	eqtr4i 2789	. . . 4 ⊢ ∪ 𝐴 = ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))
7	6	ineq2i 4117	. . 3 ⊢ (𝑧 ∩ ∪ 𝐴) = (𝑧 ∩ ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
8		iunin2 5032	. . 3 ⊢ ∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
9	7, 8	eqtr4i 2789	. 2 ⊢ (𝑧 ∩ ∪ 𝐴) = ∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
10		undif2 4434	. . . . . 6 ⊢ ({𝑧} ∪ (𝑥 ∖ {𝑧})) = ({𝑧} ∪ 𝑥)
11		snssi 4746	. . . . . . 7 ⊢ (𝑧 ∈ 𝑥 → {𝑧} ⊆ 𝑥)
12		ssequn1 4187	. . . . . . 7 ⊢ ({𝑧} ⊆ 𝑥 ↔ ({𝑧} ∪ 𝑥) = 𝑥)
13	11, 12	sylib 221	. . . . . 6 ⊢ (𝑧 ∈ 𝑥 → ({𝑧} ∪ 𝑥) = 𝑥)
14	10, 13	eqtr2id 2811	. . . . 5 ⊢ (𝑧 ∈ 𝑥 → 𝑥 = ({𝑧} ∪ (𝑥 ∖ {𝑧})))
15	14	iuneq1d 4982	. . . 4 ⊢ (𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
16		iunxun 5057	. . . . . 6 ⊢ ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (∪ 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
17		vex 3458	. . . . . . . 8 ⊢ 𝑧 ∈ V
18		difeq1 4059	. . . . . . . . . 10 ⊢ (𝑡 = 𝑧 → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑡})))
19		sneq 4594	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧})
20	19	difeq2d 4066	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {𝑧}))
21	20	unieqd 4883	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → ∪ (𝑥 ∖ {𝑡}) = ∪ (𝑥 ∖ {𝑧}))
22	21	difeq2d 4066	. . . . . . . . . 10 ⊢ (𝑡 = 𝑧 → (𝑧 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))
23	18, 22	eqtrd 2798	. . . . . . . . 9 ⊢ (𝑡 = 𝑧 → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))
24	23	ineq2d 4120	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))))
25	17, 24	iunxsn 5054	. . . . . . 7 ⊢ ∪ 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))
26	25	uneq1i 4166	. . . . . 6 ⊢ (∪ 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
27	16, 26	eqtri 2786	. . . . 5 ⊢ ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
28		eldifsni 4753	. . . . . . . . . 10 ⊢ (𝑡 ∈ (𝑥 ∖ {𝑧}) → 𝑡 ≠ 𝑧)
29		incom 4109	. . . . . . . . . . . 12 ⊢ (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ 𝑧)
30		kmlem4 10262	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧) → ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ 𝑧) = ∅)
31	29, 30	eqtrid 2810	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧) → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅)
32	31	ex 418	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑥 → (𝑡 ≠ 𝑧 → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅))
33	28, 32	syl5 35	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝑥 → (𝑡 ∈ (𝑥 ∖ {𝑧}) → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅))
34	33	ralrimiv 3157	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑥 → ∀𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅)
35		iuneq2 4974	. . . . . . . 8 ⊢ (∀𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅ → ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})∅)
36	34, 35	syl 18	. . . . . . 7 ⊢ (𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})∅)
37		iun0 5023	. . . . . . 7 ⊢ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})∅ = ∅
38	36, 37	eqtrdi 2814	. . . . . 6 ⊢ (𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅)
39	38	uneq2d 4170	. . . . 5 ⊢ (𝑧 ∈ 𝑥 → ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅))
40	27, 39	eqtrid 2810	. . . 4 ⊢ (𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅))
41	15, 40	eqtrd 2798	. . 3 ⊢ (𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅))
42		un0 4347	. . . 4 ⊢ ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))
43		indif 4228	. . . 4 ⊢ (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))
44	42, 43	eqtri 2786	. . 3 ⊢ ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))
45	41, 44	eqtrdi 2814	. 2 ⊢ (𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))
46	9, 45	eqtrid 2810	1 ⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ ∪ 𝐴) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {cab 2741   ≠ wne 2959  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  {csn 4588  ∪ cuni 4870  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-11 2197  ax-ext 2735  ax-sep 5253

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-sn 4589  df-uni 4871  df-iun 4956

This theorem is used by:  kmlem12  10270