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∈TosetRel→ordTop⁡R∈Haus

Proof

Step Hyp Ref Expression
1 eqid ⊢dom⁡R=dom⁡R
2 1 ordthauslem ⊢R∈TosetRel∧x∈dom⁡R∧y∈dom⁡R→xRy→x≠y→∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
3 1 ordthauslem ⊢R∈TosetRel∧y∈dom⁡R∧x∈dom⁡R→yRx→y≠x→∃n∈ordTop⁡R∃m∈ordTop⁡Ry∈n∧x∈m∧n∩m=∅
4 necom ⊢y≠x↔x≠y
5 3ancoma ⊢y∈n∧x∈m∧n∩m=∅↔x∈m∧y∈n∧n∩m=∅
6 incom ⊢n∩m=m∩n
7 6 eqeq1i ⊢n∩m=∅↔m∩n=∅
8 7 3anbi3i ⊢x∈m∧y∈n∧n∩m=∅↔x∈m∧y∈n∧m∩n=∅
9 5 8 bitri ⊢y∈n∧x∈m∧n∩m=∅↔x∈m∧y∈n∧m∩n=∅
10 9 2rexbii ⊢∃n∈ordTop⁡R∃m∈ordTop⁡Ry∈n∧x∈m∧n∩m=∅↔∃n∈ordTop⁡R∃m∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
11 rexcom ⊢∃n∈ordTop⁡R∃m∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅↔∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
12 10 11 bitri ⊢∃n∈ordTop⁡R∃m∈ordTop⁡Ry∈n∧x∈m∧n∩m=∅↔∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
13 4 12 imbi12i ⊢y≠x→∃n∈ordTop⁡R∃m∈ordTop⁡Ry∈n∧x∈m∧n∩m=∅↔x≠y→∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
14 3 13 imbitrdi ⊢R∈TosetRel∧y∈dom⁡R∧x∈dom⁡R→yRx→x≠y→∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
15 14 3com23 ⊢R∈TosetRel∧x∈dom⁡R∧y∈dom⁡R→yRx→x≠y→∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
16 1 tsrlin ⊢R∈TosetRel∧x∈dom⁡R∧y∈dom⁡R→xRy∨yRx
17 2 15 16 mpjaod ⊢R∈TosetRel∧x∈dom⁡R∧y∈dom⁡R→x≠y→∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
18 17 3expb ⊢R∈TosetRel∧x∈dom⁡R∧y∈dom⁡R→x≠y→∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
19 18 ralrimivva ⊢R∈TosetRel→∀x∈dom⁡R∀y∈dom⁡Rx≠y→∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
20 1 ordttopon ⊢R∈TosetRel→ordTop⁡R∈TopOn⁡dom⁡R
21 ishaus2 ⊢ordTop⁡R∈TopOn⁡dom⁡R→ordTop⁡R∈Haus↔∀x∈dom⁡R∀y∈dom⁡Rx≠y→∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
22 20 21 syl ⊢R∈TosetRel→ordTop⁡R∈Haus↔∀x∈dom⁡R∀y∈dom⁡Rx≠y→∃m∈ordTop⁡R∃n∈ordTop⁡Rx∈m∧y∈n∧m∩n=∅
23 19 22 mpbird ⊢R∈TosetRel→ordTop⁡R∈Haus