Theorem pimgtpnf2

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

	Ref	Expression
Hypotheses	pimgtpnf2.1	|- F/_ x F
	pimgtpnf2.2	|- ( ph -> F : A --> RR )
Assertion	pimgtpnf2	|- ( ph -> { x e. A | +oo < ( F ` x ) } = (/) )

Proof

Step	Hyp	Ref	Expression
1		pimgtpnf2.1	|- F/_ x F
2		pimgtpnf2.2	|- ( ph -> F : A --> RR )
3		nfcv	|- F/_ x A
4		nfcv	|- F/_ y A
5		nfv	|- F/ y +oo < ( F ` x )
6		nfcv	|- F/_ x +oo
7		nfcv	|- F/_ x <
8		nfcv	|- F/_ x y
9	1 8	nffv	|- F/_ x ( F ` y )
10	6 7 9	nfbr	|- F/ x +oo < ( F ` y )
11		fveq2	|- ( x = y -> ( F ` x ) = ( F ` y ) )
12	11	breq2d	|- ( x = y -> ( +oo < ( F ` x ) <-> +oo < ( F ` y ) ) )
13	3 4 5 10 12	cbvrabw	|- { x e. A | +oo < ( F ` x ) } = { y e. A | +oo < ( F ` y ) }
14	13	a1i	|- ( ph -> { x e. A | +oo < ( F ` x ) } = { y e. A | +oo < ( F ` y ) } )
15	2	ffvelrnda	|- ( ( ph /\ y e. A ) -> ( F ` y ) e. RR )
16	15	rexrd	|- ( ( ph /\ y e. A ) -> ( F ` y ) e. RR* )
17		pnfxr	|- +oo e. RR*
18	17	a1i	|- ( ( ph /\ y e. A ) -> +oo e. RR* )
19	15	ltpnfd	|- ( ( ph /\ y e. A ) -> ( F ` y ) < +oo )
20	16 18 19	xrltled	|- ( ( ph /\ y e. A ) -> ( F ` y ) <_ +oo )
21	16 18	xrlenltd	|- ( ( ph /\ y e. A ) -> ( ( F ` y ) <_ +oo <-> -. +oo < ( F ` y ) ) )
22	20 21	mpbid	|- ( ( ph /\ y e. A ) -> -. +oo < ( F ` y ) )
23	22	ralrimiva	|- ( ph -> A. y e. A -. +oo < ( F ` y ) )
24		rabeq0	|- ( { y e. A | +oo < ( F ` y ) } = (/) <-> A. y e. A -. +oo < ( F ` y ) )
25	23 24	sylibr	|- ( ph -> { y e. A | +oo < ( F ` y ) } = (/) )
26	14 25	eqtrd	|- ( ph -> { x e. A | +oo < ( F ` x ) } = (/) )