Theorem rfcnpre2

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

	Ref	Expression
Hypotheses	rfcnpre2.1	⊢ Ⅎ 𝑥 𝐵
	rfcnpre2.2	⊢ Ⅎ 𝑥 𝐹
	rfcnpre2.3	⊢ Ⅎ 𝑥 𝜑
	rfcnpre2.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
	rfcnpre2.5	⊢ 𝑋 = ∪ 𝐽
	rfcnpre2.6	⊢ 𝐴 = { 𝑥 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 }
	rfcnpre2.7	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	rfcnpre2.8	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	rfcnpre2	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		rfcnpre2.1	⊢ Ⅎ 𝑥 𝐵
2		rfcnpre2.2	⊢ Ⅎ 𝑥 𝐹
3		rfcnpre2.3	⊢ Ⅎ 𝑥 𝜑
4		rfcnpre2.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
5		rfcnpre2.5	⊢ 𝑋 = ∪ 𝐽
6		rfcnpre2.6	⊢ 𝐴 = { 𝑥 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 }
7		rfcnpre2.7	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
8		rfcnpre2.8	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
9	2	nfcnv	⊢ Ⅎ 𝑥 ◡ 𝐹
10		nfcv	⊢ Ⅎ 𝑥 -∞
11		nfcv	⊢ Ⅎ 𝑥 (,)
12	10 11 1	nfov	⊢ Ⅎ 𝑥 ( -∞ (,) 𝐵 )
13	9 12	nfima	⊢ Ⅎ 𝑥 ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) )
14		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 }
15		eqid	⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 )
16	4 5 15 8	fcnre	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
17	16	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
18		elioomnf	⊢ ( 𝐵 ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝐵 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) ) )
19	7 18	syl	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝐵 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) ) )
20	19	baibd	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝐵 ) ↔ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) )
21	17 20	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝐵 ) ↔ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) )
22	21	pm5.32da	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝐵 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) ) )
23		ffn	⊢ ( 𝐹 : 𝑋 ⟶ ℝ → 𝐹 Fn 𝑋 )
24		elpreima	⊢ ( 𝐹 Fn 𝑋 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝐵 ) ) ) )
25	16 23 24	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝐵 ) ) ) )
26		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 } ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) )
27	26	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 } ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) < 𝐵 ) ) )
28	22 25 27	3bitr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) ↔ 𝑥 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 } ) )
29	3 13 14 28	eqrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) = { 𝑥 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐵 } )
30	29 6	eqtr4di	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) = 𝐴 )
31		iooretop	⊢ ( -∞ (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
32	31	a1i	⊢ ( 𝜑 → ( -∞ (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
33	32 4	eleqtrrdi	⊢ ( 𝜑 → ( -∞ (,) 𝐵 ) ∈ 𝐾 )
34		cnima	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( -∞ (,) 𝐵 ) ∈ 𝐾 ) → ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) ∈ 𝐽 )
35	8 33 34	syl2anc	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ (,) 𝐵 ) ) ∈ 𝐽 )
36	30 35	eqeltrrd	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )