This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnprest2

Description: Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses cnprest.1 ⊢ 𝑋 = ∪ 𝐽
cnprest.2 ⊢ 𝑌 = ∪ 𝐾
Assertion cnprest2 ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 cnprest.1 ⊢ 𝑋 = ∪ 𝐽
2 cnprest.2 ⊢ 𝑌 = ∪ 𝐾
3 cnptop1 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐽 ∈ Top )
4 1 cnprcl ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ 𝑋 )
5 3 4 jca ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) )
6 5 a1i ⊢ ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) )
7 cnptop1 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) → 𝐽 ∈ Top )
8 1 cnprcl ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) → 𝑃 ∈ 𝑋 )
9 7 8 jca ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) )
10 9 a1i ⊢ ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) )
11 simpl2 ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ 𝐵 )
12 simprr ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝑃 ∈ 𝑋 )
13 11 12 ffvelcdmd ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝐵 )
14 13 biantrud ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐵 ) ) )
15 elin ⊢ ( ( 𝐹 ‘ 𝑃 ) ∈ ( 𝑥 ∩ 𝐵 ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐵 ) )
16 14 15 bitr4di ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 ↔ ( 𝐹 ‘ 𝑃 ) ∈ ( 𝑥 ∩ 𝐵 ) ) )
17 imassrn ⊢ ( 𝐹 “ 𝑦 ) ⊆ ran 𝐹
18 11 frnd ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ran 𝐹 ⊆ 𝐵 )
19 17 18 sstrid ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝐹 “ 𝑦 ) ⊆ 𝐵 )
20 19 biantrud ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ↔ ( ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐵 ) ) )
21 ssin ⊢ ( ( ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐵 ) ↔ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) )
22 20 21 bitrdi ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ↔ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) )
23 22 anbi2d ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ↔ ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) ) )
24 23 rexbidv ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) ) )
25 16 24 imbi12d ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ ( 𝑥 ∩ 𝐵 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) ) ) )
26 25 ralbidv ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ ( 𝑥 ∩ 𝐵 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) ) ) )
27 vex ⊢ 𝑥 ∈ V
28 27 inex1 ⊢ ( 𝑥 ∩ 𝐵 ) ∈ V
29 28 a1i ⊢ ( ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑥 ∩ 𝐵 ) ∈ V )
30 simpl1 ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝐾 ∈ Top )
31 uniexg ⊢ ( 𝐾 ∈ Top → ∪ 𝐾 ∈ V )
32 2 31 eqeltrid ⊢ ( 𝐾 ∈ Top → 𝑌 ∈ V )
33 30 32 syl ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝑌 ∈ V )
34 simpl3 ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝐵 ⊆ 𝑌 )
35 33 34 ssexd ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝐵 ∈ V )
36 elrest ⊢ ( ( 𝐾 ∈ Top ∧ 𝐵 ∈ V ) → ( 𝑧 ∈ ( 𝐾 ↾t 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐾 𝑧 = ( 𝑥 ∩ 𝐵 ) ) )
37 30 35 36 syl2anc ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝑧 ∈ ( 𝐾 ↾t 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐾 𝑧 = ( 𝑥 ∩ 𝐵 ) ) )
38 eleq2 ⊢ ( 𝑧 = ( 𝑥 ∩ 𝐵 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑃 ) ∈ ( 𝑥 ∩ 𝐵 ) ) )
39 sseq2 ⊢ ( 𝑧 = ( 𝑥 ∩ 𝐵 ) → ( ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ↔ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) )
40 39 anbi2d ⊢ ( 𝑧 = ( 𝑥 ∩ 𝐵 ) → ( ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ) ↔ ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) ) )
41 40 rexbidv ⊢ ( 𝑧 = ( 𝑥 ∩ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) ) )
42 38 41 imbi12d ⊢ ( 𝑧 = ( 𝑥 ∩ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ ( 𝑥 ∩ 𝐵 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) ) ) )
43 42 adantl ⊢ ( ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ ( 𝑥 ∩ 𝐵 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) ) ) )
44 29 37 43 ralxfr2d ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ∀ 𝑧 ∈ ( 𝐾 ↾t 𝐵 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ ( 𝑥 ∩ 𝐵 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) ) ) )
45 26 44 bitr4d ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ↔ ∀ 𝑧 ∈ ( 𝐾 ↾t 𝐵 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ) ) ) )
46 11 34 fssd ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
47 simprl ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝐽 ∈ Top )
48 1 2 iscnp2 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ) ) )
49 48 baib ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ) ) )
50 47 30 12 49 syl3anc ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ) ) )
51 46 50 mpbirand ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ) )
52 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
53 47 52 sylib ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
54 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
55 30 54 sylib ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
56 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐾 ↾t 𝐵 ) ∈ ( TopOn ‘ 𝐵 ) )
57 55 34 56 syl2anc ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝐾 ↾t 𝐵 ) ∈ ( TopOn ‘ 𝐵 ) )
58 iscnp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐾 ↾t 𝐵 ) ∈ ( TopOn ‘ 𝐵 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝐵 ∧ ∀ 𝑧 ∈ ( 𝐾 ↾t 𝐵 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ) ) ) ) )
59 53 57 12 58 syl3anc ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝐵 ∧ ∀ 𝑧 ∈ ( 𝐾 ↾t 𝐵 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ) ) ) ) )
60 11 59 mpbirand ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) ↔ ∀ 𝑧 ∈ ( 𝐾 ↾t 𝐵 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑧 ) ) ) )
61 45 51 60 3bitr4d ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) ) )
62 61 ex ⊢ ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) ) ) )
63 6 10 62 pm5.21ndd ⊢ ( ( 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ 𝐹 ∈ ( ( 𝐽 CnP ( 𝐾 ↾t 𝐵 ) ) ‘ 𝑃 ) ) )