Metamath Proof Explorer

Theorem preimaicomnf

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

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

Proof

Step Hyp Ref Expression
1 preimaicomnf.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
2 preimaicomnf.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
4 fncnvima2 ⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ ( -∞ [,) 𝐵 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) } )
5 3 4 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ [,) 𝐵 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) } )
6 mnfxr ⊢ -∞ ∈ ℝ*
7 6 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) ) → -∞ ∈ ℝ* )
8 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
9 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) )
10 icoltub ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) < 𝐵 )
11 7 8 9 10 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) < 𝐵 )
12 11 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) → ( 𝐹 ‘ 𝑥 ) < 𝐵 ) )
13 6 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) → -∞ ∈ ℝ* )
14 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) → 𝐵 ∈ ℝ* )
15 1 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
17 15 mnfled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -∞ ≤ ( 𝐹 ‘ 𝑥 ) )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) → -∞ ≤ ( 𝐹 ‘ 𝑥 ) )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) → ( 𝐹 ‘ 𝑥 ) < 𝐵 )
20 13 14 16 18 19 elicod ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) )
21 20 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) < 𝐵 → ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) ) )
22 12 21 impbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) ↔ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) )
23 22 rabbidva ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ [,) 𝐵 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 } )
24 5 23 eqtrd ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ [,) 𝐵 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 } )