Theorem kmlem9 10228

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 3492	. . . 4 ⊢ 𝑧 ∈ V
2		eqeq1 2744	. . . . 5 ⊢ (𝑢 = 𝑧 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
3	2	rexbidv 3185	. . . 4 ⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
4		kmlem9.1	. . . 4 ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}
5	1, 3, 4	elab2 3698	. . 3 ⊢ (𝑧 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
6		vex 3492	. . . . 5 ⊢ 𝑤 ∈ V
7		eqeq1 2744	. . . . . 6 ⊢ (𝑢 = 𝑤 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
8	7	rexbidv 3185	. . . . 5 ⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
9	6, 8, 4	elab2 3698	. . . 4 ⊢ (𝑤 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
10		difeq1 4142	. . . . . . 7 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {𝑡})))
11		sneq 4658	. . . . . . . . . 10 ⊢ (𝑡 = ℎ → {𝑡} = {ℎ})
12	11	difeq2d 4149	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {ℎ}))
13	12	unieqd 4944	. . . . . . . 8 ⊢ (𝑡 = ℎ → ∪ (𝑥 ∖ {𝑡}) = ∪ (𝑥 ∖ {ℎ}))
14	13	difeq2d 4149	. . . . . . 7 ⊢ (𝑡 = ℎ → (ℎ ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
15	10, 14	eqtrd 2780	. . . . . 6 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
16	15	eqeq2d 2751	. . . . 5 ⊢ (𝑡 = ℎ → (𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
17	16	cbvrexvw 3244	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
18	9, 17	bitri 275	. . 3 ⊢ (𝑤 ∈ 𝐴 ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
19		reeanv 3235	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) ↔ (∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
20		eqeq12 2757	. . . . . . . . . 10 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 = 𝑤 ↔ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
21	15, 20	imbitrrid 246	. . . . . . . . 9 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑡 = ℎ → 𝑧 = 𝑤))
22	21	necon3d 2967	. . . . . . . 8 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → 𝑡 ≠ ℎ))
23		kmlem5 10224	. . . . . . . . . 10 ⊢ ((ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ) → ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) = ∅)
24		ineq12 4236	. . . . . . . . . . 11 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ∩ 𝑤) = ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
25	24	eqeq1d 2742	. . . . . . . . . 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 3207	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
32	19, 31	sylbir 235	. . 3 ⊢ ((∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
33	5, 18, 32	syl2anb 597	. 2 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
34	33	rgen2 3205	1 ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {cab 2717   ≠ wne 2946  ∀wral 3067  ∃wrex 3076   ∖ cdif 3973   ∩ cin 3975  ∅c0 4352  {csn 4648  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-in 3983  df-ss 3993  df-nul 4353  df-sn 4649  df-uni 4932

This theorem is referenced by:  kmlem10  10229