| Step | Hyp | Ref
| Expression |
| 1 | | ordttop 23208 |
. 2
⊢ (𝑅 ∈ PosetRel →
(ordTop‘𝑅) ∈
Top) |
| 2 | | snssi 4808 |
. . . . . . . 8
⊢ (𝑥 ∈ dom 𝑅 → {𝑥} ⊆ dom 𝑅) |
| 3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → {𝑥} ⊆ dom 𝑅) |
| 4 | | sseqin2 4223 |
. . . . . . 7
⊢ ({𝑥} ⊆ dom 𝑅 ↔ (dom 𝑅 ∩ {𝑥}) = {𝑥}) |
| 5 | 3, 4 | sylib 218 |
. . . . . 6
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → (dom 𝑅 ∩ {𝑥}) = {𝑥}) |
| 6 | | velsn 4642 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥) |
| 7 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ dom 𝑅 = dom 𝑅 |
| 8 | 7 | psref 18619 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → 𝑥𝑅𝑥) |
| 9 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) ∧ 𝑦 ∈ dom 𝑅) → 𝑥𝑅𝑥) |
| 10 | 9, 9 | jca 511 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) ∧ 𝑦 ∈ dom 𝑅) → (𝑥𝑅𝑥 ∧ 𝑥𝑅𝑥)) |
| 11 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑥)) |
| 12 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦𝑅𝑥 ↔ 𝑥𝑅𝑥)) |
| 13 | 11, 12 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑥 ∧ 𝑥𝑅𝑥))) |
| 14 | 10, 13 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ (((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) ∧ 𝑦 ∈ dom 𝑅) → (𝑦 = 𝑥 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))) |
| 15 | | psasym 18621 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) |
| 16 | 15 | equcomd 2018 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑦 = 𝑥) |
| 17 | 16 | 3expib 1123 |
. . . . . . . . . 10
⊢ (𝑅 ∈ PosetRel → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑦 = 𝑥)) |
| 18 | 17 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) ∧ 𝑦 ∈ dom 𝑅) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑦 = 𝑥)) |
| 19 | 14, 18 | impbid 212 |
. . . . . . . 8
⊢ (((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) ∧ 𝑦 ∈ dom 𝑅) → (𝑦 = 𝑥 ↔ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))) |
| 20 | 6, 19 | bitrid 283 |
. . . . . . 7
⊢ (((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) ∧ 𝑦 ∈ dom 𝑅) → (𝑦 ∈ {𝑥} ↔ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))) |
| 21 | 20 | rabbi2dva 4226 |
. . . . . 6
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → (dom 𝑅 ∩ {𝑥}) = {𝑦 ∈ dom 𝑅 ∣ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)}) |
| 22 | 5, 21 | eqtr3d 2779 |
. . . . 5
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → {𝑥} = {𝑦 ∈ dom 𝑅 ∣ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)}) |
| 23 | 7 | ordtcld3 23207 |
. . . . . 6
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ∧ 𝑥 ∈ dom 𝑅) → {𝑦 ∈ dom 𝑅 ∣ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)} ∈ (Clsd‘(ordTop‘𝑅))) |
| 24 | 23 | 3anidm23 1423 |
. . . . 5
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → {𝑦 ∈ dom 𝑅 ∣ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)} ∈ (Clsd‘(ordTop‘𝑅))) |
| 25 | 22, 24 | eqeltrd 2841 |
. . . 4
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → {𝑥} ∈ (Clsd‘(ordTop‘𝑅))) |
| 26 | 25 | ralrimiva 3146 |
. . 3
⊢ (𝑅 ∈ PosetRel →
∀𝑥 ∈ dom 𝑅{𝑥} ∈ (Clsd‘(ordTop‘𝑅))) |
| 27 | 7 | ordttopon 23201 |
. . . 4
⊢ (𝑅 ∈ PosetRel →
(ordTop‘𝑅) ∈
(TopOn‘dom 𝑅)) |
| 28 | | toponuni 22920 |
. . . 4
⊢
((ordTop‘𝑅)
∈ (TopOn‘dom 𝑅)
→ dom 𝑅 = ∪ (ordTop‘𝑅)) |
| 29 | 27, 28 | syl 17 |
. . 3
⊢ (𝑅 ∈ PosetRel → dom
𝑅 = ∪ (ordTop‘𝑅)) |
| 30 | 26, 29 | raleqtrdv 3328 |
. 2
⊢ (𝑅 ∈ PosetRel →
∀𝑥 ∈ ∪ (ordTop‘𝑅){𝑥} ∈ (Clsd‘(ordTop‘𝑅))) |
| 31 | | eqid 2737 |
. . 3
⊢ ∪ (ordTop‘𝑅) = ∪
(ordTop‘𝑅) |
| 32 | 31 | ist1 23329 |
. 2
⊢
((ordTop‘𝑅)
∈ Fre ↔ ((ordTop‘𝑅) ∈ Top ∧ ∀𝑥 ∈ ∪ (ordTop‘𝑅){𝑥} ∈ (Clsd‘(ordTop‘𝑅)))) |
| 33 | 1, 30, 32 | sylanbrc 583 |
1
⊢ (𝑅 ∈ PosetRel →
(ordTop‘𝑅) ∈
Fre) |