Metamath Proof Explorer


Theorem pimltpnf2

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

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

Proof

Step Hyp Ref Expression
1 pimltpnf2.1 _ x F
2 pimltpnf2.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 nfv y φ
16 2 ffvelrnda φ y A F y
17 15 16 pimltpnf φ y A | F y < +∞ = A
18 14 17 eqtrd φ x A | F x < +∞ = A