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

Theorem toprntopon 22820
Description: A topology is the same thing as a topology on a set (variable-free version). (Contributed by BJ, 27-Apr-2021.)
Assertion
Ref Expression
toprntopon Top = ran TopOn

Proof of Theorem toprntopon
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 toptopon2 22813 . . . . 5 (𝑥 ∈ Top ↔ 𝑥 ∈ (TopOn‘ 𝑥))
2 fvex 6904 . . . . . 6 (TopOn‘ 𝑥) ∈ V
3 eleq2 2818 . . . . . . . 8 (𝑦 = (TopOn‘ 𝑥) → (𝑥𝑦𝑥 ∈ (TopOn‘ 𝑥)))
4 eleq1 2817 . . . . . . . 8 (𝑦 = (TopOn‘ 𝑥) → (𝑦 ∈ ran TopOn ↔ (TopOn‘ 𝑥) ∈ ran TopOn))
53, 4anbi12d 631 . . . . . . 7 (𝑦 = (TopOn‘ 𝑥) → ((𝑥𝑦𝑦 ∈ ran TopOn) ↔ (𝑥 ∈ (TopOn‘ 𝑥) ∧ (TopOn‘ 𝑥) ∈ ran TopOn)))
6 simpl 482 . . . . . . . 8 ((𝑥 ∈ (TopOn‘ 𝑥) ∧ (TopOn‘ 𝑥) ∈ ran TopOn) → 𝑥 ∈ (TopOn‘ 𝑥))
7 fntopon 22819 . . . . . . . . . 10 TopOn Fn V
8 vuniex 7738 . . . . . . . . . 10 𝑥 ∈ V
9 fnfvelrn 7084 . . . . . . . . . 10 ((TopOn Fn V ∧ 𝑥 ∈ V) → (TopOn‘ 𝑥) ∈ ran TopOn)
107, 8, 9mp2an 691 . . . . . . . . 9 (TopOn‘ 𝑥) ∈ ran TopOn
1110jctr 524 . . . . . . . 8 (𝑥 ∈ (TopOn‘ 𝑥) → (𝑥 ∈ (TopOn‘ 𝑥) ∧ (TopOn‘ 𝑥) ∈ ran TopOn))
126, 11impbii 208 . . . . . . 7 ((𝑥 ∈ (TopOn‘ 𝑥) ∧ (TopOn‘ 𝑥) ∈ ran TopOn) ↔ 𝑥 ∈ (TopOn‘ 𝑥))
135, 12bitrdi 287 . . . . . 6 (𝑦 = (TopOn‘ 𝑥) → ((𝑥𝑦𝑦 ∈ ran TopOn) ↔ 𝑥 ∈ (TopOn‘ 𝑥)))
142, 13spcev 3592 . . . . 5 (𝑥 ∈ (TopOn‘ 𝑥) → ∃𝑦(𝑥𝑦𝑦 ∈ ran TopOn))
151, 14sylbi 216 . . . 4 (𝑥 ∈ Top → ∃𝑦(𝑥𝑦𝑦 ∈ ran TopOn))
16 funtopon 22815 . . . . . . . . 9 Fun TopOn
17 elrnrexdm 7093 . . . . . . . . 9 (Fun TopOn → (𝑦 ∈ ran TopOn → ∃𝑧 ∈ dom TopOn𝑦 = (TopOn‘𝑧)))
1816, 17ax-mp 5 . . . . . . . 8 (𝑦 ∈ ran TopOn → ∃𝑧 ∈ dom TopOn𝑦 = (TopOn‘𝑧))
19 rexex 3072 . . . . . . . 8 (∃𝑧 ∈ dom TopOn𝑦 = (TopOn‘𝑧) → ∃𝑧 𝑦 = (TopOn‘𝑧))
2018, 19syl 17 . . . . . . 7 (𝑦 ∈ ran TopOn → ∃𝑧 𝑦 = (TopOn‘𝑧))
21 19.42v 1950 . . . . . . . 8 (∃𝑧(𝑥𝑦𝑦 = (TopOn‘𝑧)) ↔ (𝑥𝑦 ∧ ∃𝑧 𝑦 = (TopOn‘𝑧)))
22 eqimss 4036 . . . . . . . . . . 11 (𝑦 = (TopOn‘𝑧) → 𝑦 ⊆ (TopOn‘𝑧))
2322sseld 3977 . . . . . . . . . 10 (𝑦 = (TopOn‘𝑧) → (𝑥𝑦𝑥 ∈ (TopOn‘𝑧)))
2423impcom 407 . . . . . . . . 9 ((𝑥𝑦𝑦 = (TopOn‘𝑧)) → 𝑥 ∈ (TopOn‘𝑧))
2524eximi 1830 . . . . . . . 8 (∃𝑧(𝑥𝑦𝑦 = (TopOn‘𝑧)) → ∃𝑧 𝑥 ∈ (TopOn‘𝑧))
2621, 25sylbir 234 . . . . . . 7 ((𝑥𝑦 ∧ ∃𝑧 𝑦 = (TopOn‘𝑧)) → ∃𝑧 𝑥 ∈ (TopOn‘𝑧))
2720, 26sylan2 592 . . . . . 6 ((𝑥𝑦𝑦 ∈ ran TopOn) → ∃𝑧 𝑥 ∈ (TopOn‘𝑧))
28 topontop 22808 . . . . . . 7 (𝑥 ∈ (TopOn‘𝑧) → 𝑥 ∈ Top)
2928exlimiv 1926 . . . . . 6 (∃𝑧 𝑥 ∈ (TopOn‘𝑧) → 𝑥 ∈ Top)
3027, 29syl 17 . . . . 5 ((𝑥𝑦𝑦 ∈ ran TopOn) → 𝑥 ∈ Top)
3130exlimiv 1926 . . . 4 (∃𝑦(𝑥𝑦𝑦 ∈ ran TopOn) → 𝑥 ∈ Top)
3215, 31impbii 208 . . 3 (𝑥 ∈ Top ↔ ∃𝑦(𝑥𝑦𝑦 ∈ ran TopOn))
33 eluni 4906 . . 3 (𝑥 ran TopOn ↔ ∃𝑦(𝑥𝑦𝑦 ∈ ran TopOn))
3432, 33bitr4i 278 . 2 (𝑥 ∈ Top ↔ 𝑥 ran TopOn)
3534eqriv 2725 1 Top = ran TopOn
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1534  wex 1774  wcel 2099  wrex 3066  Vcvv 3470   cuni 4903  dom cdm 5672  ran crn 5673  Fun wfun 6536   Fn wfn 6537  cfv 6542  Topctop 22788  TopOnctopon 22805
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 2699  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-iota 6494  df-fun 6544  df-fn 6545  df-fv 6550  df-topon 22806
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator