Metamath Proof Explorer

Theorem preimaiocmnf

Description: Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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