Metamath Proof Explorer

Theorem cnprest

Description: Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 cnprest.1 ⊢ 𝑋 = ∪ 𝐽
2 cnprest.2 ⊢ 𝑌 = ∪ 𝐾
3 cnptop2 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐾 ∈ Top )
4 3 a1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐾 ∈ Top ) )
5 cnptop2 ⊢ ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( ( 𝐽 ↾t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) → 𝐾 ∈ Top )
6 5 a1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( ( 𝐽 ↾t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) → 𝐾 ∈ Top ) )
7 1 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 )
8 7 3ad2ant1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 )
9 simp2l ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
10 8 9 sseldd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝑃 ∈ 𝐴 )
11 10 fvresd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑃 ) = ( 𝐹 ‘ 𝑃 ) )
12 11 eqcomd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝐹 ‘ 𝑃 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑃 ) )
13 12 eleq1d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ↔ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑃 ) ∈ 𝑦 ) )
14 inss1 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥
15 imass2 ⊢ ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 → ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ ( 𝐹 “ 𝑥 ) )
16 sstr2 ⊢ ( ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ ( 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑥 ) ⊆ 𝑦 → ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) )
17 14 15 16 mp2b ⊢ ( ( 𝐹 “ 𝑥 ) ⊆ 𝑦 → ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 )
18 17 anim2i ⊢ ( ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) )
19 18 reximi ⊢ ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) )
20 simp1l ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝐽 ∈ Top )
21 1 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 )
22 21 3ad2ant1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 )
23 inopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 ) → ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ 𝐽 )
24 23 3com23 ⊢ ( ( 𝐽 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ 𝐽 )
25 24 3expia ⊢ ( ( 𝐽 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 ) → ( 𝑥 ∈ 𝐽 → ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ 𝐽 ) )
26 20 22 25 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝑥 ∈ 𝐽 → ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ 𝐽 ) )
27 elin ⊢ ( 𝑃 ∈ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ↔ ( 𝑃 ∈ 𝑥 ∧ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
28 27 simplbi2com ⊢ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) → ( 𝑃 ∈ 𝑥 → 𝑃 ∈ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) )
29 9 28 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝑃 ∈ 𝑥 → 𝑃 ∈ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) )
30 sslin ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 → ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( 𝑥 ∩ 𝐴 ) )
31 8 30 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( 𝑥 ∩ 𝐴 ) )
32 imass2 ⊢ ( ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( 𝑥 ∩ 𝐴 ) → ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) )
33 31 32 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) )
34 sstr2 ⊢ ( ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) → ( ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 → ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ 𝑦 ) )
35 33 34 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 → ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ 𝑦 ) )
36 29 35 anim12d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) → ( 𝑃 ∈ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∧ ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ 𝑦 ) ) )
37 26 36 anim12d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) ) → ( ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ 𝐽 ∧ ( 𝑃 ∈ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∧ ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ 𝑦 ) ) ) )
38 eleq2 ⊢ ( 𝑧 = ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) → ( 𝑃 ∈ 𝑧 ↔ 𝑃 ∈ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) )
39 imaeq2 ⊢ ( 𝑧 = ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) → ( 𝐹 “ 𝑧 ) = ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) )
40 39 sseq1d ⊢ ( 𝑧 = ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ↔ ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ 𝑦 ) )
41 38 40 anbi12d ⊢ ( 𝑧 = ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ↔ ( 𝑃 ∈ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∧ ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ 𝑦 ) ) )
42 41 rspcev ⊢ ( ( ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ 𝐽 ∧ ( 𝑃 ∈ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∧ ( 𝐹 “ ( 𝑥 ∩ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) )
43 37 42 syl6 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) )
44 43 expdimp ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) )
45 44 rexlimdva ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) )
46 eleq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑃 ∈ 𝑧 ↔ 𝑃 ∈ 𝑥 ) )
47 imaeq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 “ 𝑧 ) = ( 𝐹 “ 𝑥 ) )
48 47 sseq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ↔ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) )
49 46 48 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ↔ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) )
50 49 cbvrexvw ⊢ ( ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) )
51 45 50 imbitrdi ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) )
52 19 51 impbid2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) ) )
53 vex ⊢ 𝑥 ∈ V
54 53 inex1 ⊢ ( 𝑥 ∩ 𝐴 ) ∈ V
55 54 a1i ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ 𝐴 ) ∈ V )
56 20 uniexd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ∪ 𝐽 ∈ V )
57 simp1r ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝐴 ⊆ 𝑋 )
58 57 1 sseqtrdi ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝐴 ⊆ ∪ 𝐽 )
59 56 58 ssexd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝐴 ∈ V )
60 elrest ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ V ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐽 𝑧 = ( 𝑥 ∩ 𝐴 ) ) )
61 20 59 60 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐽 𝑧 = ( 𝑥 ∩ 𝐴 ) ) )
62 eleq2 ⊢ ( 𝑧 = ( 𝑥 ∩ 𝐴 ) → ( 𝑃 ∈ 𝑧 ↔ 𝑃 ∈ ( 𝑥 ∩ 𝐴 ) ) )
63 elin ⊢ ( 𝑃 ∈ ( 𝑥 ∩ 𝐴 ) ↔ ( 𝑃 ∈ 𝑥 ∧ 𝑃 ∈ 𝐴 ) )
64 63 rbaib ⊢ ( 𝑃 ∈ 𝐴 → ( 𝑃 ∈ ( 𝑥 ∩ 𝐴 ) ↔ 𝑃 ∈ 𝑥 ) )
65 10 64 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝑃 ∈ ( 𝑥 ∩ 𝐴 ) ↔ 𝑃 ∈ 𝑥 ) )
66 62 65 sylan9bbr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) ∧ 𝑧 = ( 𝑥 ∩ 𝐴 ) ) → ( 𝑃 ∈ 𝑧 ↔ 𝑃 ∈ 𝑥 ) )
67 simpr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) ∧ 𝑧 = ( 𝑥 ∩ 𝐴 ) ) → 𝑧 = ( 𝑥 ∩ 𝐴 ) )
68 67 imaeq2d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) ∧ 𝑧 = ( 𝑥 ∩ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) = ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑥 ∩ 𝐴 ) ) )
69 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
70 resima2 ⊢ ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑥 ∩ 𝐴 ) ) = ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) )
71 69 70 ax-mp ⊢ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑥 ∩ 𝐴 ) ) = ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) )
72 68 71 eqtrdi ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) ∧ 𝑧 = ( 𝑥 ∩ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) = ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) )
73 72 sseq1d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) ∧ 𝑧 = ( 𝑥 ∩ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) ⊆ 𝑦 ↔ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) )
74 66 73 anbi12d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) ∧ 𝑧 = ( 𝑥 ∩ 𝐴 ) ) → ( ( 𝑃 ∈ 𝑧 ∧ ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ↔ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) ) )
75 55 61 74 rexxfr2d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ∃ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑃 ∈ 𝑧 ∧ ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝑦 ) ) )
76 52 75 bitr4d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ↔ ∃ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑃 ∈ 𝑧 ∧ ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
77 13 76 imbi12d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ↔ ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑃 ∈ 𝑧 ∧ ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) )
78 77 ralbidv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐾 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑃 ∈ 𝑧 ∧ ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) )
79 simp2r ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝐹 : 𝑋 ⟶ 𝑌 )
80 simp3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝐾 ∈ Top )
81 57 10 sseldd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝑃 ∈ 𝑋 )
82 1 2 iscnp2 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
83 82 baib ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
84 20 80 81 83 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
85 79 84 mpbirand ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
86 79 57 fssresd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝑌 )
87 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
88 20 87 sylib ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
89 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
90 88 57 89 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
91 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
92 80 91 sylib ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
93 iscnp ⊢ ( ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( ( 𝐽 ↾t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑃 ∈ 𝑧 ∧ ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
94 90 92 10 93 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( ( 𝐽 ↾t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑃 ∈ 𝑧 ∧ ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
95 86 94 mpbirand ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( ( 𝐽 ↾t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) ↔ ∀ 𝑦 ∈ 𝐾 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑃 ∈ 𝑧 ∧ ( ( 𝐹 ↾ 𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) )
96 78 85 95 3bitr4d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐾 ∈ Top ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 ↾ 𝐴 ) ∈ ( ( ( 𝐽 ↾t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) ) )
97 96 3expia ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) → ( 𝐾 ∈ Top → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 ↾ 𝐴 ) ∈ ( ( ( 𝐽 ↾t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) ) ) )
98 4 6 97 pm5.21ndd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 ↾ 𝐴 ) ∈ ( ( ( 𝐽 ↾t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) ) )