Metamath Proof Explorer


Theorem pimltmnf2

Description: Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound -oo , is the empty set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 pimltmnf2.1 _ x F
2 pimltmnf2.2 φ F : A
3 nfcv _ x A
4 nfcv _ y A
5 nfv y F x < −∞
6 nfcv _ x y
7 1 6 nffv _ x F y
8 nfcv _ x <
9 nfcv _ x −∞
10 7 8 9 nfbr x F y < −∞
11 fveq2 x = y F x = F y
12 11 breq1d x = y F x < −∞ F y < −∞
13 3 4 5 10 12 cbvrabw x A | F x < −∞ = y A | F y < −∞
14 13 a1i φ x A | F x < −∞ = y A | F y < −∞
15 mnfxr −∞ *
16 15 a1i φ y A −∞ *
17 2 ffvelrnda φ y A F y
18 17 rexrd φ y A F y *
19 17 mnfltd φ y A −∞ < F y
20 16 18 19 xrltled φ y A −∞ F y
21 16 18 xrlenltd φ y A −∞ F y ¬ F y < −∞
22 20 21 mpbid φ y A ¬ F y < −∞
23 22 ralrimiva φ y A ¬ F y < −∞
24 rabeq0 y A | F y < −∞ = y A ¬ F y < −∞
25 23 24 sylibr φ y A | F y < −∞ =
26 14 25 eqtrd φ x A | F x < −∞ =