Theorem pimgtpnf2f

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, 15-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		pimgtpnf2f.1	|- F/_ x F
2		pimgtpnf2f.2	|- F/_ x A
3		pimgtpnf2f.3	|- ( ph -> F : A --> RR )
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	2 4 5 10 12	cbvrabw	|- { x e. A | +oo < ( F ` x ) } = { y e. A | +oo < ( F ` y ) }
14	3	ffvelcdmda	|- ( ( ph /\ y e. A ) -> ( F ` y ) e. RR )
15	14	rexrd	|- ( ( ph /\ y e. A ) -> ( F ` y ) e. RR* )
16	15	pnfged	|- ( ( ph /\ y e. A ) -> ( F ` y ) <_ +oo )
17		pnfxr	|- +oo e. RR*
18	17	a1i	|- ( ( ph /\ y e. A ) -> +oo e. RR* )
19	15 18	xrlenltd	|- ( ( ph /\ y e. A ) -> ( ( F ` y ) <_ +oo <-> -. +oo < ( F ` y ) ) )
20	16 19	mpbid	|- ( ( ph /\ y e. A ) -> -. +oo < ( F ` y ) )
21	20	ralrimiva	|- ( ph -> A. y e. A -. +oo < ( F ` y ) )
22		rabeq0	|- ( { y e. A | +oo < ( F ` y ) } = (/) <-> A. y e. A -. +oo < ( F ` y ) )
23	21 22	sylibr	|- ( ph -> { y e. A | +oo < ( F ` y ) } = (/) )
24	13 23	eqtrid	|- ( ph -> { x e. A | +oo < ( F ` x ) } = (/) )