Metamath Proof Explorer

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 ⊢ Ⅎ _ x B
rfcnpre2.2 ⊢ Ⅎ _ x F
rfcnpre2.3 ⊢ Ⅎ x φ
rfcnpre2.4 ⊢ K = topGen ⁡ ran ⁡ .
rfcnpre2.5 ⊢ X = ⋃ J
rfcnpre2.6 ⊢ A = x ∈ X | F ⁡ x < B
rfcnpre2.7 ⊢ φ → B ∈ ℝ *
rfcnpre2.8 ⊢ φ → F ∈ J Cn K
Assertion rfcnpre2 ⊢ φ → A ∈ J

Proof

Step Hyp Ref Expression
1 rfcnpre2.1 ⊢ Ⅎ _ x B
2 rfcnpre2.2 ⊢ Ⅎ _ x F
3 rfcnpre2.3 ⊢ Ⅎ x φ
4 rfcnpre2.4 ⊢ K = topGen ⁡ ran ⁡ .
5 rfcnpre2.5 ⊢ X = ⋃ J
6 rfcnpre2.6 ⊢ A = x ∈ X | F ⁡ x < B
7 rfcnpre2.7 ⊢ φ → B ∈ ℝ *
8 rfcnpre2.8 ⊢ φ → F ∈ J Cn K
9 2 nfcnv ⊢ Ⅎ _ x F -1
10 nfcv ⊢ Ⅎ _ x −∞
11 nfcv ⊢ Ⅎ _ x .
12 10 11 1 nfov ⊢ Ⅎ _ x −∞ B
13 9 12 nfima ⊢ Ⅎ _ x F -1 −∞ B
14 nfrab1 ⊢ Ⅎ _ x x ∈ X | F ⁡ x < B
15 eqid ⊢ J Cn K = J Cn K
16 4 5 15 8 fcnre ⊢ φ → F : X ⟶ ℝ
17 16 ffvelcdmda ⊢ φ ∧ x ∈ X → F ⁡ x ∈ ℝ
18 elioomnf ⊢ B ∈ ℝ * → F ⁡ x ∈ −∞ B ↔ F ⁡ x ∈ ℝ ∧ F ⁡ x < B
19 7 18 syl ⊢ φ → F ⁡ x ∈ −∞ B ↔ F ⁡ x ∈ ℝ ∧ F ⁡ x < B
20 19 baibd ⊢ φ ∧ F ⁡ x ∈ ℝ → F ⁡ x ∈ −∞ B ↔ F ⁡ x < B
21 17 20 syldan ⊢ φ ∧ x ∈ X → F ⁡ x ∈ −∞ B ↔ F ⁡ x < B
22 21 pm5.32da ⊢ φ → x ∈ X ∧ F ⁡ x ∈ −∞ B ↔ x ∈ X ∧ F ⁡ x < B
23 ffn ⊢ F : X ⟶ ℝ → F Fn X
24 elpreima ⊢ F Fn X → x ∈ F -1 −∞ B ↔ x ∈ X ∧ F ⁡ x ∈ −∞ B
25 16 23 24 3syl ⊢ φ → x ∈ F -1 −∞ B ↔ x ∈ X ∧ F ⁡ x ∈ −∞ B
26 rabid ⊢ x ∈ x ∈ X | F ⁡ x < B ↔ x ∈ X ∧ F ⁡ x < B
27 26 a1i ⊢ φ → x ∈ x ∈ X | F ⁡ x < B ↔ x ∈ X ∧ F ⁡ x < B
28 22 25 27 3bitr4d ⊢ φ → x ∈ F -1 −∞ B ↔ x ∈ x ∈ X | F ⁡ x < B
29 3 13 14 28 eqrd ⊢ φ → F -1 −∞ B = x ∈ X | F ⁡ x < B
30 29 6 eqtr4di ⊢ φ → F -1 −∞ B = A
31 iooretop ⊢ −∞ B ∈ topGen ⁡ ran ⁡ .
32 31 a1i ⊢ φ → −∞ B ∈ topGen ⁡ ran ⁡ .
33 32 4 eleqtrrdi ⊢ φ → −∞ B ∈ K
34 cnima ⊢ F ∈ J Cn K ∧ −∞ B ∈ K → F -1 −∞ B ∈ J
35 8 33 34 syl2anc ⊢ φ → F -1 −∞ B ∈ J
36 30 35 eqeltrrd ⊢ φ → A ∈ J