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

Theorem tgcn 23247
Description: The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
tgcn.1 (𝜑𝐽 ∈ (TopOn‘𝑋))
tgcn.3 (𝜑𝐾 = (topGen‘𝐵))
tgcn.4 (𝜑𝐾 ∈ (TopOn‘𝑌))
Assertion
Ref Expression
tgcn (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽)))
Distinct variable groups:   𝑦,𝐵   𝑦,𝐹   𝑦,𝐽   𝑦,𝐾   𝑦,𝑋   𝑦,𝑌
Allowed substitution hint:   𝜑(𝑦)

Proof of Theorem tgcn
Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tgcn.1 . . 3 (𝜑𝐽 ∈ (TopOn‘𝑋))
2 tgcn.4 . . 3 (𝜑𝐾 ∈ (TopOn‘𝑌))
3 iscn 23230 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽)))
41, 2, 3syl2anc 582 . 2 (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽)))
5 tgcn.3 . . . . . . . . 9 (𝜑𝐾 = (topGen‘𝐵))
6 topontop 22906 . . . . . . . . . 10 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
72, 6syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Top)
85, 7eqeltrrd 2827 . . . . . . . 8 (𝜑 → (topGen‘𝐵) ∈ Top)
9 tgclb 22964 . . . . . . . 8 (𝐵 ∈ TopBases ↔ (topGen‘𝐵) ∈ Top)
108, 9sylibr 233 . . . . . . 7 (𝜑𝐵 ∈ TopBases)
11 bastg 22960 . . . . . . 7 (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
1210, 11syl 17 . . . . . 6 (𝜑𝐵 ⊆ (topGen‘𝐵))
1312, 5sseqtrrd 4021 . . . . 5 (𝜑𝐵𝐾)
14 ssralv 4048 . . . . 5 (𝐵𝐾 → (∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽 → ∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽))
1513, 14syl 17 . . . 4 (𝜑 → (∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽 → ∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽))
165eleq2d 2812 . . . . . . . . 9 (𝜑 → (𝑥𝐾𝑥 ∈ (topGen‘𝐵)))
17 eltg3 22956 . . . . . . . . . 10 (𝐵 ∈ TopBases → (𝑥 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧𝐵𝑥 = 𝑧)))
1810, 17syl 17 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧𝐵𝑥 = 𝑧)))
1916, 18bitrd 278 . . . . . . . 8 (𝜑 → (𝑥𝐾 ↔ ∃𝑧(𝑧𝐵𝑥 = 𝑧)))
20 ssralv 4048 . . . . . . . . . . . 12 (𝑧𝐵 → (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 → ∀𝑦𝑧 (𝐹𝑦) ∈ 𝐽))
21 topontop 22906 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
221, 21syl 17 . . . . . . . . . . . . 13 (𝜑𝐽 ∈ Top)
23 iunopn 22891 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ ∀𝑦𝑧 (𝐹𝑦) ∈ 𝐽) → 𝑦𝑧 (𝐹𝑦) ∈ 𝐽)
2423ex 411 . . . . . . . . . . . . 13 (𝐽 ∈ Top → (∀𝑦𝑧 (𝐹𝑦) ∈ 𝐽 𝑦𝑧 (𝐹𝑦) ∈ 𝐽))
2522, 24syl 17 . . . . . . . . . . . 12 (𝜑 → (∀𝑦𝑧 (𝐹𝑦) ∈ 𝐽 𝑦𝑧 (𝐹𝑦) ∈ 𝐽))
2620, 25sylan9r 507 . . . . . . . . . . 11 ((𝜑𝑧𝐵) → (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 𝑦𝑧 (𝐹𝑦) ∈ 𝐽))
27 imaeq2 6065 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹 𝑧))
28 imauni 7261 . . . . . . . . . . . . . 14 (𝐹 𝑧) = 𝑦𝑧 (𝐹𝑦)
2927, 28eqtrdi 2782 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹𝑥) = 𝑦𝑧 (𝐹𝑦))
3029eleq1d 2811 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝐹𝑥) ∈ 𝐽 𝑦𝑧 (𝐹𝑦) ∈ 𝐽))
3130imbi2d 339 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 → (𝐹𝑥) ∈ 𝐽) ↔ (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 𝑦𝑧 (𝐹𝑦) ∈ 𝐽)))
3226, 31syl5ibrcom 246 . . . . . . . . . 10 ((𝜑𝑧𝐵) → (𝑥 = 𝑧 → (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 → (𝐹𝑥) ∈ 𝐽)))
3332expimpd 452 . . . . . . . . 9 (𝜑 → ((𝑧𝐵𝑥 = 𝑧) → (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 → (𝐹𝑥) ∈ 𝐽)))
3433exlimdv 1929 . . . . . . . 8 (𝜑 → (∃𝑧(𝑧𝐵𝑥 = 𝑧) → (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 → (𝐹𝑥) ∈ 𝐽)))
3519, 34sylbid 239 . . . . . . 7 (𝜑 → (𝑥𝐾 → (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 → (𝐹𝑥) ∈ 𝐽)))
3635imp 405 . . . . . 6 ((𝜑𝑥𝐾) → (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 → (𝐹𝑥) ∈ 𝐽))
3736ralrimdva 3144 . . . . 5 (𝜑 → (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 → ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽))
38 imaeq2 6065 . . . . . . 7 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
3938eleq1d 2811 . . . . . 6 (𝑥 = 𝑦 → ((𝐹𝑥) ∈ 𝐽 ↔ (𝐹𝑦) ∈ 𝐽))
4039cbvralvw 3225 . . . . 5 (∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽 ↔ ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽)
4137, 40imbitrdi 250 . . . 4 (𝜑 → (∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽 → ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽))
4215, 41impbid 211 . . 3 (𝜑 → (∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽 ↔ ∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽))
4342anbi2d 628 . 2 (𝜑 → ((𝐹:𝑋𝑌 ∧ ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽)))
444, 43bitrd 278 1 (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝐵 (𝐹𝑦) ∈ 𝐽)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1534  wex 1774  wcel 2099  wral 3051  wss 3947   cuni 4913   ciun 5001  ccnv 5681  cima 5685  wf 6550  cfv 6554  (class class class)co 7424  topGenctg 17452  Topctop 22886  TopOnctopon 22903  TopBasesctb 22939   Cn ccn 23219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-fv 6562  df-ov 7427  df-oprab 7428  df-mpo 7429  df-map 8857  df-topgen 17458  df-top 22887  df-topon 22904  df-bases 22940  df-cn 23222
This theorem is referenced by:  subbascn  23249  txcnmpt  23619  ismtyhmeolem  37505
  Copyright terms: Public domain W3C validator