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