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 ⊢ ( 𝜑 → 𝐽 ∈ 1stω )
1stccnp.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
1stccnp.3 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
1stccn.7 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
Assertion 1stccn ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 1stccnp.1 ⊢ ( 𝜑 → 𝐽 ∈ 1stω )
2 1stccnp.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 1stccnp.3 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
4 1stccn.7 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
5 cncnp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) )
6 2 3 5 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) )
7 4 6 mpbirand ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) )
8 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
9 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ 1stω )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
13 9 10 11 12 1stccnp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )
14 8 13 mpbirand ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
15 14 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
16 ralcom4 ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑓 ∀ 𝑥 ∈ 𝑋 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) )
17 impexp ⊢ ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
18 17 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑓 : ℕ ⟶ 𝑋 → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
19 r19.21v ⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑓 : ℕ ⟶ 𝑋 → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ∈ 𝑋 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
20 18 19 bitri ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ∈ 𝑋 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
21 df-ral ⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑋 → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
22 lmcl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑋 )
23 2 22 sylan ⊢ ( ( 𝜑 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑋 )
24 23 ex ⊢ ( 𝜑 → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → 𝑥 ∈ 𝑋 ) )
25 24 pm4.71rd ⊢ ( 𝜑 → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) )
26 25 imbi1d ⊢ ( 𝜑 → ( ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
27 impexp ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝑋 → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
28 26 27 bitr2di ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
29 28 albidv ⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑋 → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
30 21 29 syl5bb ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) )
31 30 imbi2d ⊢ ( 𝜑 → ( ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ∈ 𝑋 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )
32 20 31 syl5bb ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )
33 32 albidv ⊢ ( 𝜑 → ( ∀ 𝑓 ∀ 𝑥 ∈ 𝑋 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )
34 16 33 syl5bb ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )
35 7 15 34 3bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )