Theorem leordtval

Description: The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypotheses	leordtval.1	⊢ 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
	leordtval.2	⊢ 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
	leordtval.3	⊢ 𝐶 = ran (,)
Assertion	leordtval	⊢ ( ordTop ‘ ≤ ) = ( topGen ‘ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		leordtval.1	⊢ 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
2		leordtval.2	⊢ 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
3		leordtval.3	⊢ 𝐶 = ran (,)
4	1 2	leordtval2	⊢ ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
5		letsr	⊢ ≤ ∈ TosetRel
6		ledm	⊢ ℝ* = dom ≤
7	1	leordtvallem1	⊢ 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥 } )
8	1 2	leordtvallem2	⊢ 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦 } )
9		df-ioo	⊢ (,) = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ( 𝑎 < 𝑦 ∧ 𝑦 < 𝑏 ) } )
10		xrltnle	⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑎 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑎 ) )
11	10	adantlr	⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → ( 𝑎 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑎 ) )
12		xrltnle	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑦 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑦 ) )
13	12	ancoms	⊢ ( ( 𝑏 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑦 ) )
14	13	adantll	⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑦 ) )
15	11 14	anbi12d	⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑎 < 𝑦 ∧ 𝑦 < 𝑏 ) ↔ ( ¬ 𝑦 ≤ 𝑎 ∧ ¬ 𝑏 ≤ 𝑦 ) ) )
16	15	rabbidva	⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → { 𝑦 ∈ ℝ* ∣ ( 𝑎 < 𝑦 ∧ 𝑦 < 𝑏 ) } = { 𝑦 ∈ ℝ* ∣ ( ¬ 𝑦 ≤ 𝑎 ∧ ¬ 𝑏 ≤ 𝑦 ) } )
17	16	mpoeq3ia	⊢ ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ( 𝑎 < 𝑦 ∧ 𝑦 < 𝑏 ) } ) = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ( ¬ 𝑦 ≤ 𝑎 ∧ ¬ 𝑏 ≤ 𝑦 ) } )
18	9 17	eqtri	⊢ (,) = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ( ¬ 𝑦 ≤ 𝑎 ∧ ¬ 𝑏 ≤ 𝑦 ) } )
19	18	rneqi	⊢ ran (,) = ran ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ( ¬ 𝑦 ≤ 𝑎 ∧ ¬ 𝑏 ≤ 𝑦 ) } )
20	3 19	eqtri	⊢ 𝐶 = ran ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ( ¬ 𝑦 ≤ 𝑎 ∧ ¬ 𝑏 ≤ 𝑦 ) } )
21	6 7 8 20	ordtbas2	⊢ ( ≤ ∈ TosetRel → ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
22	5 21	ax-mp	⊢ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 )
23	22	fveq2i	⊢ ( topGen ‘ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) = ( topGen ‘ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
24	4 23	eqtri	⊢ ( ordTop ‘ ≤ ) = ( topGen ‘ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )