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
|- ( R e. PosetRel -> ( ordTop ` R ) e. Fre )

Proof

Step Hyp Ref Expression
1 ordttop
 |-  ( R e. PosetRel -> ( ordTop ` R ) e. Top )
2 snssi
 |-  ( x e. dom R -> { x } C_ dom R )
3 2 adantl
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> { x } C_ dom R )
4 sseqin2
 |-  ( { x } C_ dom R <-> ( dom R i^i { x } ) = { x } )
5 3 4 sylib
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> ( dom R i^i { x } ) = { x } )
6 velsn
 |-  ( y e. { x } <-> y = x )
7 eqid
 |-  dom R = dom R
8 7 psref
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> x R x )
9 8 adantr
 |-  ( ( ( R e. PosetRel /\ x e. dom R ) /\ y e. dom R ) -> x R x )
10 9 9 jca
 |-  ( ( ( R e. PosetRel /\ x e. dom R ) /\ y e. dom R ) -> ( x R x /\ x R x ) )
11 breq2
 |-  ( y = x -> ( x R y <-> x R x ) )
12 breq1
 |-  ( y = x -> ( y R x <-> x R x ) )
13 11 12 anbi12d
 |-  ( y = x -> ( ( x R y /\ y R x ) <-> ( x R x /\ x R x ) ) )
14 10 13 syl5ibrcom
 |-  ( ( ( R e. PosetRel /\ x e. dom R ) /\ y e. dom R ) -> ( y = x -> ( x R y /\ y R x ) ) )
15 psasym
 |-  ( ( R e. PosetRel /\ x R y /\ y R x ) -> x = y )
16 15 equcomd
 |-  ( ( R e. PosetRel /\ x R y /\ y R x ) -> y = x )
17 16 3expib
 |-  ( R e. PosetRel -> ( ( x R y /\ y R x ) -> y = x ) )
18 17 ad2antrr
 |-  ( ( ( R e. PosetRel /\ x e. dom R ) /\ y e. dom R ) -> ( ( x R y /\ y R x ) -> y = x ) )
19 14 18 impbid
 |-  ( ( ( R e. PosetRel /\ x e. dom R ) /\ y e. dom R ) -> ( y = x <-> ( x R y /\ y R x ) ) )
20 6 19 syl5bb
 |-  ( ( ( R e. PosetRel /\ x e. dom R ) /\ y e. dom R ) -> ( y e. { x } <-> ( x R y /\ y R x ) ) )
21 20 rabbi2dva
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> ( dom R i^i { x } ) = { y e. dom R | ( x R y /\ y R x ) } )
22 5 21 eqtr3d
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> { x } = { y e. dom R | ( x R y /\ y R x ) } )
23 7 ordtcld3
 |-  ( ( R e. PosetRel /\ x e. dom R /\ x e. dom R ) -> { y e. dom R | ( x R y /\ y R x ) } e. ( Clsd ` ( ordTop ` R ) ) )
24 23 3anidm23
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> { y e. dom R | ( x R y /\ y R x ) } e. ( Clsd ` ( ordTop ` R ) ) )
25 22 24 eqeltrd
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> { x } e. ( Clsd ` ( ordTop ` R ) ) )
26 25 ralrimiva
 |-  ( R e. PosetRel -> A. x e. dom R { x } e. ( Clsd ` ( ordTop ` R ) ) )
27 7 ordttopon
 |-  ( R e. PosetRel -> ( ordTop ` R ) e. ( TopOn ` dom R ) )
28 toponuni
 |-  ( ( ordTop ` R ) e. ( TopOn ` dom R ) -> dom R = U. ( ordTop ` R ) )
29 27 28 syl
 |-  ( R e. PosetRel -> dom R = U. ( ordTop ` R ) )
30 29 raleqdv
 |-  ( R e. PosetRel -> ( A. x e. dom R { x } e. ( Clsd ` ( ordTop ` R ) ) <-> A. x e. U. ( ordTop ` R ) { x } e. ( Clsd ` ( ordTop ` R ) ) ) )
31 26 30 mpbid
 |-  ( R e. PosetRel -> A. x e. U. ( ordTop ` R ) { x } e. ( Clsd ` ( ordTop ` R ) ) )
32 eqid
 |-  U. ( ordTop ` R ) = U. ( ordTop ` R )
33 32 ist1
 |-  ( ( ordTop ` R ) e. Fre <-> ( ( ordTop ` R ) e. Top /\ A. x e. U. ( ordTop ` R ) { x } e. ( Clsd ` ( ordTop ` R ) ) ) )
34 1 31 33 sylanbrc
 |-  ( R e. PosetRel -> ( ordTop ` R ) e. Fre )