rfcnpre1

Description: If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than a given extended real B is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	rfcnpre1.1	$⊢ \underline{Ⅎ} x B$
	rfcnpre1.2	$⊢ \underline{Ⅎ} x F$
	rfcnpre1.3	$⊢ Ⅎ x φ$
	rfcnpre1.4	$⊢ K = topGen (ran (.))$
	rfcnpre1.5	$⊢ X = ⋃ J$
	rfcnpre1.6	$⊢ A = \{x \in X \| B < F (x)\}$
	rfcnpre1.7	$⊢ φ \to B \in ℝ^{*}$
	rfcnpre1.8	$⊢ φ \to F \in (J Cn K)$
Assertion	rfcnpre1	$⊢ φ \to A \in J$

Proof

Step	Hyp	Ref	Expression
1		rfcnpre1.1	$⊢ \underline{Ⅎ} x B$
2		rfcnpre1.2	$⊢ \underline{Ⅎ} x F$
3		rfcnpre1.3	$⊢ Ⅎ x φ$
4		rfcnpre1.4	$⊢ K = topGen (ran (.))$
5		rfcnpre1.5	$⊢ X = ⋃ J$
6		rfcnpre1.6	$⊢ A = \{x \in X \| B < F (x)\}$
7		rfcnpre1.7	$⊢ φ \to B \in ℝ^{*}$
8		rfcnpre1.8	$⊢ φ \to F \in (J Cn K)$
9	2	nfcnv	$⊢ \underline{Ⅎ} x F^{-1}$
10		nfcv	$⊢ \underline{Ⅎ} x (.)$
11		nfcv	$⊢ \underline{Ⅎ} x +∞$
12	1 10 11	nfov	$⊢ \underline{Ⅎ} x (B, +∞)$
13	9 12	nfima	$⊢ \underline{Ⅎ} x F^{-1} [(B, +∞)]$
14		nfrab1	$⊢ \underline{Ⅎ} x \{x \in X \| B < F (x)\}$
15		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
16	8 15	syl	$⊢ φ \to J \in Top$
17		istopon	$⊢ J \in TopOn (X) \leftrightarrow (J \in Top \land X = ⋃ J)$
18	16 5 17	sylanblrc	$⊢ φ \to J \in TopOn (X)$
19		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
20	4 19	eqeltri	$⊢ K \in TopOn (ℝ)$
21		iscn	$⊢ (J \in TopOn (X) \land K \in TopOn (ℝ)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ ℝ \land \forall y \in K F^{-1} [y] \in J))$
22	18 20 21	sylancl	$⊢ φ \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ ℝ \land \forall y \in K F^{-1} [y] \in J))$
23	8 22	mpbid	$⊢ φ \to (F : X ⟶ ℝ \land \forall y \in K F^{-1} [y] \in J)$
24	23	simpld	$⊢ φ \to F : X ⟶ ℝ$
25	24	ffvelcdmda	$⊢ (φ \land x \in X) \to F (x) \in ℝ$
26		elioopnf	$⊢ B \in ℝ^{*} \to (F (x) \in (B, +∞) \leftrightarrow (F (x) \in ℝ \land B < F (x)))$
27	7 26	syl	$⊢ φ \to (F (x) \in (B, +∞) \leftrightarrow (F (x) \in ℝ \land B < F (x)))$
28	27	baibd	$⊢ (φ \land F (x) \in ℝ) \to (F (x) \in (B, +∞) \leftrightarrow B < F (x))$
29	25 28	syldan	$⊢ (φ \land x \in X) \to (F (x) \in (B, +∞) \leftrightarrow B < F (x))$
30	29	pm5.32da	$⊢ φ \to ((x \in X \land F (x) \in (B, +∞)) \leftrightarrow (x \in X \land B < F (x)))$
31		ffn	$⊢ F : X ⟶ ℝ \to F Fn X$
32		elpreima	$⊢ F Fn X \to (x \in F^{-1} [(B, +∞)] \leftrightarrow (x \in X \land F (x) \in (B, +∞)))$
33	24 31 32	3syl	$⊢ φ \to (x \in F^{-1} [(B, +∞)] \leftrightarrow (x \in X \land F (x) \in (B, +∞)))$
34		rabid	$⊢ x \in \{x \in X \| B < F (x)\} \leftrightarrow (x \in X \land B < F (x))$
35	34	a1i	$⊢ φ \to (x \in \{x \in X \| B < F (x)\} \leftrightarrow (x \in X \land B < F (x)))$
36	30 33 35	3bitr4d	$⊢ φ \to (x \in F^{-1} [(B, +∞)] \leftrightarrow x \in \{x \in X \| B < F (x)\})$
37	3 13 14 36	eqrd	$⊢ φ \to F^{-1} [(B, +∞)] = \{x \in X \| B < F (x)\}$
38	37 6	eqtr4di	$⊢ φ \to F^{-1} [(B, +∞)] = A$
39		iooretop	$⊢ (B, +∞) \in topGen (ran (.))$
40	39 4	eleqtrri	$⊢ (B, +∞) \in K$
41		cnima	$⊢ (F \in (J Cn K) \land (B, +∞) \in K) \to F^{-1} [(B, +∞)] \in J$
42	8 40 41	sylancl	$⊢ φ \to F^{-1} [(B, +∞)] \in J$
43	38 42	eqeltrrd	$⊢ φ \to A \in J$

Metamath Proof Explorer

Theorem rfcnpre1

Proof