Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnpresti Structured version   Visualization version   GIF version

Theorem cnpresti 21896
 Description: One direction of cnprest 21897 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.)
Hypothesis
Ref Expression
cnprest.1 𝑋 = 𝐽
Assertion
Ref Expression
cnpresti ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹𝐴) ∈ (((𝐽t 𝐴) CnP 𝐾)‘𝑃))

Proof of Theorem cnpresti
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnprest.1 . . . . 5 𝑋 = 𝐽
2 eqid 2824 . . . . 5 𝐾 = 𝐾
31, 2cnpf 21855 . . . 4 (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐹:𝑋 𝐾)
433ad2ant3 1132 . . 3 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋 𝐾)
5 simp1 1133 . . 3 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐴𝑋)
64, 5fssresd 6535 . 2 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹𝐴):𝐴 𝐾)
7 simpl2 1189 . . . . . 6 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦𝐾) → 𝑃𝐴)
87fvresd 6681 . . . . 5 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦𝐾) → ((𝐹𝐴)‘𝑃) = (𝐹𝑃))
98eleq1d 2900 . . . 4 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦𝐾) → (((𝐹𝐴)‘𝑃) ∈ 𝑦 ↔ (𝐹𝑃) ∈ 𝑦))
10 cnpimaex 21864 . . . . . . 7 ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦) → ∃𝑥𝐽 (𝑃𝑥 ∧ (𝐹𝑥) ⊆ 𝑦))
11103expia 1118 . . . . . 6 ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝑦𝐾) → ((𝐹𝑃) ∈ 𝑦 → ∃𝑥𝐽 (𝑃𝑥 ∧ (𝐹𝑥) ⊆ 𝑦)))
12113ad2antl3 1184 . . . . 5 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦𝐾) → ((𝐹𝑃) ∈ 𝑦 → ∃𝑥𝐽 (𝑃𝑥 ∧ (𝐹𝑥) ⊆ 𝑦)))
13 idd 24 . . . . . . . . . . 11 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝑃𝑥𝑃𝑥))
14 simp2 1134 . . . . . . . . . . 11 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑃𝐴)
1513, 14jctird 530 . . . . . . . . . 10 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝑃𝑥 → (𝑃𝑥𝑃𝐴)))
16 elin 3935 . . . . . . . . . 10 (𝑃 ∈ (𝑥𝐴) ↔ (𝑃𝑥𝑃𝐴))
1715, 16syl6ibr 255 . . . . . . . . 9 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝑃𝑥𝑃 ∈ (𝑥𝐴)))
18 inss1 4190 . . . . . . . . . . 11 (𝑥𝐴) ⊆ 𝑥
19 imass2 5952 . . . . . . . . . . 11 ((𝑥𝐴) ⊆ 𝑥 → (𝐹 “ (𝑥𝐴)) ⊆ (𝐹𝑥))
2018, 19ax-mp 5 . . . . . . . . . 10 (𝐹 “ (𝑥𝐴)) ⊆ (𝐹𝑥)
21 id 22 . . . . . . . . . 10 ((𝐹𝑥) ⊆ 𝑦 → (𝐹𝑥) ⊆ 𝑦)
2220, 21sstrid 3964 . . . . . . . . 9 ((𝐹𝑥) ⊆ 𝑦 → (𝐹 “ (𝑥𝐴)) ⊆ 𝑦)
2317, 22anim12d1 612 . . . . . . . 8 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ((𝑃𝑥 ∧ (𝐹𝑥) ⊆ 𝑦) → (𝑃 ∈ (𝑥𝐴) ∧ (𝐹 “ (𝑥𝐴)) ⊆ 𝑦)))
2423reximdv 3265 . . . . . . 7 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (∃𝑥𝐽 (𝑃𝑥 ∧ (𝐹𝑥) ⊆ 𝑦) → ∃𝑥𝐽 (𝑃 ∈ (𝑥𝐴) ∧ (𝐹 “ (𝑥𝐴)) ⊆ 𝑦)))
25 vex 3483 . . . . . . . . . 10 𝑥 ∈ V
2625inex1 5207 . . . . . . . . 9 (𝑥𝐴) ∈ V
2726a1i 11 . . . . . . . 8 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑥𝐽) → (𝑥𝐴) ∈ V)
28 cnptop1 21850 . . . . . . . . . 10 (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top)
29283ad2ant3 1132 . . . . . . . . 9 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐽 ∈ Top)
3029uniexd 7462 . . . . . . . . . 10 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐽 ∈ V)
315, 1sseqtrdi 4003 . . . . . . . . . 10 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐴 𝐽)
3230, 31ssexd 5214 . . . . . . . . 9 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐴 ∈ V)
33 elrest 16701 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽t 𝐴) ↔ ∃𝑥𝐽 𝑧 = (𝑥𝐴)))
3429, 32, 33syl2anc 587 . . . . . . . 8 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝑧 ∈ (𝐽t 𝐴) ↔ ∃𝑥𝐽 𝑧 = (𝑥𝐴)))
35 simpr 488 . . . . . . . . . 10 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑧 = (𝑥𝐴)) → 𝑧 = (𝑥𝐴))
3635eleq2d 2901 . . . . . . . . 9 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑧 = (𝑥𝐴)) → (𝑃𝑧𝑃 ∈ (𝑥𝐴)))
3735imaeq2d 5916 . . . . . . . . . . 11 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑧 = (𝑥𝐴)) → ((𝐹𝐴) “ 𝑧) = ((𝐹𝐴) “ (𝑥𝐴)))
38 inss2 4191 . . . . . . . . . . . 12 (𝑥𝐴) ⊆ 𝐴
39 resima2 5875 . . . . . . . . . . . 12 ((𝑥𝐴) ⊆ 𝐴 → ((𝐹𝐴) “ (𝑥𝐴)) = (𝐹 “ (𝑥𝐴)))
4038, 39ax-mp 5 . . . . . . . . . . 11 ((𝐹𝐴) “ (𝑥𝐴)) = (𝐹 “ (𝑥𝐴))
4137, 40syl6eq 2875 . . . . . . . . . 10 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑧 = (𝑥𝐴)) → ((𝐹𝐴) “ 𝑧) = (𝐹 “ (𝑥𝐴)))
4241sseq1d 3984 . . . . . . . . 9 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑧 = (𝑥𝐴)) → (((𝐹𝐴) “ 𝑧) ⊆ 𝑦 ↔ (𝐹 “ (𝑥𝐴)) ⊆ 𝑦))
4336, 42anbi12d 633 . . . . . . . 8 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑧 = (𝑥𝐴)) → ((𝑃𝑧 ∧ ((𝐹𝐴) “ 𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ (𝑥𝐴) ∧ (𝐹 “ (𝑥𝐴)) ⊆ 𝑦)))
4427, 34, 43rexxfr2d 5299 . . . . . . 7 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (∃𝑧 ∈ (𝐽t 𝐴)(𝑃𝑧 ∧ ((𝐹𝐴) “ 𝑧) ⊆ 𝑦) ↔ ∃𝑥𝐽 (𝑃 ∈ (𝑥𝐴) ∧ (𝐹 “ (𝑥𝐴)) ⊆ 𝑦)))
4524, 44sylibrd 262 . . . . . 6 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (∃𝑥𝐽 (𝑃𝑥 ∧ (𝐹𝑥) ⊆ 𝑦) → ∃𝑧 ∈ (𝐽t 𝐴)(𝑃𝑧 ∧ ((𝐹𝐴) “ 𝑧) ⊆ 𝑦)))
4645adantr 484 . . . . 5 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦𝐾) → (∃𝑥𝐽 (𝑃𝑥 ∧ (𝐹𝑥) ⊆ 𝑦) → ∃𝑧 ∈ (𝐽t 𝐴)(𝑃𝑧 ∧ ((𝐹𝐴) “ 𝑧) ⊆ 𝑦)))
4712, 46syld 47 . . . 4 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦𝐾) → ((𝐹𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽t 𝐴)(𝑃𝑧 ∧ ((𝐹𝐴) “ 𝑧) ⊆ 𝑦)))
489, 47sylbid 243 . . 3 (((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦𝐾) → (((𝐹𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽t 𝐴)(𝑃𝑧 ∧ ((𝐹𝐴) “ 𝑧) ⊆ 𝑦)))
4948ralrimiva 3177 . 2 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∀𝑦𝐾 (((𝐹𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽t 𝐴)(𝑃𝑧 ∧ ((𝐹𝐴) “ 𝑧) ⊆ 𝑦)))
501toptopon 21525 . . . . 5 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
5129, 50sylib 221 . . . 4 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐽 ∈ (TopOn‘𝑋))
52 resttopon 21769 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴𝑋) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
5351, 5, 52syl2anc 587 . . 3 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
54 cnptop2 21851 . . . . 5 (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top)
55543ad2ant3 1132 . . . 4 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐾 ∈ Top)
562toptopon 21525 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
5755, 56sylib 221 . . 3 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐾 ∈ (TopOn‘ 𝐾))
58 iscnp 21845 . . 3 (((𝐽t 𝐴) ∈ (TopOn‘𝐴) ∧ 𝐾 ∈ (TopOn‘ 𝐾) ∧ 𝑃𝐴) → ((𝐹𝐴) ∈ (((𝐽t 𝐴) CnP 𝐾)‘𝑃) ↔ ((𝐹𝐴):𝐴 𝐾 ∧ ∀𝑦𝐾 (((𝐹𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽t 𝐴)(𝑃𝑧 ∧ ((𝐹𝐴) “ 𝑧) ⊆ 𝑦)))))
5953, 57, 14, 58syl3anc 1368 . 2 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ((𝐹𝐴) ∈ (((𝐽t 𝐴) CnP 𝐾)‘𝑃) ↔ ((𝐹𝐴):𝐴 𝐾 ∧ ∀𝑦𝐾 (((𝐹𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽t 𝐴)(𝑃𝑧 ∧ ((𝐹𝐴) “ 𝑧) ⊆ 𝑦)))))
606, 49, 59mpbir2and 712 1 ((𝐴𝑋𝑃𝐴𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹𝐴) ∈ (((𝐽t 𝐴) CnP 𝐾)‘𝑃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115  ∀wral 3133  ∃wrex 3134  Vcvv 3480   ∩ cin 3918   ⊆ wss 3919  ∪ cuni 4824   ↾ cres 5544   “ cima 5545  ⟶wf 6339  ‘cfv 6343  (class class class)co 7149   ↾t crest 16694  Topctop 21501  TopOnctopon 21518   CnP ccnp 21833 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-oadd 8102  df-er 8285  df-map 8404  df-en 8506  df-fin 8509  df-fi 8872  df-rest 16696  df-topgen 16717  df-top 21502  df-topon 21519  df-bases 21554  df-cnp 21836 This theorem is referenced by:  efrlim  25558  cvmlift2lem11  32617
 Copyright terms: Public domain W3C validator