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