This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordtt1

Description: The order topology is T_1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion ordtt1 ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ Fre )

Proof

Step Hyp Ref Expression
1 ordttop ⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ Top )
2 snssi ⊢ ( 𝑥 ∈ dom 𝑅 → { 𝑥 } ⊆ dom 𝑅 )
3 2 adantl ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑥 } ⊆ dom 𝑅 )
4 sseqin2 ⊢ ( { 𝑥 } ⊆ dom 𝑅 ↔ ( dom 𝑅 ∩ { 𝑥 } ) = { 𝑥 } )
5 3 4 sylib ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → ( dom 𝑅 ∩ { 𝑥 } ) = { 𝑥 } )
6 velsn ⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
7 eqid ⊢ dom 𝑅 = dom 𝑅
8 7 psref ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → 𝑥 𝑅 𝑥 )
9 8 adantr ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → 𝑥 𝑅 𝑥 )
10 9 9 jca ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑥 𝑅 𝑥 ∧ 𝑥 𝑅 𝑥 ) )
11 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝑥 ) )
12 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝑥 ↔ 𝑥 𝑅 𝑥 ) )
13 11 12 anbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 𝑅 𝑥 ) ) )
14 10 13 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
15 psasym ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 )
16 15 equcomd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑦 = 𝑥 )
17 16 3expib ⊢ ( 𝑅 ∈ PosetRel → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑦 = 𝑥 ) )
18 17 ad2antrr ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑦 = 𝑥 ) )
19 14 18 impbid ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑦 = 𝑥 ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
20 6 19 bitrid ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑦 ∈ { 𝑥 } ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
21 20 rabbi2dva ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → ( dom 𝑅 ∩ { 𝑥 } ) = { 𝑦 ∈ dom 𝑅 ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) } )
22 5 21 eqtr3d ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑥 } = { 𝑦 ∈ dom 𝑅 ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) } )
23 7 ordtcld3 ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑦 ∈ dom 𝑅 ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
24 23 3anidm23 ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑦 ∈ dom 𝑅 ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
25 22 24 eqeltrd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
26 25 ralrimiva ⊢ ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∈ dom 𝑅 { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
27 7 ordttopon ⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) )
28 toponuni ⊢ ( ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) → dom 𝑅 = ∪ ( ordTop ‘ 𝑅 ) )
29 27 28 syl ⊢ ( 𝑅 ∈ PosetRel → dom 𝑅 = ∪ ( ordTop ‘ 𝑅 ) )
30 26 29 raleqtrdv ⊢ ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∈ ∪ ( ordTop ‘ 𝑅 ) { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
31 eqid ⊢ ∪ ( ordTop ‘ 𝑅 ) = ∪ ( ordTop ‘ 𝑅 )
32 31 ist1 ⊢ ( ( ordTop ‘ 𝑅 ) ∈ Fre ↔ ( ( ordTop ‘ 𝑅 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( ordTop ‘ 𝑅 ) { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) ) )
33 1 30 32 sylanbrc ⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ Fre )