| Step | Hyp | Ref
| Expression |
| 1 | | ist1-2 23355 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Fre ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) |
| 2 | | toponmax 22932 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
| 3 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑜 = 𝑋 → (𝑥 ∈ 𝑜 ↔ 𝑥 ∈ 𝑋)) |
| 4 | 3 | intminss 4974 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑥 ∈ 𝑋) → ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} ⊆ 𝑋) |
| 5 | 2, 4 | sylan 580 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝑋) → ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} ⊆ 𝑋) |
| 6 | 5 | sselda 3983 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜}) → 𝑦 ∈ 𝑋) |
| 7 | | biimt 360 |
. . . . . 6
⊢ (𝑦 ∈ 𝑋 → (𝑦 ∈ {𝑥} ↔ (𝑦 ∈ 𝑋 → 𝑦 ∈ {𝑥}))) |
| 8 | 6, 7 | syl 17 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜}) → (𝑦 ∈ {𝑥} ↔ (𝑦 ∈ 𝑋 → 𝑦 ∈ {𝑥}))) |
| 9 | 8 | ralbidva 3176 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝑋) → (∀𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜}𝑦 ∈ {𝑥} ↔ ∀𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} (𝑦 ∈ 𝑋 → 𝑦 ∈ {𝑥}))) |
| 10 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑜) |
| 11 | 10 | rgenw 3065 |
. . . . . . . 8
⊢
∀𝑜 ∈
𝐽 (𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑜) |
| 12 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 13 | 12 | elintrab 4960 |
. . . . . . . 8
⊢ (𝑥 ∈ ∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} ↔ ∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑜)) |
| 14 | 11, 13 | mpbir 231 |
. . . . . . 7
⊢ 𝑥 ∈ ∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} |
| 15 | | snssi 4808 |
. . . . . . 7
⊢ (𝑥 ∈ ∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} → {𝑥} ⊆ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜}) |
| 16 | 14, 15 | ax-mp 5 |
. . . . . 6
⊢ {𝑥} ⊆ ∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} |
| 17 | | eqss 3999 |
. . . . . 6
⊢ (∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} = {𝑥} ↔ (∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} ⊆ {𝑥} ∧ {𝑥} ⊆ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜})) |
| 18 | 16, 17 | mpbiran2 710 |
. . . . 5
⊢ (∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} = {𝑥} ↔ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} ⊆ {𝑥}) |
| 19 | | dfss3 3972 |
. . . . 5
⊢ (∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} ⊆ {𝑥} ↔ ∀𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜}𝑦 ∈ {𝑥}) |
| 20 | 18, 19 | bitri 275 |
. . . 4
⊢ (∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} = {𝑥} ↔ ∀𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜}𝑦 ∈ {𝑥}) |
| 21 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 22 | 21 | elintrab 4960 |
. . . . . . 7
⊢ (𝑦 ∈ ∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} ↔ ∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜)) |
| 23 | | velsn 4642 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥) |
| 24 | | equcom 2017 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
| 25 | 23, 24 | bitri 275 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥} ↔ 𝑥 = 𝑦) |
| 26 | 22, 25 | imbi12i 350 |
. . . . . 6
⊢ ((𝑦 ∈ ∩ {𝑜
∈ 𝐽 ∣ 𝑥 ∈ 𝑜} → 𝑦 ∈ {𝑥}) ↔ (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)) |
| 27 | 26 | ralbii 3093 |
. . . . 5
⊢
(∀𝑦 ∈
𝑋 (𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} → 𝑦 ∈ {𝑥}) ↔ ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)) |
| 28 | | ralcom3 3097 |
. . . . 5
⊢
(∀𝑦 ∈
𝑋 (𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} → 𝑦 ∈ {𝑥}) ↔ ∀𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} (𝑦 ∈ 𝑋 → 𝑦 ∈ {𝑥})) |
| 29 | 27, 28 | bitr3i 277 |
. . . 4
⊢
(∀𝑦 ∈
𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} (𝑦 ∈ 𝑋 → 𝑦 ∈ {𝑥})) |
| 30 | 9, 20, 29 | 3bitr4g 314 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝑋) → (∩
{𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} = {𝑥} ↔ ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) |
| 31 | 30 | ralbidva 3176 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝑋 ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} = {𝑥} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) |
| 32 | 1, 31 | bitr4d 282 |
1
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Fre ↔ ∀𝑥 ∈ 𝑋 ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} = {𝑥})) |