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

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 ( 𝑅 ∈ TosetRel → ( ordTop ‘ 𝑅 ) ∈ Haus )

Proof

Step Hyp Ref Expression
1 eqid ⊢ dom 𝑅 = dom 𝑅
2 1 ordthauslem ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑥 𝑅 𝑦 → ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
3 1 ordthauslem ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑦 ∈ dom 𝑅 ∧ 𝑥 ∈ dom 𝑅 ) → ( 𝑦 𝑅 𝑥 → ( 𝑦 ≠ 𝑥 → ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ( 𝑦 ∈ 𝑛 ∧ 𝑥 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
4 necom ⊢ ( 𝑦 ≠ 𝑥 ↔ 𝑥 ≠ 𝑦 )
5 3ancoma ⊢ ( ( 𝑦 ∈ 𝑛 ∧ 𝑥 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
6 incom ⊢ ( 𝑛 ∩ 𝑚 ) = ( 𝑚 ∩ 𝑛 )
7 6 eqeq1i ⊢ ( ( 𝑛 ∩ 𝑚 ) = ∅ ↔ ( 𝑚 ∩ 𝑛 ) = ∅ )
8 7 3anbi3i ⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
9 5 8 bitri ⊢ ( ( 𝑦 ∈ 𝑛 ∧ 𝑥 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
10 9 2rexbii ⊢ ( ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ( 𝑦 ∈ 𝑛 ∧ 𝑥 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
11 rexcom ⊢ ( ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
12 10 11 bitri ⊢ ( ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ( 𝑦 ∈ 𝑛 ∧ 𝑥 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
13 4 12 imbi12i ⊢ ( ( 𝑦 ≠ 𝑥 → ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ( 𝑦 ∈ 𝑛 ∧ 𝑥 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ↔ ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
14 3 13 imbitrdi ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑦 ∈ dom 𝑅 ∧ 𝑥 ∈ dom 𝑅 ) → ( 𝑦 𝑅 𝑥 → ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
15 14 3com23 ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑦 𝑅 𝑥 → ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
16 1 tsrlin ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
17 2 15 16 mpjaod ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
18 17 3expb ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
19 18 ralrimivva ⊢ ( 𝑅 ∈ TosetRel → ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
20 1 ordttopon ⊢ ( 𝑅 ∈ TosetRel → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) )
21 ishaus2 ⊢ ( ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) → ( ( ordTop ‘ 𝑅 ) ∈ Haus ↔ ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
22 20 21 syl ⊢ ( 𝑅 ∈ TosetRel → ( ( ordTop ‘ 𝑅 ) ∈ Haus ↔ ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
23 19 22 mpbird ⊢ ( 𝑅 ∈ TosetRel → ( ordTop ‘ 𝑅 ) ∈ Haus )