Theorem pimltpnf

Description: Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +oo , is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Revised by Glauco Siliprandi, 20-Dec-2024)

	Ref	Expression
Hypotheses	pimltpnf.1	|- F/ x ph
	pimltpnf.2	|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion	pimltpnf	|- ( ph -> { x e. A | B < +oo } = A )

Proof

Step	Hyp	Ref	Expression
1		pimltpnf.1	|- F/ x ph
2		pimltpnf.2	|- ( ( ph /\ x e. A ) -> B e. RR )
3		nfcv	|- F/_ x A
4	1 3 2	pimltpnff	|- ( ph -> { x e. A | B < +oo } = A )