Metamath Proof Explorer

Theorem ordthaus

Description: The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Assertion ordthaus 
|- ( R e. TosetRel -> ( ordTop ` R ) e. Haus )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  dom R = dom R
2 1 ordthauslem 
 |-  ( ( R e. TosetRel /\ x e. dom R /\ y e. dom R ) -> ( x R y -> ( x =/= y -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
3 1 ordthauslem 
 |-  ( ( R e. TosetRel /\ y e. dom R /\ x e. dom R ) -> ( y R x -> ( y =/= x -> E. n e. ( ordTop ` R ) E. m e. ( ordTop ` R ) ( y e. n /\ x e. m /\ ( n i^i m ) = (/) ) ) ) )
4 necom 
 |-  ( y =/= x <-> x =/= y )
5 3ancoma 
 |-  ( ( y e. n /\ x e. m /\ ( n i^i m ) = (/) ) <-> ( x e. m /\ y e. n /\ ( n i^i m ) = (/) ) )
6 incom 
 |-  ( n i^i m ) = ( m i^i n )
7 6 eqeq1i 
 |-  ( ( n i^i m ) = (/) <-> ( m i^i n ) = (/) )
8 7 3anbi3i 
 |-  ( ( x e. m /\ y e. n /\ ( n i^i m ) = (/) ) <-> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
9 5 8 bitri 
 |-  ( ( y e. n /\ x e. m /\ ( n i^i m ) = (/) ) <-> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
10 9 2rexbii 
 |-  ( E. n e. ( ordTop ` R ) E. m e. ( ordTop ` R ) ( y e. n /\ x e. m /\ ( n i^i m ) = (/) ) <-> E. n e. ( ordTop ` R ) E. m e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
11 rexcom 
 |-  ( E. n e. ( ordTop ` R ) E. m e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) <-> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
12 10 11 bitri 
 |-  ( E. n e. ( ordTop ` R ) E. m e. ( ordTop ` R ) ( y e. n /\ x e. m /\ ( n i^i m ) = (/) ) <-> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
13 4 12 imbi12i 
 |-  ( ( y =/= x -> E. n e. ( ordTop ` R ) E. m e. ( ordTop ` R ) ( y e. n /\ x e. m /\ ( n i^i m ) = (/) ) ) <-> ( x =/= y -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
14 3 13 syl6ib 
 |-  ( ( R e. TosetRel /\ y e. dom R /\ x e. dom R ) -> ( y R x -> ( x =/= y -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
15 14 3com23 
 |-  ( ( R e. TosetRel /\ x e. dom R /\ y e. dom R ) -> ( y R x -> ( x =/= y -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
16 1 tsrlin 
 |-  ( ( R e. TosetRel /\ x e. dom R /\ y e. dom R ) -> ( x R y \/ y R x ) )
17 2 15 16 mpjaod 
 |-  ( ( R e. TosetRel /\ x e. dom R /\ y e. dom R ) -> ( x =/= y -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
18 17 3expb 
 |-  ( ( R e. TosetRel /\ ( x e. dom R /\ y e. dom R ) ) -> ( x =/= y -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
19 18 ralrimivva 
 |-  ( R e. TosetRel -> A. x e. dom R A. y e. dom R ( x =/= y -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
20 1 ordttopon 
 |-  ( R e. TosetRel -> ( ordTop ` R ) e. ( TopOn ` dom R ) )
21 ishaus2 
 |-  ( ( ordTop ` R ) e. ( TopOn ` dom R ) -> ( ( ordTop ` R ) e. Haus <-> A. x e. dom R A. y e. dom R ( x =/= y -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
22 20 21 syl 
 |-  ( R e. TosetRel -> ( ( ordTop ` R ) e. Haus <-> A. x e. dom R A. y e. dom R ( x =/= y -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
23 19 22 mpbird 
 |-  ( R e. TosetRel -> ( ordTop ` R ) e. Haus )