Theorem pimgtmnf

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	pimgtmnf.1	|- F/ x ph
	pimgtmnf.2	|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion	pimgtmnf	|- ( ph -> { x e. A | -oo < B } = A )

Proof

Step	Hyp	Ref	Expression
1		pimgtmnf.1	|- F/ x ph
2		pimgtmnf.2	|- ( ( ph /\ x e. A ) -> B e. RR )
3		eqidd	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
4	3 2	fvmpt2d	|- ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
5	4	eqcomd	|- ( ( ph /\ x e. A ) -> B = ( ( x e. A |-> B ) ` x ) )
6	5	breq2d	|- ( ( ph /\ x e. A ) -> ( -oo < B <-> -oo < ( ( x e. A |-> B ) ` x ) ) )
7	1 6	rabbida	|- ( ph -> { x e. A | -oo < B } = { x e. A | -oo < ( ( x e. A |-> B ) ` x ) } )
8		nfmpt1	|- F/_ x ( x e. A |-> B )
9		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
10	1 2 9	fmptdf	|- ( ph -> ( x e. A |-> B ) : A --> RR )
11	8 10	pimgtmnf2	|- ( ph -> { x e. A | -oo < ( ( x e. A |-> B ) ` x ) } = A )
12	7 11	eqtrd	|- ( ph -> { x e. A | -oo < B } = A )