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
|- F/_ x F
pimltpnf2.2
|- ( ph -> F : A --> RR )
Assertion pimltpnf2
|- ( ph -> { x e. A | ( F ` x ) < +oo } = A )

Proof

Step Hyp Ref Expression
1 pimltpnf2.1
 |-  F/_ x F
2 pimltpnf2.2
 |-  ( ph -> F : A --> RR )
3 nfcv
 |-  F/_ x A
4 nfcv
 |-  F/_ y A
5 nfv
 |-  F/ y ( F ` x ) < +oo
6 nfcv
 |-  F/_ x y
7 1 6 nffv
 |-  F/_ x ( F ` y )
8 nfcv
 |-  F/_ x <
9 nfcv
 |-  F/_ x +oo
10 7 8 9 nfbr
 |-  F/ x ( F ` y ) < +oo
11 fveq2
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
12 11 breq1d
 |-  ( x = y -> ( ( F ` x ) < +oo <-> ( F ` y ) < +oo ) )
13 3 4 5 10 12 cbvrabw
 |-  { x e. A | ( F ` x ) < +oo } = { y e. A | ( F ` y ) < +oo }
14 13 a1i
 |-  ( ph -> { x e. A | ( F ` x ) < +oo } = { y e. A | ( F ` y ) < +oo } )
15 nfv
 |-  F/ y ph
16 2 ffvelrnda
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) e. RR )
17 15 16 pimltpnf
 |-  ( ph -> { y e. A | ( F ` y ) < +oo } = A )
18 14 17 eqtrd
 |-  ( ph -> { x e. A | ( F ` x ) < +oo } = A )