Theorem 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	⊢ Ⅎ 𝑥 𝐵
	rfcnpre1.2	⊢ Ⅎ 𝑥 𝐹
	rfcnpre1.3	⊢ Ⅎ 𝑥 𝜑
	rfcnpre1.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
	rfcnpre1.5	⊢ 𝑋 = ∪ 𝐽
	rfcnpre1.6	⊢ 𝐴 = { 𝑥 ∈ 𝑋 ∣ 𝐵 < ( 𝐹 ‘ 𝑥 ) }
	rfcnpre1.7	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	rfcnpre1.8	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	rfcnpre1	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		rfcnpre1.1	⊢ Ⅎ 𝑥 𝐵
2		rfcnpre1.2	⊢ Ⅎ 𝑥 𝐹
3		rfcnpre1.3	⊢ Ⅎ 𝑥 𝜑
4		rfcnpre1.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
5		rfcnpre1.5	⊢ 𝑋 = ∪ 𝐽
6		rfcnpre1.6	⊢ 𝐴 = { 𝑥 ∈ 𝑋 ∣ 𝐵 < ( 𝐹 ‘ 𝑥 ) }
7		rfcnpre1.7	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
8		rfcnpre1.8	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
9	2	nfcnv	⊢ Ⅎ 𝑥 ◡ 𝐹
10		nfcv	⊢ Ⅎ 𝑥 (,)
11		nfcv	⊢ Ⅎ 𝑥 +∞
12	1 10 11	nfov	⊢ Ⅎ 𝑥 ( 𝐵 (,) +∞ )
13	9 12	nfima	⊢ Ⅎ 𝑥 ( ◡ 𝐹 “ ( 𝐵 (,) +∞ ) )
14		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝑋 ∣ 𝐵 < ( 𝐹 ‘ 𝑥 ) }
15		cntop1	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
16	8 15	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
17		istopon	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽 ) )
18	16 5 17	sylanblrc	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19		retopon	⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
20	4 19	eqeltri	⊢ 𝐾 ∈ ( TopOn ‘ ℝ )
21		iscn	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ℝ ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
22	18 20 21	sylancl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
23	8 22	mpbid	⊢ ( 𝜑 → ( 𝐹 : 𝑋 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
24	23	simpld	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
25	24	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
26		elioopnf	⊢ ( 𝐵 ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝐵 < ( 𝐹 ‘ 𝑥 ) ) ) )
27	7 26	syl	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝐵 < ( 𝐹 ‘ 𝑥 ) ) ) )
28	27	baibd	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 (,) +∞ ) ↔ 𝐵 < ( 𝐹 ‘ 𝑥 ) ) )
29	25 28	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 (,) +∞ ) ↔ 𝐵 < ( 𝐹 ‘ 𝑥 ) ) )
30	29	pm5.32da	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝐵 < ( 𝐹 ‘ 𝑥 ) ) ) )
31		ffn	⊢ ( 𝐹 : 𝑋 ⟶ ℝ → 𝐹 Fn 𝑋 )
32		elpreima	⊢ ( 𝐹 Fn 𝑋 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝐵 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 (,) +∞ ) ) ) )
33	24 31 32	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝐵 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 (,) +∞ ) ) ) )
34		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝑋 ∣ 𝐵 < ( 𝐹 ‘ 𝑥 ) } ↔ ( 𝑥 ∈ 𝑋 ∧ 𝐵 < ( 𝐹 ‘ 𝑥 ) ) )
35	34	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ 𝑋 ∣ 𝐵 < ( 𝐹 ‘ 𝑥 ) } ↔ ( 𝑥 ∈ 𝑋 ∧ 𝐵 < ( 𝐹 ‘ 𝑥 ) ) ) )
36	30 33 35	3bitr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝐵 (,) +∞ ) ) ↔ 𝑥 ∈ { 𝑥 ∈ 𝑋 ∣ 𝐵 < ( 𝐹 ‘ 𝑥 ) } ) )
37	3 13 14 36	eqrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐵 (,) +∞ ) ) = { 𝑥 ∈ 𝑋 ∣ 𝐵 < ( 𝐹 ‘ 𝑥 ) } )
38	37 6	eqtr4di	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐵 (,) +∞ ) ) = 𝐴 )
39		iooretop	⊢ ( 𝐵 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
40	39 4	eleqtrri	⊢ ( 𝐵 (,) +∞ ) ∈ 𝐾
41		cnima	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐵 (,) +∞ ) ∈ 𝐾 ) → ( ◡ 𝐹 “ ( 𝐵 (,) +∞ ) ) ∈ 𝐽 )
42	8 40 41	sylancl	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐵 (,) +∞ ) ) ∈ 𝐽 )
43	38 42	eqeltrrd	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )