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) (Revised by Glauco Siliprandi, 20-Dec-2024)

	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		nfcv	|- F/_ x A
4	1 3 2	pimgtmnff	|- ( ph -> { x e. A | -oo < B } = A )