Step | Hyp | Ref
| Expression |
1 | | ist0.1 |
. . . . . . 7
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | ishaus 22473 |
. . . . . 6
⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
3 | 2 | simprbi 497 |
. . . . 5
⊢ (𝐽 ∈ Haus →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))) |
4 | | neeq1 3006 |
. . . . . . 7
⊢ (𝑥 = 𝑃 → (𝑥 ≠ 𝑦 ↔ 𝑃 ≠ 𝑦)) |
5 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑥 = 𝑃 → (𝑥 ∈ 𝑛 ↔ 𝑃 ∈ 𝑛)) |
6 | 5 | 3anbi1d 1439 |
. . . . . . . 8
⊢ (𝑥 = 𝑃 → ((𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) ↔ (𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))) |
7 | 6 | 2rexbidv 3229 |
. . . . . . 7
⊢ (𝑥 = 𝑃 → (∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) ↔ ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))) |
8 | 4, 7 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑃 → ((𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) ↔ (𝑃 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
9 | | neeq2 3007 |
. . . . . . 7
⊢ (𝑦 = 𝑄 → (𝑃 ≠ 𝑦 ↔ 𝑃 ≠ 𝑄)) |
10 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑦 = 𝑄 → (𝑦 ∈ 𝑚 ↔ 𝑄 ∈ 𝑚)) |
11 | 10 | 3anbi2d 1440 |
. . . . . . . 8
⊢ (𝑦 = 𝑄 → ((𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) ↔ (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))) |
12 | 11 | 2rexbidv 3229 |
. . . . . . 7
⊢ (𝑦 = 𝑄 → (∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) ↔ ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))) |
13 | 9, 12 | imbi12d 345 |
. . . . . 6
⊢ (𝑦 = 𝑄 → ((𝑃 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) ↔ (𝑃 ≠ 𝑄 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
14 | 8, 13 | rspc2v 3570 |
. . . . 5
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝑃 ≠ 𝑄 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
15 | 3, 14 | syl5 34 |
. . . 4
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) → (𝐽 ∈ Haus → (𝑃 ≠ 𝑄 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
16 | 15 | ex 413 |
. . 3
⊢ (𝑃 ∈ 𝑋 → (𝑄 ∈ 𝑋 → (𝐽 ∈ Haus → (𝑃 ≠ 𝑄 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))) |
17 | 16 | com3r 87 |
. 2
⊢ (𝐽 ∈ Haus → (𝑃 ∈ 𝑋 → (𝑄 ∈ 𝑋 → (𝑃 ≠ 𝑄 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))) |
18 | 17 | 3imp2 1348 |
1
⊢ ((𝐽 ∈ Haus ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑃 ≠ 𝑄)) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) |