Metamath Proof Explorer

Theorem cncnp

Description: A continuous function is continuous at all points. Theorem 7.2(g) of Munkres p. 107. (Contributed by NM, 15-May-2007) (Proof shortened by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cncnp ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
2 1 simprbda ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 3 cncnpi ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) )
5 4 ralrimiva ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ∀ 𝑥 ∈ ∪ 𝐽 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) )
6 5 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ ∪ 𝐽 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) )
7 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
8 7 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑋 = ∪ 𝐽 )
9 8 raleqdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ∪ 𝐽 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) )
10 6 9 mpbird ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) )
11 2 10 jca ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) )
12 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
13 cnvimass ⊢ ( ◡ 𝐹 “ 𝑦 ) ⊆ dom 𝐹
14 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
15 14 adantl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → dom 𝐹 = 𝑋 )
16 13 15 sseqtrid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 )
17 ssralv ⊢ ( ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) )
18 16 17 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) )
19 simprr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) )
20 simpllr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → 𝑦 ∈ 𝐾 )
21 ffn ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝐹 Fn 𝑋 )
22 21 ad2antlr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → 𝐹 Fn 𝑋 )
23 simprl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) )
24 elpreima ⊢ ( 𝐹 Fn 𝑋 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑦 ) ) )
25 24 simplbda ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑦 )
26 22 23 25 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑦 )
27 cnpimaex ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ∧ 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑦 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑦 ) )
28 19 20 26 27 syl3anc ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑦 ) )
29 simpllr ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐽 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
30 29 ffund ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐽 ) → Fun 𝐹 )
31 simp-4l ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
32 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑢 ∈ 𝐽 ) → 𝑢 ⊆ 𝑋 )
33 31 32 sylan ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐽 ) → 𝑢 ⊆ 𝑋 )
34 29 14 syl ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐽 ) → dom 𝐹 = 𝑋 )
35 33 34 sseqtrrd ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐽 ) → 𝑢 ⊆ dom 𝐹 )
36 funimass3 ⊢ ( ( Fun 𝐹 ∧ 𝑢 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑢 ) ⊆ 𝑦 ↔ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
37 30 35 36 syl2anc ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑢 ) ⊆ 𝑦 ↔ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
38 37 anbi2d ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑢 ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑦 ) ↔ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
39 38 rexbidva ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → ( ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑦 ) ↔ ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
40 28 39 mpbid ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
41 40 expr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
42 41 ralimdva ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
43 18 42 syld ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
44 43 impr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
45 44 an32s ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐾 ) → ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
46 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
47 46 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐾 ) → 𝐽 ∈ Top )
48 eltop2 ⊢ ( 𝐽 ∈ Top → ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
49 47 48 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( ◡ 𝐹 “ 𝑦 ) ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
50 45 49 mpbird ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
51 50 ralrimiva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
52 1 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
53 12 51 52 mpbir2and ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
54 11 53 impbida ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) )