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

Metamath Proof Explorer

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 ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦 } )