Theorem pimgtpnf2

Description: Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound +oo , is the empty set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	pimgtpnf2.1	$$⊢\underset{\_}{Ⅎ}xF$$
	pimgtpnf2.2	$$⊢\phi \to F:A⟶ℝ$$
Assertion	pimgtpnf2	$$⊢\phi \to \left\{x\in A|\mathrm{+\infty }<F\left(x\right)\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		pimgtpnf2.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		pimgtpnf2.2	$$⊢\phi \to F:A⟶ℝ$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
5		nfv	$$⊢Ⅎy\mathrm{+\infty }<F\left(x\right)$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{+\infty }$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}x<$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
9	1 8	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
10	6 7 9	nfbr	$$⊢Ⅎx\mathrm{+\infty }<F\left(y\right)$$
11		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
12	11	breq2d	$$⊢x=y\to \left(\mathrm{+\infty }<F\left(x\right)\leftrightarrow \mathrm{+\infty }<F\left(y\right)\right)$$
13	3 4 5 10 12	cbvrabw	$$⊢\left\{x\in A|\mathrm{+\infty }<F\left(x\right)\right\}=\left\{y\in A|\mathrm{+\infty }<F\left(y\right)\right\}$$
14	13	a1i	$$⊢\phi \to \left\{x\in A|\mathrm{+\infty }<F\left(x\right)\right\}=\left\{y\in A|\mathrm{+\infty }<F\left(y\right)\right\}$$
15	2	ffvelrnda	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)\in ℝ$$
16	15	rexrd	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)\in {ℝ}^{*}$$
17		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
18	17	a1i	$$⊢\left(\phi \wedge y\in A\right)\to \mathrm{+\infty }\in {ℝ}^{*}$$
19	15	ltpnfd	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)<\mathrm{+\infty }$$
20	16 18 19	xrltled	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)\le \mathrm{+\infty }$$
21	16 18	xrlenltd	$$⊢\left(\phi \wedge y\in A\right)\to \left(F\left(y\right)\le \mathrm{+\infty }\leftrightarrow \neg \mathrm{+\infty }<F\left(y\right)\right)$$
22	20 21	mpbid	$$⊢\left(\phi \wedge y\in A\right)\to \neg \mathrm{+\infty }<F\left(y\right)$$
23	22	ralrimiva	$$⊢\phi \to \forall y\in A\neg \mathrm{+\infty }<F\left(y\right)$$
24		rabeq0	$$⊢\left\{y\in A|\mathrm{+\infty }<F\left(y\right)\right\}=\varnothing \leftrightarrow \forall y\in A\neg \mathrm{+\infty }<F\left(y\right)$$
25	23 24	sylibr	$$⊢\phi \to \left\{y\in A|\mathrm{+\infty }<F\left(y\right)\right\}=\varnothing$$
26	14 25	eqtrd	$$⊢\phi \to \left\{x\in A|\mathrm{+\infty }<F\left(x\right)\right\}=\varnothing$$