Theorem kmlem9 10050

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 3440	. . . 4 ⊢ 𝑧 ∈ V
2		eqeq1 2735	. . . . 5 ⊢ (𝑢 = 𝑧 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
3	2	rexbidv 3156	. . . 4 ⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
4		kmlem9.1	. . . 4 ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}
5	1, 3, 4	elab2 3638	. . 3 ⊢ (𝑧 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
6		vex 3440	. . . . 5 ⊢ 𝑤 ∈ V
7		eqeq1 2735	. . . . . 6 ⊢ (𝑢 = 𝑤 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
8	7	rexbidv 3156	. . . . 5 ⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
9	6, 8, 4	elab2 3638	. . . 4 ⊢ (𝑤 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
10		difeq1 4069	. . . . . . 7 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {𝑡})))
11		sneq 4586	. . . . . . . . . 10 ⊢ (𝑡 = ℎ → {𝑡} = {ℎ})
12	11	difeq2d 4076	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {ℎ}))
13	12	unieqd 4872	. . . . . . . 8 ⊢ (𝑡 = ℎ → ∪ (𝑥 ∖ {𝑡}) = ∪ (𝑥 ∖ {ℎ}))
14	13	difeq2d 4076	. . . . . . 7 ⊢ (𝑡 = ℎ → (ℎ ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
15	10, 14	eqtrd 2766	. . . . . 6 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
16	15	eqeq2d 2742	. . . . 5 ⊢ (𝑡 = ℎ → (𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
17	16	cbvrexvw 3211	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
18	9, 17	bitri 275	. . 3 ⊢ (𝑤 ∈ 𝐴 ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
19		reeanv 3204	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) ↔ (∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
20		eqeq12 2748	. . . . . . . . . 10 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 = 𝑤 ↔ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
21	15, 20	imbitrrid 246	. . . . . . . . 9 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑡 = ℎ → 𝑧 = 𝑤))
22	21	necon3d 2949	. . . . . . . 8 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → 𝑡 ≠ ℎ))
23		kmlem5 10046	. . . . . . . . . 10 ⊢ ((ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ) → ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) = ∅)
24		ineq12 4165	. . . . . . . . . . 11 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ∩ 𝑤) = ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
25	24	eqeq1d 2733	. . . . . . . . . 10 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → ((𝑧 ∩ 𝑤) = ∅ ↔ ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) = ∅))
26	23, 25	imbitrrid 246	. . . . . . . . 9 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → ((ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ) → (𝑧 ∩ 𝑤) = ∅))
27	26	expd 415	. . . . . . . 8 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (ℎ ∈ 𝑥 → (𝑡 ≠ ℎ → (𝑧 ∩ 𝑤) = ∅)))
28	22, 27	syl5d 73	. . . . . . 7 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (ℎ ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
29	28	com12 32	. . . . . 6 ⊢ (ℎ ∈ 𝑥 → ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
30	29	adantl 481	. . . . 5 ⊢ ((𝑡 ∈ 𝑥 ∧ ℎ ∈ 𝑥) → ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
31	30	rexlimivv 3174	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
32	19, 31	sylbir 235	. . 3 ⊢ ((∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
33	5, 18, 32	syl2anb 598	. 2 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
34	33	rgen2 3172	1 ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {cab 2709   ≠ wne 2928  ∀wral 3047  ∃wrex 3056   ∖ cdif 3899   ∩ cin 3901  ∅c0 4283  {csn 4576  ∪ cuni 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4284  df-sn 4577  df-uni 4860

This theorem is referenced by:  kmlem10  10051