Theorem kmlem9 10152

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 3478	. . . 4 ⊢ 𝑧 ∈ V
2		eqeq1 2736	. . . . 5 ⊢ (𝑢 = 𝑧 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
3	2	rexbidv 3178	. . . 4 ⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
4		kmlem9.1	. . . 4 ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}
5	1, 3, 4	elab2 3672	. . 3 ⊢ (𝑧 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
6		vex 3478	. . . . 5 ⊢ 𝑤 ∈ V
7		eqeq1 2736	. . . . . 6 ⊢ (𝑢 = 𝑤 → (𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
8	7	rexbidv 3178	. . . . 5 ⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))))
9	6, 8, 4	elab2 3672	. . . 4 ⊢ (𝑤 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))
10		difeq1 4115	. . . . . . 7 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {𝑡})))
11		sneq 4638	. . . . . . . . . 10 ⊢ (𝑡 = ℎ → {𝑡} = {ℎ})
12	11	difeq2d 4122	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {ℎ}))
13	12	unieqd 4922	. . . . . . . 8 ⊢ (𝑡 = ℎ → ∪ (𝑥 ∖ {𝑡}) = ∪ (𝑥 ∖ {ℎ}))
14	13	difeq2d 4122	. . . . . . 7 ⊢ (𝑡 = ℎ → (ℎ ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
15	10, 14	eqtrd 2772	. . . . . 6 ⊢ (𝑡 = ℎ → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
16	15	eqeq2d 2743	. . . . 5 ⊢ (𝑡 = ℎ → (𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
17	16	cbvrexvw 3235	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 𝑤 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
18	9, 17	bitri 274	. . 3 ⊢ (𝑤 ∈ 𝐴 ↔ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ})))
19		reeanv 3226	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) ↔ (∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
20		eqeq12 2749	. . . . . . . . . 10 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 = 𝑤 ↔ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
21	15, 20	imbitrrid 245	. . . . . . . . 9 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑡 = ℎ → 𝑧 = 𝑤))
22	21	necon3d 2961	. . . . . . . 8 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → 𝑡 ≠ ℎ))
23		kmlem5 10148	. . . . . . . . . 10 ⊢ ((ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ) → ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) = ∅)
24		ineq12 4207	. . . . . . . . . . 11 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ∩ 𝑤) = ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))))
25	24	eqeq1d 2734	. . . . . . . . . 10 ⊢ ((𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → ((𝑧 ∩ 𝑤) = ∅ ↔ ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) = ∅))
26	23, 25	imbitrrid 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 3199	. . . 4 ⊢ (∃𝑡 ∈ 𝑥 ∃ℎ ∈ 𝑥 (𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
32	19, 31	sylbir 234	. . 3 ⊢ ((∃𝑡 ∈ 𝑥 𝑧 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∧ ∃ℎ ∈ 𝑥 𝑤 = (ℎ ∖ ∪ (𝑥 ∖ {ℎ}))) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
33	5, 18, 32	syl2anb 598	. 2 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))
34	33	rgen2 3197	1 ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2709   ≠ wne 2940  ∀wral 3061  ∃wrex 3070   ∖ cdif 3945   ∩ cin 3947  ∅c0 4322  {csn 4628  ∪ cuni 4908

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 2703

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 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965  df-nul 4323  df-sn 4629  df-uni 4909

This theorem is referenced by:  kmlem10  10153