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 ffvelrnda φ 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