Theorem pimgtmnff

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, 20-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		pimgtmnff.1	|- F/ x ph
2		pimgtmnff.2	|- F/_ x A
3		pimgtmnff.3	|- ( ( ph /\ x e. A ) -> B e. RR )
4	2	ssrab2f	|- { x e. A | -oo < B } C_ A
5	4	a1i	|- ( ph -> { x e. A | -oo < B } C_ A )
6		simpr	|- ( ( ph /\ x e. A ) -> x e. A )
7		mnflt	|- ( B e. RR -> -oo < B )
8	3 7	syl	|- ( ( ph /\ x e. A ) -> -oo < B )
9	6 8	jca	|- ( ( ph /\ x e. A ) -> ( x e. A /\ -oo < B ) )
10		rabid	|- ( x e. { x e. A | -oo < B } <-> ( x e. A /\ -oo < B ) )
11	9 10	sylibr	|- ( ( ph /\ x e. A ) -> x e. { x e. A | -oo < B } )
12	11	ex	|- ( ph -> ( x e. A -> x e. { x e. A | -oo < B } ) )
13	1 12	ralrimi	|- ( ph -> A. x e. A x e. { x e. A | -oo < B } )
14		nfrab1	|- F/_ x { x e. A | -oo < B }
15	2 14	dfss3f	|- ( A C_ { x e. A | -oo < B } <-> A. x e. A x e. { x e. A | -oo < B } )
16	13 15	sylibr	|- ( ph -> A C_ { x e. A | -oo < B } )
17	5 16	eqssd	|- ( ph -> { x e. A | -oo < B } = A )