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)

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