Metamath Proof Explorer


Theorem cnpresti

Description: One direction of cnprest under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Hypothesis cnprest.1 𝑋 = 𝐽
Assertion cnpresti ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝐹𝐴 ) ∈ ( ( ( 𝐽t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 cnprest.1 𝑋 = 𝐽
2 eqid 𝐾 = 𝐾
3 1 2 cnpf ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐹 : 𝑋 𝐾 )
4 3 3ad2ant3 ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 𝐾 )
5 simp1 ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐴𝑋 )
6 4 5 fssresd ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝐹𝐴 ) : 𝐴 𝐾 )
7 simpl2 ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦𝐾 ) → 𝑃𝐴 )
8 7 fvresd ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦𝐾 ) → ( ( 𝐹𝐴 ) ‘ 𝑃 ) = ( 𝐹𝑃 ) )
9 8 eleq1d ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦𝐾 ) → ( ( ( 𝐹𝐴 ) ‘ 𝑃 ) ∈ 𝑦 ↔ ( 𝐹𝑃 ) ∈ 𝑦 ) )
10 cnpimaex ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝑦𝐾 ∧ ( 𝐹𝑃 ) ∈ 𝑦 ) → ∃ 𝑥𝐽 ( 𝑃𝑥 ∧ ( 𝐹𝑥 ) ⊆ 𝑦 ) )
11 10 3expia ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝑦𝐾 ) → ( ( 𝐹𝑃 ) ∈ 𝑦 → ∃ 𝑥𝐽 ( 𝑃𝑥 ∧ ( 𝐹𝑥 ) ⊆ 𝑦 ) ) )
12 11 3ad2antl3 ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦𝐾 ) → ( ( 𝐹𝑃 ) ∈ 𝑦 → ∃ 𝑥𝐽 ( 𝑃𝑥 ∧ ( 𝐹𝑥 ) ⊆ 𝑦 ) ) )
13 idd ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝑃𝑥𝑃𝑥 ) )
14 simp2 ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑃𝐴 )
15 13 14 jctird ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝑃𝑥 → ( 𝑃𝑥𝑃𝐴 ) ) )
16 elin ( 𝑃 ∈ ( 𝑥𝐴 ) ↔ ( 𝑃𝑥𝑃𝐴 ) )
17 15 16 syl6ibr ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝑃𝑥𝑃 ∈ ( 𝑥𝐴 ) ) )
18 inss1 ( 𝑥𝐴 ) ⊆ 𝑥
19 imass2 ( ( 𝑥𝐴 ) ⊆ 𝑥 → ( 𝐹 “ ( 𝑥𝐴 ) ) ⊆ ( 𝐹𝑥 ) )
20 18 19 ax-mp ( 𝐹 “ ( 𝑥𝐴 ) ) ⊆ ( 𝐹𝑥 )
21 id ( ( 𝐹𝑥 ) ⊆ 𝑦 → ( 𝐹𝑥 ) ⊆ 𝑦 )
22 20 21 sstrid ( ( 𝐹𝑥 ) ⊆ 𝑦 → ( 𝐹 “ ( 𝑥𝐴 ) ) ⊆ 𝑦 )
23 17 22 anim12d1 ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( ( 𝑃𝑥 ∧ ( 𝐹𝑥 ) ⊆ 𝑦 ) → ( 𝑃 ∈ ( 𝑥𝐴 ) ∧ ( 𝐹 “ ( 𝑥𝐴 ) ) ⊆ 𝑦 ) ) )
24 23 reximdv ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( ∃ 𝑥𝐽 ( 𝑃𝑥 ∧ ( 𝐹𝑥 ) ⊆ 𝑦 ) → ∃ 𝑥𝐽 ( 𝑃 ∈ ( 𝑥𝐴 ) ∧ ( 𝐹 “ ( 𝑥𝐴 ) ) ⊆ 𝑦 ) ) )
25 vex 𝑥 ∈ V
26 25 inex1 ( 𝑥𝐴 ) ∈ V
27 26 a1i ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑥𝐽 ) → ( 𝑥𝐴 ) ∈ V )
28 cnptop1 ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐽 ∈ Top )
29 28 3ad2ant3 ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐽 ∈ Top )
30 29 uniexd ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐽 ∈ V )
31 5 1 sseqtrdi ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐴 𝐽 )
32 30 31 ssexd ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐴 ∈ V )
33 elrest ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ V ) → ( 𝑧 ∈ ( 𝐽t 𝐴 ) ↔ ∃ 𝑥𝐽 𝑧 = ( 𝑥𝐴 ) ) )
34 29 32 33 syl2anc ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝑧 ∈ ( 𝐽t 𝐴 ) ↔ ∃ 𝑥𝐽 𝑧 = ( 𝑥𝐴 ) ) )
35 simpr ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑧 = ( 𝑥𝐴 ) ) → 𝑧 = ( 𝑥𝐴 ) )
36 35 eleq2d ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑧 = ( 𝑥𝐴 ) ) → ( 𝑃𝑧𝑃 ∈ ( 𝑥𝐴 ) ) )
37 35 imaeq2d ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑧 = ( 𝑥𝐴 ) ) → ( ( 𝐹𝐴 ) “ 𝑧 ) = ( ( 𝐹𝐴 ) “ ( 𝑥𝐴 ) ) )
38 inss2 ( 𝑥𝐴 ) ⊆ 𝐴
39 resima2 ( ( 𝑥𝐴 ) ⊆ 𝐴 → ( ( 𝐹𝐴 ) “ ( 𝑥𝐴 ) ) = ( 𝐹 “ ( 𝑥𝐴 ) ) )
40 38 39 ax-mp ( ( 𝐹𝐴 ) “ ( 𝑥𝐴 ) ) = ( 𝐹 “ ( 𝑥𝐴 ) )
41 37 40 eqtrdi ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑧 = ( 𝑥𝐴 ) ) → ( ( 𝐹𝐴 ) “ 𝑧 ) = ( 𝐹 “ ( 𝑥𝐴 ) ) )
42 41 sseq1d ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑧 = ( 𝑥𝐴 ) ) → ( ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ↔ ( 𝐹 “ ( 𝑥𝐴 ) ) ⊆ 𝑦 ) )
43 36 42 anbi12d ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑧 = ( 𝑥𝐴 ) ) → ( ( 𝑃𝑧 ∧ ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ↔ ( 𝑃 ∈ ( 𝑥𝐴 ) ∧ ( 𝐹 “ ( 𝑥𝐴 ) ) ⊆ 𝑦 ) ) )
44 27 34 43 rexxfr2d ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( ∃ 𝑧 ∈ ( 𝐽t 𝐴 ) ( 𝑃𝑧 ∧ ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ↔ ∃ 𝑥𝐽 ( 𝑃 ∈ ( 𝑥𝐴 ) ∧ ( 𝐹 “ ( 𝑥𝐴 ) ) ⊆ 𝑦 ) ) )
45 24 44 sylibrd ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( ∃ 𝑥𝐽 ( 𝑃𝑥 ∧ ( 𝐹𝑥 ) ⊆ 𝑦 ) → ∃ 𝑧 ∈ ( 𝐽t 𝐴 ) ( 𝑃𝑧 ∧ ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
46 45 adantr ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦𝐾 ) → ( ∃ 𝑥𝐽 ( 𝑃𝑥 ∧ ( 𝐹𝑥 ) ⊆ 𝑦 ) → ∃ 𝑧 ∈ ( 𝐽t 𝐴 ) ( 𝑃𝑧 ∧ ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
47 12 46 syld ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦𝐾 ) → ( ( 𝐹𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽t 𝐴 ) ( 𝑃𝑧 ∧ ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
48 9 47 sylbid ( ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦𝐾 ) → ( ( ( 𝐹𝐴 ) ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽t 𝐴 ) ( 𝑃𝑧 ∧ ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
49 48 ralrimiva ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ∀ 𝑦𝐾 ( ( ( 𝐹𝐴 ) ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽t 𝐴 ) ( 𝑃𝑧 ∧ ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
50 1 toptopon ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
51 29 50 sylib ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
52 resttopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴𝑋 ) → ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
53 51 5 52 syl2anc ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
54 cnptop2 ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐾 ∈ Top )
55 54 3ad2ant3 ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐾 ∈ Top )
56 2 toptopon ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
57 55 56 sylib ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
58 iscnp ( ( ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝐾 ) ∧ 𝑃𝐴 ) → ( ( 𝐹𝐴 ) ∈ ( ( ( 𝐽t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐹𝐴 ) : 𝐴 𝐾 ∧ ∀ 𝑦𝐾 ( ( ( 𝐹𝐴 ) ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽t 𝐴 ) ( 𝑃𝑧 ∧ ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
59 53 57 14 58 syl3anc ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( ( 𝐹𝐴 ) ∈ ( ( ( 𝐽t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐹𝐴 ) : 𝐴 𝐾 ∧ ∀ 𝑦𝐾 ( ( ( 𝐹𝐴 ) ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝐽t 𝐴 ) ( 𝑃𝑧 ∧ ( ( 𝐹𝐴 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
60 6 49 59 mpbir2and ( ( 𝐴𝑋𝑃𝐴𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝐹𝐴 ) ∈ ( ( ( 𝐽t 𝐴 ) CnP 𝐾 ) ‘ 𝑃 ) )