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 ⊢ φ → F : A ⟶ ℝ
preimaiocmnf.2 ⊢ φ → B ∈ ℝ *
Assertion preimaiocmnf ⊢ φ → F -1 −∞ B = x ∈ A | F ⁡ x ≤ B

Proof

Step Hyp Ref Expression
1 preimaiocmnf.1 ⊢ φ → F : A ⟶ ℝ
2 preimaiocmnf.2 ⊢ φ → B ∈ ℝ *
3 1 ffnd ⊢ φ → F Fn A
4 fncnvima2 ⊢ F Fn A → F -1 −∞ B = x ∈ A | F ⁡ x ∈ −∞ B
5 3 4 syl ⊢ φ → F -1 −∞ B = x ∈ A | F ⁡ x ∈ −∞ B
6 mnfxr ⊢ −∞ ∈ ℝ *
7 6 a1i ⊢ φ ∧ F ⁡ x ∈ −∞ B → −∞ ∈ ℝ *
8 2 adantr ⊢ φ ∧ F ⁡ x ∈ −∞ B → B ∈ ℝ *
9 simpr ⊢ φ ∧ F ⁡ x ∈ −∞ B → F ⁡ x ∈ −∞ B
10 7 8 9 iocleubd ⊢ φ ∧ F ⁡ x ∈ −∞ B → F ⁡ x ≤ B
11 10 ex ⊢ φ → F ⁡ x ∈ −∞ B → F ⁡ x ≤ B
12 11 adantr ⊢ φ ∧ x ∈ A → F ⁡ x ∈ −∞ B → F ⁡ x ≤ B
13 6 a1i ⊢ φ ∧ x ∈ A ∧ F ⁡ x ≤ B → −∞ ∈ ℝ *
14 2 adantr ⊢ φ ∧ F ⁡ x ≤ B → B ∈ ℝ *
15 14 adantlr ⊢ φ ∧ x ∈ A ∧ F ⁡ x ≤ B → B ∈ ℝ *
16 1 ffvelcdmda ⊢ φ ∧ x ∈ A → F ⁡ x ∈ ℝ
17 16 rexrd ⊢ φ ∧ x ∈ A → F ⁡ x ∈ ℝ *
18 17 adantr ⊢ φ ∧ x ∈ A ∧ F ⁡ x ≤ B → F ⁡ x ∈ ℝ *
19 16 mnfltd ⊢ φ ∧ x ∈ A → −∞ < F ⁡ x
20 19 adantr ⊢ φ ∧ x ∈ A ∧ F ⁡ x ≤ B → −∞ < F ⁡ x
21 simpr ⊢ φ ∧ x ∈ A ∧ F ⁡ x ≤ B → F ⁡ x ≤ B
22 13 15 18 20 21 eliocd ⊢ φ ∧ x ∈ A ∧ F ⁡ x ≤ B → F ⁡ x ∈ −∞ B
23 22 ex ⊢ φ ∧ x ∈ A → F ⁡ x ≤ B → F ⁡ x ∈ −∞ B
24 12 23 impbid ⊢ φ ∧ x ∈ A → F ⁡ x ∈ −∞ B ↔ F ⁡ x ≤ B
25 24 rabbidva ⊢ φ → x ∈ A | F ⁡ x ∈ −∞ B = x ∈ A | F ⁡ x ≤ B
26 5 25 eqtrd ⊢ φ → F -1 −∞ B = x ∈ A | F ⁡ x ≤ B