This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem kmlem9

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

Ref Expression
Hypothesis kmlem9.1 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
Assertion kmlem9 ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ )

Proof

Step Hyp Ref Expression
1 kmlem9.1 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
2 vex ⊢ 𝑧 ∈ V
3 eqeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
4 3 rexbidv ⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
5 2 4 1 elab2 ⊢ ( 𝑧 ∈ 𝐴 ↔ ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
6 vex ⊢ 𝑤 ∈ V
7 eqeq1 ⊢ ( 𝑢 = 𝑤 → ( 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
8 7 rexbidv ⊢ ( 𝑢 = 𝑤 → ( ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ ∃ 𝑡 ∈ 𝑥 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
9 6 8 1 elab2 ⊢ ( 𝑤 ∈ 𝐴 ↔ ∃ 𝑡 ∈ 𝑥 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
10 difeq1 ⊢ ( 𝑡 = ℎ → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( ℎ ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
11 sneq ⊢ ( 𝑡 = ℎ → { 𝑡 } = { ℎ } )
12 11 difeq2d ⊢ ( 𝑡 = ℎ → ( 𝑥 ∖ { 𝑡 } ) = ( 𝑥 ∖ { ℎ } ) )
13 12 unieqd ⊢ ( 𝑡 = ℎ → ∪ ( 𝑥 ∖ { 𝑡 } ) = ∪ ( 𝑥 ∖ { ℎ } ) )
14 13 difeq2d ⊢ ( 𝑡 = ℎ → ( ℎ ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) )
15 10 14 eqtrd ⊢ ( 𝑡 = ℎ → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) )
16 15 eqeq2d ⊢ ( 𝑡 = ℎ → ( 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) )
17 16 cbvrexvw ⊢ ( ∃ 𝑡 ∈ 𝑥 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ ∃ ℎ ∈ 𝑥 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) )
18 9 17 bitri ⊢ ( 𝑤 ∈ 𝐴 ↔ ∃ ℎ ∈ 𝑥 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) )
19 reeanv ⊢ ( ∃ 𝑡 ∈ 𝑥 ∃ ℎ ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) ↔ ( ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ ∃ ℎ ∈ 𝑥 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) )
20 eqeq12 ⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 = 𝑤 ↔ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) )
21 15 20 imbitrrid ⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑡 = ℎ → 𝑧 = 𝑤 ) )
22 21 necon3d ⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → 𝑡 ≠ ℎ ) )
23 kmlem5 ⊢ ( ( ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ ) → ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) = ∅ )
24 ineq12 ⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ∩ 𝑤 ) = ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) )
25 24 eqeq1d ⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( ( 𝑧 ∩ 𝑤 ) = ∅ ↔ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) = ∅ ) )
26 23 25 imbitrrid ⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( ( ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ ) → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
27 26 expd ⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( ℎ ∈ 𝑥 → ( 𝑡 ≠ ℎ → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
28 22 27 syl5d ⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( ℎ ∈ 𝑥 → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
29 28 com12 ⊢ ( ℎ ∈ 𝑥 → ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
30 29 adantl ⊢ ( ( 𝑡 ∈ 𝑥 ∧ ℎ ∈ 𝑥 ) → ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
31 30 rexlimivv ⊢ ( ∃ 𝑡 ∈ 𝑥 ∃ ℎ ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
32 19 31 sylbir ⊢ ( ( ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ ∃ ℎ ∈ 𝑥 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
33 5 18 32 syl2anb ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
34 33 rgen2 ⊢ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ )