Theorem kmlem9 8863

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

Hypothesis

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

Assertion

Ref	Expression
kmlem9	⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)

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

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

Proof of Theorem kmlem9

Dummy variable ℎ is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3176	. . . 4 ⊢ 𝑧 ∈ V
2		eqeq1 2614	. . . . 5 ⊢ (𝑢 = 𝑧 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
3	2	rexbidv 3034	. . . 4 ⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
4		kmlem9.1	. . . 4 ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}
5	1, 3, 4	elab2 3323	. . 3 ⊢ (𝑧 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
6		vex 3176	. . . . 5 ⊢ 𝑤 ∈ V
7		eqeq1 2614	. . . . . 6 ⊢ (𝑢 = 𝑤 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
8	7	rexbidv 3034	. . . . 5 ⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
9	6, 8, 4	elab2 3323	. . . 4 ⊢ (𝑤 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
10		difeq1 3683	. . . . . . 7 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {𝑡})))
11		sneq 4135	. . . . . . . . . 10 ⊢ (𝑡 = ℎ → {𝑡} = {ℎ})
12	11	difeq2d 3690	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {ℎ}))
13	12	unieqd 4382	. . . . . . . 8 ⊢ (𝑡 = ℎ → ∪ (𝑥 ∖ {𝑡}) = ∪ (𝑥 ∖ {ℎ}))
14	13	difeq2d 3690	. . . . . . 7 ⊢ (𝑡 = ℎ → (ℎ ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
15	10, 14	eqtrd 2644	. . . . . 6 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
16	15	eqeq2d 2620	. . . . 5 ⊢ (𝑡 = ℎ → (𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
17	16	cbvrexv 3148	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
18	9, 17	bitri 263	. . 3 ⊢ (𝑤 ∈ 𝐴 ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
19		reeanv 3086	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) ↔ (∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
20		eqeq12 2623	. . . . . . . . . 10 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 = 𝑤 ↔ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
21	15, 20	syl5ibr 235	. . . . . . . . 9 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑡 = ℎ → 𝑧 = 𝑤))
22	21	necon3d 2803	. . . . . . . 8 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → 𝑡 ≠ ℎ))
23		kmlem5 8859	. . . . . . . . . 10 ⊢ ((ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ) → ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) = ∅)
24		ineq12 3771	. . . . . . . . . . 11 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ∩ 𝑤) = ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
25	24	eqeq1d 2612	. . . . . . . . . 10 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → ((𝑧 ∩ 𝑤) = ∅ ↔ ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) = ∅))
26	23, 25	syl5ibr 235	. . . . . . . . 9 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → ((ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ) → (𝑧 ∩ 𝑤) = ∅))
27	26	expd 451	. . . . . . . 8 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (ℎ ∈ 𝑥 → (𝑡 ≠ ℎ → (𝑧 ∩ 𝑤) = ∅)))
28	22, 27	syl5d 71	. . . . . . 7 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (ℎ ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
29	28	com12 32	. . . . . 6 ⊢ (ℎ ∈ 𝑥 → ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
30	29	adantl 481	. . . . 5 ⊢ ((𝑡 ∈ 𝑥 ∧ ℎ ∈ 𝑥) → ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
31	30	rexlimivv 3018	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
32	19, 31	sylbir 224	. . 3 ⊢ ((∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
33	5, 18, 32	syl2anb 495	. 2 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
34	33	rgen2a 2960	1 ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537   ∩ cin 3539  ∅c0 3874  {csn 4125  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126  df-uni 4373

This theorem is referenced by:  kmlem10  8864