Theorem pimltpnf2

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	pimltpnf2.1	$$⊢\underset{\_}{Ⅎ}xF$$
	pimltpnf2.2	$$⊢\phi \to F:A⟶ℝ$$
Assertion	pimltpnf2	$$⊢\phi \to \left\{x\in A|F\left(x\right)<\mathrm{+\infty }\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		pimltpnf2.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		pimltpnf2.2	$$⊢\phi \to F:A⟶ℝ$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
5		nfv	$$⊢ℲyF\left(x\right)<\mathrm{+\infty }$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
7	1 6	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}x<$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{+\infty }$$
10	7 8 9	nfbr	$$⊢ℲxF\left(y\right)<\mathrm{+\infty }$$
11		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
12	11	breq1d	$$⊢x=y\to \left(F\left(x\right)<\mathrm{+\infty }\leftrightarrow F\left(y\right)<\mathrm{+\infty }\right)$$
13	3 4 5 10 12	cbvrabw	$$⊢\left\{x\in A|F\left(x\right)<\mathrm{+\infty }\right\}=\left\{y\in A|F\left(y\right)<\mathrm{+\infty }\right\}$$
14	13	a1i	$$⊢\phi \to \left\{x\in A|F\left(x\right)<\mathrm{+\infty }\right\}=\left\{y\in A|F\left(y\right)<\mathrm{+\infty }\right\}$$
15		nfv	$$⊢Ⅎy\phi$$
16	2	ffvelrnda	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)\in ℝ$$
17	15 16	pimltpnf	$$⊢\phi \to \left\{y\in A|F\left(y\right)<\mathrm{+\infty }\right\}=A$$
18	14 17	eqtrd	$$⊢\phi \to \left\{x\in A|F\left(x\right)<\mathrm{+\infty }\right\}=A$$