Theorem pimgtmnf2

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

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

Proof

Step	Hyp	Ref	Expression
1		pimgtmnf2.1	|- F/_ x F
2		pimgtmnf2.2	|- ( ph -> F : A --> RR )
3		ssrab2	|- { x e. A | -oo < ( F ` x ) } C_ A
4	3	a1i	|- ( ph -> { x e. A | -oo < ( F ` x ) } C_ A )
5		ssid	|- A C_ A
6	5	a1i	|- ( ph -> A C_ A )
7	2	ffvelrnda	|- ( ( ph /\ y e. A ) -> ( F ` y ) e. RR )
8	7	mnfltd	|- ( ( ph /\ y e. A ) -> -oo < ( F ` y ) )
9	8	ralrimiva	|- ( ph -> A. y e. A -oo < ( F ` y ) )
10		nfcv	|- F/_ x -oo
11		nfcv	|- F/_ x <
12		nfcv	|- F/_ x y
13	1 12	nffv	|- F/_ x ( F ` y )
14	10 11 13	nfbr	|- F/ x -oo < ( F ` y )
15		nfv	|- F/ y -oo < ( F ` x )
16		fveq2	|- ( y = x -> ( F ` y ) = ( F ` x ) )
17	16	breq2d	|- ( y = x -> ( -oo < ( F ` y ) <-> -oo < ( F ` x ) ) )
18	14 15 17	cbvralw	|- ( A. y e. A -oo < ( F ` y ) <-> A. x e. A -oo < ( F ` x ) )
19	9 18	sylib	|- ( ph -> A. x e. A -oo < ( F ` x ) )
20	6 19	jca	|- ( ph -> ( A C_ A /\ A. x e. A -oo < ( F ` x ) ) )
21		nfcv	|- F/_ x A
22	21 21	ssrabf	|- ( A C_ { x e. A | -oo < ( F ` x ) } <-> ( A C_ A /\ A. x e. A -oo < ( F ` x ) ) )
23	20 22	sylibr	|- ( ph -> A C_ { x e. A | -oo < ( F ` x ) } )
24	4 23	eqssd	|- ( ph -> { x e. A | -oo < ( F ` x ) } = A )