Metamath Proof Explorer

Theorem cncnpi

Description: A continuous function is continuous at all points. One direction of Theorem 7.2(g) of Munkres p. 107. (Contributed by Raph Levien, 20-Nov-2006) (Proof shortened by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypothesis cnsscnp.1 ⊢ 𝑋 = ∪ 𝐽
Assertion cncnpi ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cnsscnp.1 ⊢ 𝑋 = ∪ 𝐽
2 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
3 1 2 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
4 3 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
5 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑦 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
6 5 ad2ant2r ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
7 simpr ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
8 7 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 ) ) → 𝐴 ∈ 𝑋 )
9 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 )
10 3 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 ) ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
11 ffn ⊢ ( 𝐹 : 𝑋 ⟶ ∪ 𝐾 → 𝐹 Fn 𝑋 )
12 elpreima ⊢ ( 𝐹 Fn 𝑋 → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝑦 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 ) ) )
13 10 11 12 3syl ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 ) ) → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝑦 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 ) ) )
14 8 9 13 mpbir2and ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 ) ) → 𝐴 ∈ ( ◡ 𝐹 “ 𝑦 ) )
15 eqimss ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → 𝑥 ⊆ ( ◡ 𝐹 “ 𝑦 ) )
16 15 biantrud ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐴 ∈ 𝑥 ↔ ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
17 eleq2 ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝑦 ) ) )
18 16 17 bitr3d ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝑦 ) ) )
19 18 rspcev ⊢ ( ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
20 6 14 19 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
21 20 expr ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
22 21 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
23 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
24 23 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ Top )
25 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
26 24 25 sylib ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
27 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
28 27 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐾 ∈ Top )
29 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
30 28 29 sylib ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
31 iscnp3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ ∪ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) )
32 26 30 7 31 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ ∪ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) )
33 4 22 32 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) )