| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 2 | 1 | hausnei 23336 | . . . . . . . 8
⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) → ∃𝑧 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅)) | 
| 3 |  | simprr1 1222 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) ∧ 𝑧 ∈ 𝐽) ∧ (𝑤 ∈ 𝐽 ∧ (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))) → 𝑥 ∈ 𝑧) | 
| 4 |  | noel 4338 | . . . . . . . . . . . . 13
⊢  ¬
𝑦 ∈
∅ | 
| 5 |  | simprr3 1224 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) ∧ 𝑧 ∈ 𝐽) ∧ (𝑤 ∈ 𝐽 ∧ (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))) → (𝑧 ∩ 𝑤) = ∅) | 
| 6 | 5 | eleq2d 2827 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) ∧ 𝑧 ∈ 𝐽) ∧ (𝑤 ∈ 𝐽 ∧ (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))) → (𝑦 ∈ (𝑧 ∩ 𝑤) ↔ 𝑦 ∈ ∅)) | 
| 7 | 4, 6 | mtbiri 327 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) ∧ 𝑧 ∈ 𝐽) ∧ (𝑤 ∈ 𝐽 ∧ (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))) → ¬ 𝑦 ∈ (𝑧 ∩ 𝑤)) | 
| 8 |  | simprr2 1223 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) ∧ 𝑧 ∈ 𝐽) ∧ (𝑤 ∈ 𝐽 ∧ (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))) → 𝑦 ∈ 𝑤) | 
| 9 |  | elin 3967 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝑧 ∩ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤)) | 
| 10 | 9 | simplbi2com 502 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑤 → (𝑦 ∈ 𝑧 → 𝑦 ∈ (𝑧 ∩ 𝑤))) | 
| 11 | 8, 10 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) ∧ 𝑧 ∈ 𝐽) ∧ (𝑤 ∈ 𝐽 ∧ (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))) → (𝑦 ∈ 𝑧 → 𝑦 ∈ (𝑧 ∩ 𝑤))) | 
| 12 | 7, 11 | mtod 198 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) ∧ 𝑧 ∈ 𝐽) ∧ (𝑤 ∈ 𝐽 ∧ (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))) → ¬ 𝑦 ∈ 𝑧) | 
| 13 | 3, 12 | jca 511 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) ∧ 𝑧 ∈ 𝐽) ∧ (𝑤 ∈ 𝐽 ∧ (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))) → (𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧)) | 
| 14 | 13 | rexlimdvaa 3156 | . . . . . . . . 9
⊢ (((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) ∧ 𝑧 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧))) | 
| 15 | 14 | reximdva 3168 | . . . . . . . 8
⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) → (∃𝑧 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅) → ∃𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧))) | 
| 16 | 2, 15 | mpd 15 | . . . . . . 7
⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) → ∃𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧)) | 
| 17 |  | rexanali 3102 | . . . . . . 7
⊢
(∃𝑧 ∈
𝐽 (𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧) ↔ ¬ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | 
| 18 | 16, 17 | sylib 218 | . . . . . 6
⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽
∧ 𝑥 ≠ 𝑦)) → ¬ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | 
| 19 | 18 | 3exp2 1355 | . . . . 5
⊢ (𝐽 ∈ Haus → (𝑥 ∈ ∪ 𝐽
→ (𝑦 ∈ ∪ 𝐽
→ (𝑥 ≠ 𝑦 → ¬ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))))) | 
| 20 | 19 | imp32 418 | . . . 4
⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽))
→ (𝑥 ≠ 𝑦 → ¬ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))) | 
| 21 | 20 | necon4ad 2959 | . . 3
⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑦 ∈ ∪ 𝐽))
→ (∀𝑧 ∈
𝐽 (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧) → 𝑥 = 𝑦)) | 
| 22 | 21 | ralrimivva 3202 | . 2
⊢ (𝐽 ∈ Haus →
∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧) → 𝑥 = 𝑦)) | 
| 23 |  | haustop 23339 | . . . 4
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) | 
| 24 |  | toptopon2 22924 | . . . 4
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 25 | 23, 24 | sylib 218 | . . 3
⊢ (𝐽 ∈ Haus → 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 26 |  | ist1-2 23355 | . . 3
⊢ (𝐽 ∈ (TopOn‘∪ 𝐽)
→ (𝐽 ∈ Fre ↔
∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧) → 𝑥 = 𝑦))) | 
| 27 | 25, 26 | syl 17 | . 2
⊢ (𝐽 ∈ Haus → (𝐽 ∈ Fre ↔ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧) → 𝑥 = 𝑦))) | 
| 28 | 22, 27 | mpbird 257 | 1
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Fre) |