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 )