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 imbitrrdi ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑃 ∈ 𝐴 ∧ 𝐹 ∈ ( ( 𝐽 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 𝐾 ) ‘ 𝑃 ) )