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 ⊢φ→FFnA
4 fncnvima2 ⊢FFnA→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