Theorem leordtvallem2

Description: Lemma for leordtval . (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypotheses	leordtval.1	⊢ 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
	leordtval.2	⊢ 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
Assertion	leordtvallem2	⊢ 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		leordtval.1	⊢ 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
2		leordtval.2	⊢ 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
3		icossxr	⊢ ( -∞ [,) 𝑥 ) ⊆ ℝ*
4		sseqin2	⊢ ( ( -∞ [,) 𝑥 ) ⊆ ℝ* ↔ ( ℝ* ∩ ( -∞ [,) 𝑥 ) ) = ( -∞ [,) 𝑥 ) )
5	3 4	mpbi	⊢ ( ℝ* ∩ ( -∞ [,) 𝑥 ) ) = ( -∞ [,) 𝑥 )
6		mnfxr	⊢ -∞ ∈ ℝ*
7		simpl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 𝑥 ∈ ℝ* )
8		elico1	⊢ ( ( -∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑦 ∈ ( -∞ [,) 𝑥 ) ↔ ( 𝑦 ∈ ℝ* ∧ -∞ ≤ 𝑦 ∧ 𝑦 < 𝑥 ) ) )
9	6 7 8	sylancr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 ∈ ( -∞ [,) 𝑥 ) ↔ ( 𝑦 ∈ ℝ* ∧ -∞ ≤ 𝑦 ∧ 𝑦 < 𝑥 ) ) )
10		simpr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 𝑦 ∈ ℝ* )
11		mnfle	⊢ ( 𝑦 ∈ ℝ* → -∞ ≤ 𝑦 )
12	10 11	jccir	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 ∈ ℝ* ∧ -∞ ≤ 𝑦 ) )
13	12	biantrurd	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 < 𝑥 ↔ ( ( 𝑦 ∈ ℝ* ∧ -∞ ≤ 𝑦 ) ∧ 𝑦 < 𝑥 ) ) )
14		df-3an	⊢ ( ( 𝑦 ∈ ℝ* ∧ -∞ ≤ 𝑦 ∧ 𝑦 < 𝑥 ) ↔ ( ( 𝑦 ∈ ℝ* ∧ -∞ ≤ 𝑦 ) ∧ 𝑦 < 𝑥 ) )
15	13 14	bitr4di	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 < 𝑥 ↔ ( 𝑦 ∈ ℝ* ∧ -∞ ≤ 𝑦 ∧ 𝑦 < 𝑥 ) ) )
16		xrltnle	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
17	16	ancoms	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
18	9 15 17	3bitr2d	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 ∈ ( -∞ [,) 𝑥 ) ↔ ¬ 𝑥 ≤ 𝑦 ) )
19	18	rabbi2dva	⊢ ( 𝑥 ∈ ℝ* → ( ℝ* ∩ ( -∞ [,) 𝑥 ) ) = { 𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦 } )
20	5 19	eqtr3id	⊢ ( 𝑥 ∈ ℝ* → ( -∞ [,) 𝑥 ) = { 𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦 } )
21	20	mpteq2ia	⊢ ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) = ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦 } )
22	21	rneqi	⊢ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦 } )
23	2 22	eqtri	⊢ 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦 } )