| Step | Hyp | Ref
| Expression |
| 1 | | an4 656 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽) ∧ (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦)) ↔ ((𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥) ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦))) |
| 2 | | nnuz 12921 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
| 3 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥) |
| 4 | | 1zzd 12648 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → 1 ∈ ℤ) |
| 5 | | lmmo.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐴) |
| 6 | 5 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → 𝐹(⇝𝑡‘𝐽)𝐴) |
| 7 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → 𝑥 ∈ 𝐽) |
| 8 | 2, 3, 4, 6, 7 | lmcvg 23270 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥) |
| 9 | 8 | ex 412 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥)) |
| 10 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → 𝐵 ∈ 𝑦) |
| 11 | | 1zzd 12648 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → 1 ∈ ℤ) |
| 12 | | lmmo.5 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐵) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → 𝐹(⇝𝑡‘𝐽)𝐵) |
| 14 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → 𝑦 ∈ 𝐽) |
| 15 | 2, 10, 11, 13, 14 | lmcvg 23270 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦) |
| 16 | 15 | ex 412 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦)) |
| 17 | 9, 16 | anim12d 609 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥) ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦))) |
| 18 | 2 | rexanuz2 15388 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦) ↔ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦)) |
| 19 | | nnz 12634 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
| 20 | | uzid 12893 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
| 21 | | ne0i 4341 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (ℤ≥‘𝑗) ≠ ∅) |
| 22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ →
(ℤ≥‘𝑗) ≠ ∅) |
| 23 | | r19.2z 4495 |
. . . . . . . . . . . . . 14
⊢
(((ℤ≥‘𝑗) ≠ ∅ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) → ∃𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) |
| 24 | | elin 3967 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘) ∈ (𝑥 ∩ 𝑦) ↔ ((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) |
| 25 | | n0i 4340 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘) ∈ (𝑥 ∩ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
| 26 | 24, 25 | sylbir 235 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
| 27 | 26 | rexlimivw 3151 |
. . . . . . . . . . . . . 14
⊢
(∃𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
| 28 | 23, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((ℤ≥‘𝑗) ≠ ∅ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) → ¬ (𝑥 ∩ 𝑦) = ∅) |
| 29 | 22, 28 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℕ ∧
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) → ¬ (𝑥 ∩ 𝑦) = ∅) |
| 30 | 29 | rexlimiva 3147 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
| 31 | 18, 30 | sylbir 235 |
. . . . . . . . . 10
⊢
((∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
| 32 | 17, 31 | syl6 35 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥) ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → ¬ (𝑥 ∩ 𝑦) = ∅)) |
| 33 | 1, 32 | biimtrid 242 |
. . . . . . . 8
⊢ (𝜑 → (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽) ∧ (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦)) → ¬ (𝑥 ∩ 𝑦) = ∅)) |
| 34 | 33 | expdimp 452 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅)) |
| 35 | | imnan 399 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) ↔ ¬ ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) ∧ (𝑥 ∩ 𝑦) = ∅)) |
| 36 | 34, 35 | sylib 218 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ¬ ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) ∧ (𝑥 ∩ 𝑦) = ∅)) |
| 37 | | df-3an 1089 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅) ↔ ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) ∧ (𝑥 ∩ 𝑦) = ∅)) |
| 38 | 36, 37 | sylnibr 329 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ¬ (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
| 39 | 38 | anassrs 467 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ 𝐽) → ¬ (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
| 40 | 39 | nrexdv 3149 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → ¬ ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
| 41 | 40 | nrexdv 3149 |
. 2
⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
| 42 | | lmmo.1 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ Haus) |
| 43 | | haustop 23339 |
. . . . . . 7
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
| 44 | 42, 43 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Top) |
| 45 | | toptopon2 22924 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 46 | 44, 45 | sylib 218 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 47 | | lmcl 23305 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐹(⇝𝑡‘𝐽)𝐴) → 𝐴 ∈ ∪ 𝐽) |
| 48 | 46, 5, 47 | syl2anc 584 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ∪ 𝐽) |
| 49 | | lmcl 23305 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐹(⇝𝑡‘𝐽)𝐵) → 𝐵 ∈ ∪ 𝐽) |
| 50 | 46, 12, 49 | syl2anc 584 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ∪ 𝐽) |
| 51 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 52 | 51 | hausnei 23336 |
. . . . 5
⊢ ((𝐽 ∈ Haus ∧ (𝐴 ∈ ∪ 𝐽
∧ 𝐵 ∈ ∪ 𝐽
∧ 𝐴 ≠ 𝐵)) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
| 53 | 52 | 3exp2 1355 |
. . . 4
⊢ (𝐽 ∈ Haus → (𝐴 ∈ ∪ 𝐽
→ (𝐵 ∈ ∪ 𝐽
→ (𝐴 ≠ 𝐵 → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))))) |
| 54 | 42, 48, 50, 53 | syl3c 66 |
. . 3
⊢ (𝜑 → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))) |
| 55 | 54 | necon1bd 2958 |
. 2
⊢ (𝜑 → (¬ ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅) → 𝐴 = 𝐵)) |
| 56 | 41, 55 | mpd 15 |
1
⊢ (𝜑 → 𝐴 = 𝐵) |