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

Theorem iscncl 21549
Description: A characterization of a continuity function using closed sets. Theorem 1(d) of [BourbakiTop1] p. I.9. (Contributed by FL, 19-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
iscncl ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))))
Distinct variable groups:   𝑦,𝐹   𝑦,𝐽   𝑦,𝐾   𝑦,𝑋   𝑦,𝑌

Proof of Theorem iscncl
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 cnf2 21529 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋𝑌)
213expa 1109 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋𝑌)
3 cnclima 21548 . . . . 5 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (𝐹𝑦) ∈ (Clsd‘𝐽))
43ralrimiva 3147 . . . 4 (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))
54adantl 482 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))
62, 5jca 512 . 2 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽)))
7 simprl 767 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) → 𝐹:𝑋𝑌)
8 toponuni 21194 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
98ad3antrrr 726 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → 𝑋 = 𝐽)
10 simplrl 773 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → 𝐹:𝑋𝑌)
11 fimacnv 6695 . . . . . . . . . . 11 (𝐹:𝑋𝑌 → (𝐹𝑌) = 𝑋)
1211eqcomd 2799 . . . . . . . . . 10 (𝐹:𝑋𝑌𝑋 = (𝐹𝑌))
1310, 12syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → 𝑋 = (𝐹𝑌))
149, 13eqtr3d 2831 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → 𝐽 = (𝐹𝑌))
1514difeq1d 4014 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → ( 𝐽 ∖ (𝐹𝑥)) = ((𝐹𝑌) ∖ (𝐹𝑥)))
16 ffun 6377 . . . . . . . 8 (𝐹:𝑋𝑌 → Fun 𝐹)
17 funcnvcnv 6283 . . . . . . . 8 (Fun 𝐹 → Fun 𝐹)
18 imadif 6300 . . . . . . . 8 (Fun 𝐹 → (𝐹 “ (𝑌𝑥)) = ((𝐹𝑌) ∖ (𝐹𝑥)))
1910, 16, 17, 184syl 19 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → (𝐹 “ (𝑌𝑥)) = ((𝐹𝑌) ∖ (𝐹𝑥)))
2015, 19eqtr4d 2832 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → ( 𝐽 ∖ (𝐹𝑥)) = (𝐹 “ (𝑌𝑥)))
21 imaeq2 5794 . . . . . . . 8 (𝑦 = (𝑌𝑥) → (𝐹𝑦) = (𝐹 “ (𝑌𝑥)))
2221eleq1d 2865 . . . . . . 7 (𝑦 = (𝑌𝑥) → ((𝐹𝑦) ∈ (Clsd‘𝐽) ↔ (𝐹 “ (𝑌𝑥)) ∈ (Clsd‘𝐽)))
23 simplrr 774 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))
24 toponuni 21194 . . . . . . . . . 10 (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = 𝐾)
2524ad3antlr 727 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → 𝑌 = 𝐾)
2625difeq1d 4014 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → (𝑌𝑥) = ( 𝐾𝑥))
27 topontop 21193 . . . . . . . . . 10 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
2827ad3antlr 727 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → 𝐾 ∈ Top)
29 eqid 2793 . . . . . . . . . 10 𝐾 = 𝐾
3029opncld 21313 . . . . . . . . 9 ((𝐾 ∈ Top ∧ 𝑥𝐾) → ( 𝐾𝑥) ∈ (Clsd‘𝐾))
3128, 30sylancom 588 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → ( 𝐾𝑥) ∈ (Clsd‘𝐾))
3226, 31eqeltrd 2881 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → (𝑌𝑥) ∈ (Clsd‘𝐾))
3322, 23, 32rspcdva 3560 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → (𝐹 “ (𝑌𝑥)) ∈ (Clsd‘𝐽))
3420, 33eqeltrd 2881 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → ( 𝐽 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽))
35 topontop 21193 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
3635ad3antrrr 726 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → 𝐽 ∈ Top)
37 cnvimass 5817 . . . . . . . 8 (𝐹𝑥) ⊆ dom 𝐹
3837, 10fssdm 6390 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → (𝐹𝑥) ⊆ 𝑋)
3938, 9sseqtrd 3923 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → (𝐹𝑥) ⊆ 𝐽)
40 eqid 2793 . . . . . . 7 𝐽 = 𝐽
4140isopn2 21312 . . . . . 6 ((𝐽 ∈ Top ∧ (𝐹𝑥) ⊆ 𝐽) → ((𝐹𝑥) ∈ 𝐽 ↔ ( 𝐽 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽)))
4236, 39, 41syl2anc 584 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → ((𝐹𝑥) ∈ 𝐽 ↔ ( 𝐽 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽)))
4334, 42mpbird 258 . . . 4 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) ∧ 𝑥𝐾) → (𝐹𝑥) ∈ 𝐽)
4443ralrimiva 3147 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) → ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)
45 iscn 21515 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
4645adantr 481 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
477, 44, 46mpbir2and 709 . 2 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))) → 𝐹 ∈ (𝐽 Cn 𝐾))
486, 47impbida 797 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(𝐹𝑦) ∈ (Clsd‘𝐽))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1520  wcel 2079  wral 3103  cdif 3851  wss 3854   cuni 4739  ccnv 5434  cima 5438  Fun wfun 6211  wf 6213  cfv 6217  (class class class)co 7007  Topctop 21173  TopOnctopon 21190  Clsdccld 21296   Cn ccn 21504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-fv 6225  df-ov 7010  df-oprab 7011  df-mpo 7012  df-map 8249  df-top 21174  df-topon 21191  df-cld 21299  df-cn 21507
This theorem is referenced by:  cncls2  21553  paste  21574  cmphaushmeo  22080  ubthlem1  28326  ubthlem2  28327
  Copyright terms: Public domain W3C validator