Theorem preimaioomnf

Description: Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	preimaioomnf.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
	preimaioomnf.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
Assertion	preimaioomnf	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		preimaioomnf.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
2		preimaioomnf.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
4	1	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
5		fimacnvinrn2	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ℝ ) → ( ◡ 𝐹 “ ( -∞ [,) 𝐵 ) ) = ( ◡ 𝐹 “ ( ( -∞ [,) 𝐵 ) ∩ ℝ ) ) )
6	3 4 5	syl2anc	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ [,) 𝐵 ) ) = ( ◡ 𝐹 “ ( ( -∞ [,) 𝐵 ) ∩ ℝ ) ) )
7	2	icomnfinre	⊢ ( 𝜑 → ( ( -∞ [,) 𝐵 ) ∩ ℝ ) = ( -∞ (,) 𝐵 ) )
8	7	imaeq2d	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ( -∞ [,) 𝐵 ) ∩ ℝ ) ) = ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) )
9	6 8	eqtr2d	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) = ( ◡ 𝐹 “ ( -∞ [,) 𝐵 ) ) )
10	1	frexr	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
11	10 2	preimaicomnf	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ [,) 𝐵 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 } )
12	9 11	eqtrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 } )