Theorem kmlem9 10094

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 3449	. . . 4 ⊢ 𝑧 ∈ V
2		eqeq1 2740	. . . . 5 ⊢ (𝑢 = 𝑧 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
3	2	rexbidv 3175	. . . 4 ⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
4		kmlem9.1	. . . 4 ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}
5	1, 3, 4	elab2 3634	. . 3 ⊢ (𝑧 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
6		vex 3449	. . . . 5 ⊢ 𝑤 ∈ V
7		eqeq1 2740	. . . . . 6 ⊢ (𝑢 = 𝑤 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
8	7	rexbidv 3175	. . . . 5 ⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
9	6, 8, 4	elab2 3634	. . . 4 ⊢ (𝑤 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
10		difeq1 4075	. . . . . . 7 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {𝑡})))
11		sneq 4596	. . . . . . . . . 10 ⊢ (𝑡 = ℎ → {𝑡} = {ℎ})
12	11	difeq2d 4082	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {ℎ}))
13	12	unieqd 4879	. . . . . . . 8 ⊢ (𝑡 = ℎ → ∪ (𝑥 ∖ {𝑡}) = ∪ (𝑥 ∖ {ℎ}))
14	13	difeq2d 4082	. . . . . . 7 ⊢ (𝑡 = ℎ → (ℎ ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
15	10, 14	eqtrd 2776	. . . . . 6 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
16	15	eqeq2d 2747	. . . . 5 ⊢ (𝑡 = ℎ → (𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
17	16	cbvrexvw 3226	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
18	9, 17	bitri 274	. . 3 ⊢ (𝑤 ∈ 𝐴 ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
19		reeanv 3217	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) ↔ (∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
20		eqeq12 2753	. . . . . . . . . 10 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 = 𝑤 ↔ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
21	15, 20	syl5ibr 245	. . . . . . . . 9 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑡 = ℎ → 𝑧 = 𝑤))
22	21	necon3d 2964	. . . . . . . 8 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → 𝑡 ≠ ℎ))
23		kmlem5 10090	. . . . . . . . . 10 ⊢ ((ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ) → ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) = ∅)
24		ineq12 4167	. . . . . . . . . . 11 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ∩ 𝑤) = ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
25	24	eqeq1d 2738	. . . . . . . . . 10 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → ((𝑧 ∩ 𝑤) = ∅ ↔ ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) = ∅))
26	23, 25	syl5ibr 245	. . . . . . . . 9 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → ((ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ) → (𝑧 ∩ 𝑤) = ∅))
27	26	expd 416	. . . . . . . 8 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (ℎ ∈ 𝑥 → (𝑡 ≠ ℎ → (𝑧 ∩ 𝑤) = ∅)))
28	22, 27	syl5d 73	. . . . . . 7 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (ℎ ∈ 𝑥 → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
29	28	com12 32	. . . . . 6 ⊢ (ℎ ∈ 𝑥 → ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
30	29	adantl 482	. . . . 5 ⊢ ((𝑡 ∈ 𝑥 ∧ ℎ ∈ 𝑥) → ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))
31	30	rexlimivv 3196	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
32	19, 31	sylbir 234	. . 3 ⊢ ((∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
33	5, 18, 32	syl2anb 598	. 2 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
34	33	rgen2 3194	1 ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2713   ≠ wne 2943  ∀wral 3064  ∃wrex 3073   ∖ cdif 3907   ∩ cin 3909  ∅c0 4282  {csn 4586  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-in 3917  df-ss 3927  df-nul 4283  df-sn 4587  df-uni 4866

This theorem is referenced by:  kmlem10  10095