Theorem pimgtmnf2

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

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

Proof

Step	Hyp	Ref	Expression
1		pimgtmnf2.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		pimgtmnf2.2	$$⊢\phi \to F:A⟶ℝ$$
3		ssrab2	$$⊢\left\{x\in A|\mathrm{-\infty }<F\left(x\right)\right\}\subseteq A$$
4	3	a1i	$$⊢\phi \to \left\{x\in A|\mathrm{-\infty }<F\left(x\right)\right\}\subseteq A$$
5		ssid	$$⊢A\subseteq A$$
6	5	a1i	$$⊢\phi \to A\subseteq A$$
7	2	ffvelcdmda	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)\in ℝ$$
8	7	mnfltd	$$⊢\left(\phi \wedge y\in A\right)\to \mathrm{-\infty }<F\left(y\right)$$
9	8	ralrimiva	$$⊢\phi \to \forall y\in A\mathrm{-\infty }<F\left(y\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{-\infty }$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}x<$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
13	1 12	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
14	10 11 13	nfbr	$$⊢Ⅎx\mathrm{-\infty }<F\left(y\right)$$
15		nfv	$$⊢Ⅎy\mathrm{-\infty }<F\left(x\right)$$
16		fveq2	$$⊢y=x\to F\left(y\right)=F\left(x\right)$$
17	16	breq2d	$$⊢y=x\to \left(\mathrm{-\infty }<F\left(y\right)\leftrightarrow \mathrm{-\infty }<F\left(x\right)\right)$$
18	14 15 17	cbvralw	$$⊢\forall y\in A\mathrm{-\infty }<F\left(y\right)\leftrightarrow \forall x\in A\mathrm{-\infty }<F\left(x\right)$$
19	9 18	sylib	$$⊢\phi \to \forall x\in A\mathrm{-\infty }<F\left(x\right)$$
20	6 19	jca	$$⊢\phi \to \left(A\subseteq A\wedge \forall x\in A\mathrm{-\infty }<F\left(x\right)\right)$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
22	21 21	ssrabf	$$⊢A\subseteq \left\{x\in A|\mathrm{-\infty }<F\left(x\right)\right\}\leftrightarrow \left(A\subseteq A\wedge \forall x\in A\mathrm{-\infty }<F\left(x\right)\right)$$
23	20 22	sylibr	$$⊢\phi \to A\subseteq \left\{x\in A|\mathrm{-\infty }<F\left(x\right)\right\}$$
24	4 23	eqssd	$$⊢\phi \to \left\{x\in A|\mathrm{-\infty }<F\left(x\right)\right\}=A$$