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

Metamath Proof Explorer

Theorem leordtvallem1

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

Ref Expression
Hypothesis leordtval.1 ⊢ 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
Assertion leordtvallem1 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥 } )

Proof

Step Hyp Ref Expression
1 leordtval.1 ⊢ 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
2 iocssxr ⊢ ( 𝑥 (,] +∞ ) ⊆ ℝ*
3 sseqin2 ⊢ ( ( 𝑥 (,] +∞ ) ⊆ ℝ* ↔ ( ℝ* ∩ ( 𝑥 (,] +∞ ) ) = ( 𝑥 (,] +∞ ) )
4 2 3 mpbi ⊢ ( ℝ* ∩ ( 𝑥 (,] +∞ ) ) = ( 𝑥 (,] +∞ )
5 simpl ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 𝑥 ∈ ℝ* )
6 pnfxr ⊢ +∞ ∈ ℝ*
7 elioc1 ⊢ ( ( 𝑥 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑦 ∈ ( 𝑥 (,] +∞ ) ↔ ( 𝑦 ∈ ℝ* ∧ 𝑥 < 𝑦 ∧ 𝑦 ≤ +∞ ) ) )
8 5 6 7 sylancl ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝑥 (,] +∞ ) ↔ ( 𝑦 ∈ ℝ* ∧ 𝑥 < 𝑦 ∧ 𝑦 ≤ +∞ ) ) )
9 simpr ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 𝑦 ∈ ℝ* )
10 pnfge ⊢ ( 𝑦 ∈ ℝ* → 𝑦 ≤ +∞ )
11 9 10 jccir ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 ∈ ℝ* ∧ 𝑦 ≤ +∞ ) )
12 11 biantrurd ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ ( ( 𝑦 ∈ ℝ* ∧ 𝑦 ≤ +∞ ) ∧ 𝑥 < 𝑦 ) ) )
13 3anan32 ⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 < 𝑦 ∧ 𝑦 ≤ +∞ ) ↔ ( ( 𝑦 ∈ ℝ* ∧ 𝑦 ≤ +∞ ) ∧ 𝑥 < 𝑦 ) )
14 12 13 bitr4di ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ ( 𝑦 ∈ ℝ* ∧ 𝑥 < 𝑦 ∧ 𝑦 ≤ +∞ ) ) )
15 xrltnle ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
16 8 14 15 3bitr2d ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝑥 (,] +∞ ) ↔ ¬ 𝑦 ≤ 𝑥 ) )
17 16 rabbi2dva ⊢ ( 𝑥 ∈ ℝ* → ( ℝ* ∩ ( 𝑥 (,] +∞ ) ) = { 𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥 } )
18 4 17 eqtr3id ⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 (,] +∞ ) = { 𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥 } )
19 18 mpteq2ia ⊢ ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) = ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥 } )
20 19 rneqi ⊢ ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥 } )
21 1 20 eqtri ⊢ 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥 } )