Theorem pimltpnff

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

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

Proof

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