Metamath Proof Explorer


Theorem pimgtmnf2

Description: Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -oo , is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses pimgtmnf2.1 _ x F
pimgtmnf2.2 φ F : A
Assertion pimgtmnf2 φ x A | −∞ < F x = A

Proof

Step Hyp Ref Expression
1 pimgtmnf2.1 _ x F
2 pimgtmnf2.2 φ F : A
3 ssrab2 x A | −∞ < F x A
4 3 a1i φ x A | −∞ < F x A
5 ssid A A
6 5 a1i φ A A
7 2 ffvelrnda φ y A F y
8 7 mnfltd φ y A −∞ < F y
9 8 ralrimiva φ y A −∞ < F y
10 nfcv _ x −∞
11 nfcv _ x <
12 nfcv _ x y
13 1 12 nffv _ x F y
14 10 11 13 nfbr x −∞ < F y
15 nfv y −∞ < F x
16 fveq2 y = x F y = F x
17 16 breq2d y = x −∞ < F y −∞ < F x
18 14 15 17 cbvralw y A −∞ < F y x A −∞ < F x
19 9 18 sylib φ x A −∞ < F x
20 6 19 jca φ A A x A −∞ < F x
21 nfcv _ x A
22 21 21 ssrabf A x A | −∞ < F x A A x A −∞ < F x
23 20 22 sylibr φ A x A | −∞ < F x
24 4 23 eqssd φ x A | −∞ < F x = A