ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnntr GIF version
Theorem cnntr 13728
Description: Continuity in terms of interior. (Contributed by Jeff Hankins, 2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
Assertion
Ref Expression
cnntr ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝒫 π‘Œ(◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)))))
Distinct variable groups:   π‘₯,𝐹   π‘₯,𝐽   π‘₯,𝐾   π‘₯,𝑋   π‘₯,π‘Œ
Proof of Theorem cnntr
StepHypRef Expression
1 cnf2 13708 . . . 4 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) β†’ 𝐹:π‘‹βŸΆπ‘Œ)
213expia 1205 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) β†’ 𝐹:π‘‹βŸΆπ‘Œ))
3 elpwi 3585 . . . . . . 7 (π‘₯ ∈ 𝒫 π‘Œ β†’ π‘₯ βŠ† π‘Œ)
43adantl 277 . . . . . 6 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ π‘₯ ∈ 𝒫 π‘Œ) β†’ π‘₯ βŠ† π‘Œ)
5 toponuni 13518 . . . . . . 7 (𝐾 ∈ (TopOnβ€˜π‘Œ) β†’ π‘Œ = βˆͺ 𝐾)
65ad2antlr 489 . . . . . 6 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ π‘₯ ∈ 𝒫 π‘Œ) β†’ π‘Œ = βˆͺ 𝐾)
74, 6sseqtrd 3194 . . . . 5 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ π‘₯ ∈ 𝒫 π‘Œ) β†’ π‘₯ βŠ† βˆͺ 𝐾)
8 eqid 2177 . . . . . . 7 βˆͺ 𝐾 = βˆͺ 𝐾
98cnntri 13727 . . . . . 6 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ π‘₯ βŠ† βˆͺ 𝐾) β†’ (◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)))
109expcom 116 . . . . 5 (π‘₯ βŠ† βˆͺ 𝐾 β†’ (𝐹 ∈ (𝐽 Cn 𝐾) β†’ (◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))))
117, 10syl 14 . . . 4 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ π‘₯ ∈ 𝒫 π‘Œ) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) β†’ (◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))))
1211ralrimdva 2557 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) β†’ βˆ€π‘₯ ∈ 𝒫 π‘Œ(◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))))
132, 12jcad 307 . 2 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) β†’ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝒫 π‘Œ(◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)))))
14 toponss 13529 . . . . . . . . . 10 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ π‘₯ βŠ† π‘Œ)
15 velpw 3583 . . . . . . . . . 10 (π‘₯ ∈ 𝒫 π‘Œ ↔ π‘₯ βŠ† π‘Œ)
1614, 15sylibr 134 . . . . . . . . 9 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ π‘₯ ∈ 𝒫 π‘Œ)
1716ex 115 . . . . . . . 8 (𝐾 ∈ (TopOnβ€˜π‘Œ) β†’ (π‘₯ ∈ 𝐾 β†’ π‘₯ ∈ 𝒫 π‘Œ))
1817ad2antlr 489 . . . . . . 7 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ (π‘₯ ∈ 𝐾 β†’ π‘₯ ∈ 𝒫 π‘Œ))
1918imim1d 75 . . . . . 6 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ ((π‘₯ ∈ 𝒫 π‘Œ β†’ (◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))) β†’ (π‘₯ ∈ 𝐾 β†’ (◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)))))
20 topontop 13517 . . . . . . . . . . 11 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
2120ad3antrrr 492 . . . . . . . . . 10 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ 𝐽 ∈ Top)
22 cnvimass 4992 . . . . . . . . . . 11 (◑𝐹 β€œ π‘₯) βŠ† dom 𝐹
23 fdm 5372 . . . . . . . . . . . . 13 (𝐹:π‘‹βŸΆπ‘Œ β†’ dom 𝐹 = 𝑋)
2423ad2antlr 489 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ dom 𝐹 = 𝑋)
25 toponuni 13518 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
2625ad3antrrr 492 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ 𝑋 = βˆͺ 𝐽)
2724, 26eqtrd 2210 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ dom 𝐹 = βˆͺ 𝐽)
2822, 27sseqtrid 3206 . . . . . . . . . 10 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ (◑𝐹 β€œ π‘₯) βŠ† βˆͺ 𝐽)
29 eqid 2177 . . . . . . . . . . 11 βˆͺ 𝐽 = βˆͺ 𝐽
3029ntrss2 13624 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (◑𝐹 β€œ π‘₯) βŠ† βˆͺ 𝐽) β†’ ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) βŠ† (◑𝐹 β€œ π‘₯))
3121, 28, 30syl2anc 411 . . . . . . . . 9 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) βŠ† (◑𝐹 β€œ π‘₯))
32 eqss 3171 . . . . . . . . . 10 (((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) = (◑𝐹 β€œ π‘₯) ↔ (((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) βŠ† (◑𝐹 β€œ π‘₯) ∧ (◑𝐹 β€œ π‘₯) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))))
3332baib 919 . . . . . . . . 9 (((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) βŠ† (◑𝐹 β€œ π‘₯) β†’ (((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) = (◑𝐹 β€œ π‘₯) ↔ (◑𝐹 β€œ π‘₯) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))))
3431, 33syl 14 . . . . . . . 8 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ (((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) = (◑𝐹 β€œ π‘₯) ↔ (◑𝐹 β€œ π‘₯) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))))
3529isopn3 13628 . . . . . . . . 9 ((𝐽 ∈ Top ∧ (◑𝐹 β€œ π‘₯) βŠ† βˆͺ 𝐽) β†’ ((◑𝐹 β€œ π‘₯) ∈ 𝐽 ↔ ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) = (◑𝐹 β€œ π‘₯)))
3621, 28, 35syl2anc 411 . . . . . . . 8 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ ((◑𝐹 β€œ π‘₯) ∈ 𝐽 ↔ ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) = (◑𝐹 β€œ π‘₯)))
37 topontop 13517 . . . . . . . . . . . 12 (𝐾 ∈ (TopOnβ€˜π‘Œ) β†’ 𝐾 ∈ Top)
3837ad3antlr 493 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ 𝐾 ∈ Top)
39 isopn3i 13638 . . . . . . . . . . 11 ((𝐾 ∈ Top ∧ π‘₯ ∈ 𝐾) β†’ ((intβ€˜πΎ)β€˜π‘₯) = π‘₯)
4038, 39sylancom 420 . . . . . . . . . 10 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ ((intβ€˜πΎ)β€˜π‘₯) = π‘₯)
4140imaeq2d 4971 . . . . . . . . 9 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ (◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) = (◑𝐹 β€œ π‘₯))
4241sseq1d 3185 . . . . . . . 8 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ ((◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) ↔ (◑𝐹 β€œ π‘₯) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))))
4334, 36, 423bitr4rd 221 . . . . . . 7 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘₯ ∈ 𝐾) β†’ ((◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) ↔ (◑𝐹 β€œ π‘₯) ∈ 𝐽))
4443pm5.74da 443 . . . . . 6 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ ((π‘₯ ∈ 𝐾 β†’ (◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))) ↔ (π‘₯ ∈ 𝐾 β†’ (◑𝐹 β€œ π‘₯) ∈ 𝐽)))
4519, 44sylibd 149 . . . . 5 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ ((π‘₯ ∈ 𝒫 π‘Œ β†’ (◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))) β†’ (π‘₯ ∈ 𝐾 β†’ (◑𝐹 β€œ π‘₯) ∈ 𝐽)))
4645ralimdv2 2547 . . . 4 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ (βˆ€π‘₯ ∈ 𝒫 π‘Œ(◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)) β†’ βˆ€π‘₯ ∈ 𝐾 (◑𝐹 β€œ π‘₯) ∈ 𝐽))
4746imdistanda 448 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ ((𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝒫 π‘Œ(◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))) β†’ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝐾 (◑𝐹 β€œ π‘₯) ∈ 𝐽)))
48 iscn 13700 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝐾 (◑𝐹 β€œ π‘₯) ∈ 𝐽)))
4947, 48sylibrd 169 . 2 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ ((𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝒫 π‘Œ(◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯))) β†’ 𝐹 ∈ (𝐽 Cn 𝐾)))
5013, 49impbid 129 1 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝒫 π‘Œ(◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)))))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  βˆ€wral 2455   βŠ† wss 3130  π’« cpw 3576  βˆͺ cuni 3810  β—‘ccnv 4626  dom cdm 4627   β€œ cima 4630  βŸΆwf 5213  β€˜cfv 5217  (class class class)co 5875  Topctop 13500  TopOnctopon 13513  intcnt 13596   Cn ccn 13688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-map 6650  df-top 13501  df-topon 13514  df-ntr 13599  df-cn 13691
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator