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 𝐾 ) ‘ 𝐴 ) )