Metamath Proof Explorer

Theorem 1stccn

Description: A mapping X --> Y , where X is first-countable, is continuous iff it is sequentially continuous, meaning that for any sequence f ( n ) converging to x , its image under F converges to F ( x ) . (Contributed by Mario Carneiro, 7-Sep-2015)

Ref Expression
Hypotheses 1stccnp.1 ⊢ φ → J ∈ 1 st 𝜔
1stccnp.2 ⊢ φ → J ∈ TopOn ⁡ X
1stccnp.3 ⊢ φ → K ∈ TopOn ⁡ Y
1stccn.7 ⊢ φ → F : X ⟶ Y
Assertion 1stccn ⊢ φ → F ∈ J Cn K ↔ ∀ f f : ℕ ⟶ X → ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x

Proof

Step Hyp Ref Expression
1 1stccnp.1 ⊢ φ → J ∈ 1 st 𝜔
2 1stccnp.2 ⊢ φ → J ∈ TopOn ⁡ X
3 1stccnp.3 ⊢ φ → K ∈ TopOn ⁡ Y
4 1stccn.7 ⊢ φ → F : X ⟶ Y
5 cncnp ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x
6 2 3 5 syl2anc ⊢ φ → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x
7 4 6 mpbirand ⊢ φ → F ∈ J Cn K ↔ ∀ x ∈ X F ∈ J CnP K ⁡ x
8 4 adantr ⊢ φ ∧ x ∈ X → F : X ⟶ Y
9 1 adantr ⊢ φ ∧ x ∈ X → J ∈ 1 st 𝜔
10 2 adantr ⊢ φ ∧ x ∈ X → J ∈ TopOn ⁡ X
11 3 adantr ⊢ φ ∧ x ∈ X → K ∈ TopOn ⁡ Y
12 simpr ⊢ φ ∧ x ∈ X → x ∈ X
13 9 10 11 12 1stccnp ⊢ φ ∧ x ∈ X → F ∈ J CnP K ⁡ x ↔ F : X ⟶ Y ∧ ∀ f f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
14 8 13 mpbirand ⊢ φ ∧ x ∈ X → F ∈ J CnP K ⁡ x ↔ ∀ f f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
15 14 ralbidva ⊢ φ → ∀ x ∈ X F ∈ J CnP K ⁡ x ↔ ∀ x ∈ X ∀ f f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
16 ralcom4 ⊢ ∀ x ∈ X ∀ f f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ ∀ f ∀ x ∈ X f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
17 impexp ⊢ f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ f : ℕ ⟶ X → f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
18 17 ralbii ⊢ ∀ x ∈ X f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ ∀ x ∈ X f : ℕ ⟶ X → f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
19 r19.21v ⊢ ∀ x ∈ X f : ℕ ⟶ X → f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ f : ℕ ⟶ X → ∀ x ∈ X f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
20 18 19 bitri ⊢ ∀ x ∈ X f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ f : ℕ ⟶ X → ∀ x ∈ X f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
21 df-ral ⊢ ∀ x ∈ X f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ ∀ x x ∈ X → f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
22 lmcl ⊢ J ∈ TopOn ⁡ X ∧ f ⇝t ⁡ J x → x ∈ X
23 2 22 sylan ⊢ φ ∧ f ⇝t ⁡ J x → x ∈ X
24 23 ex ⊢ φ → f ⇝t ⁡ J x → x ∈ X
25 24 pm4.71rd ⊢ φ → f ⇝t ⁡ J x ↔ x ∈ X ∧ f ⇝t ⁡ J x
26 25 imbi1d ⊢ φ → f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ x ∈ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
27 impexp ⊢ x ∈ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ x ∈ X → f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
28 26 27 syl6rbb ⊢ φ → x ∈ X → f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
29 28 albidv ⊢ φ → ∀ x x ∈ X → f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
30 21 29 syl5bb ⊢ φ → ∀ x ∈ X f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
31 30 imbi2d ⊢ φ → f : ℕ ⟶ X → ∀ x ∈ X f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ f : ℕ ⟶ X → ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
32 20 31 syl5bb ⊢ φ → ∀ x ∈ X f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ f : ℕ ⟶ X → ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
33 32 albidv ⊢ φ → ∀ f ∀ x ∈ X f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ ∀ f f : ℕ ⟶ X → ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
34 16 33 syl5bb ⊢ φ → ∀ x ∈ X ∀ f f : ℕ ⟶ X ∧ f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x ↔ ∀ f f : ℕ ⟶ X → ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x
35 7 15 34 3bitrd ⊢ φ → F ∈ J Cn K ↔ ∀ f f : ℕ ⟶ X → ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x