Theorem pimltmnf2f

Description: Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound -oo , is the empty set. (Contributed by Glauco Siliprandi, 15-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		pimltmnf2f.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		pimltmnf2f.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		pimltmnf2f.3	$$⊢\phi \to F:A⟶ℝ$$
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	2 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	3	ffvelcdmda	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)\in ℝ$$
15	14	rexrd	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)\in {ℝ}^{*}$$
16	15	mnfled	$$⊢\left(\phi \wedge y\in A\right)\to \mathrm{-\infty }\le F\left(y\right)$$
17		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
18	17	a1i	$$⊢\left(\phi \wedge y\in A\right)\to \mathrm{-\infty }\in {ℝ}^{*}$$
19	18 15	xrlenltd	$$⊢\left(\phi \wedge y\in A\right)\to \left(\mathrm{-\infty }\le F\left(y\right)\leftrightarrow \neg F\left(y\right)<\mathrm{-\infty }\right)$$
20	16 19	mpbid	$$⊢\left(\phi \wedge y\in A\right)\to \neg F\left(y\right)<\mathrm{-\infty }$$
21	20	ralrimiva	$$⊢\phi \to \forall y\in A\neg F\left(y\right)<\mathrm{-\infty }$$
22		rabeq0	$$⊢\left\{y\in A|F\left(y\right)<\mathrm{-\infty }\right\}=\varnothing \leftrightarrow \forall y\in A\neg F\left(y\right)<\mathrm{-\infty }$$
23	21 22	sylibr	$$⊢\phi \to \left\{y\in A|F\left(y\right)<\mathrm{-\infty }\right\}=\varnothing$$
24	13 23	eqtrid	$$⊢\phi \to \left\{x\in A|F\left(x\right)<\mathrm{-\infty }\right\}=\varnothing$$