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 )