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

Theorem toponmre 21701
Description: The topologies over a given base set form a Moore collection: the intersection of any family of them is a topology, including the empty (relative) intersection which gives the discrete topology distop 21603. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 5-May-2015.)
Assertion
Ref Expression
toponmre (𝐵𝑉 → (TopOn‘𝐵) ∈ (Moore‘𝒫 𝐵))

Proof of Theorem toponmre
Dummy variables 𝑏 𝑐 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 toponsspwpw 21530 . . 3 (TopOn‘𝐵) ⊆ 𝒫 𝒫 𝐵
21a1i 11 . 2 (𝐵𝑉 → (TopOn‘𝐵) ⊆ 𝒫 𝒫 𝐵)
3 distopon 21605 . 2 (𝐵𝑉 → 𝒫 𝐵 ∈ (TopOn‘𝐵))
4 simpl 486 . . . . . . . . . . . . . 14 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝑏 ⊆ (TopOn‘𝐵))
54sselda 3918 . . . . . . . . . . . . 13 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑥𝑏) → 𝑥 ∈ (TopOn‘𝐵))
65adantrl 715 . . . . . . . . . . . 12 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥𝑏)) → 𝑥 ∈ (TopOn‘𝐵))
7 topontop 21521 . . . . . . . . . . . 12 (𝑥 ∈ (TopOn‘𝐵) → 𝑥 ∈ Top)
86, 7syl 17 . . . . . . . . . . 11 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥𝑏)) → 𝑥 ∈ Top)
9 simpl 486 . . . . . . . . . . . . 13 ((𝑐 𝑏𝑥𝑏) → 𝑐 𝑏)
10 intss1 4856 . . . . . . . . . . . . . 14 (𝑥𝑏 𝑏𝑥)
1110adantl 485 . . . . . . . . . . . . 13 ((𝑐 𝑏𝑥𝑏) → 𝑏𝑥)
129, 11sstrd 3928 . . . . . . . . . . . 12 ((𝑐 𝑏𝑥𝑏) → 𝑐𝑥)
1312adantl 485 . . . . . . . . . . 11 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥𝑏)) → 𝑐𝑥)
14 uniopn 21505 . . . . . . . . . . 11 ((𝑥 ∈ Top ∧ 𝑐𝑥) → 𝑐𝑥)
158, 13, 14syl2anc 587 . . . . . . . . . 10 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥𝑏)) → 𝑐𝑥)
1615expr 460 . . . . . . . . 9 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 𝑏) → (𝑥𝑏 𝑐𝑥))
1716ralrimiv 3151 . . . . . . . 8 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 𝑏) → ∀𝑥𝑏 𝑐𝑥)
18 vuniex 7449 . . . . . . . . 9 𝑐 ∈ V
1918elint2 4848 . . . . . . . 8 ( 𝑐 𝑏 ↔ ∀𝑥𝑏 𝑐𝑥)
2017, 19sylibr 237 . . . . . . 7 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 𝑏) → 𝑐 𝑏)
2120ex 416 . . . . . 6 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → (𝑐 𝑏 𝑐 𝑏))
2221alrimiv 1928 . . . . 5 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐(𝑐 𝑏 𝑐 𝑏))
23 simpll 766 . . . . . . . . . . 11 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) → 𝑏 ⊆ (TopOn‘𝐵))
2423sselda 3918 . . . . . . . . . 10 ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) ∧ 𝑦𝑏) → 𝑦 ∈ (TopOn‘𝐵))
25 topontop 21521 . . . . . . . . . 10 (𝑦 ∈ (TopOn‘𝐵) → 𝑦 ∈ Top)
2624, 25syl 17 . . . . . . . . 9 ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) ∧ 𝑦𝑏) → 𝑦 ∈ Top)
27 intss1 4856 . . . . . . . . . . 11 (𝑦𝑏 𝑏𝑦)
2827adantl 485 . . . . . . . . . 10 ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) ∧ 𝑦𝑏) → 𝑏𝑦)
29 simplrl 776 . . . . . . . . . 10 ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) ∧ 𝑦𝑏) → 𝑐 𝑏)
3028, 29sseldd 3919 . . . . . . . . 9 ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) ∧ 𝑦𝑏) → 𝑐𝑦)
31 simplrr 777 . . . . . . . . . 10 ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) ∧ 𝑦𝑏) → 𝑥 𝑏)
3228, 31sseldd 3919 . . . . . . . . 9 ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) ∧ 𝑦𝑏) → 𝑥𝑦)
33 inopn 21507 . . . . . . . . 9 ((𝑦 ∈ Top ∧ 𝑐𝑦𝑥𝑦) → (𝑐𝑥) ∈ 𝑦)
3426, 30, 32, 33syl3anc 1368 . . . . . . . 8 ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) ∧ 𝑦𝑏) → (𝑐𝑥) ∈ 𝑦)
3534ralrimiva 3152 . . . . . . 7 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) → ∀𝑦𝑏 (𝑐𝑥) ∈ 𝑦)
36 vex 3447 . . . . . . . . 9 𝑐 ∈ V
3736inex1 5188 . . . . . . . 8 (𝑐𝑥) ∈ V
3837elint2 4848 . . . . . . 7 ((𝑐𝑥) ∈ 𝑏 ↔ ∀𝑦𝑏 (𝑐𝑥) ∈ 𝑦)
3935, 38sylibr 237 . . . . . 6 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥 𝑏)) → (𝑐𝑥) ∈ 𝑏)
4039ralrimivva 3159 . . . . 5 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐 𝑏𝑥 𝑏(𝑐𝑥) ∈ 𝑏)
41 intex 5207 . . . . . . . 8 (𝑏 ≠ ∅ ↔ 𝑏 ∈ V)
4241biimpi 219 . . . . . . 7 (𝑏 ≠ ∅ → 𝑏 ∈ V)
4342adantl 485 . . . . . 6 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝑏 ∈ V)
44 istopg 21503 . . . . . 6 ( 𝑏 ∈ V → ( 𝑏 ∈ Top ↔ (∀𝑐(𝑐 𝑏 𝑐 𝑏) ∧ ∀𝑐 𝑏𝑥 𝑏(𝑐𝑥) ∈ 𝑏)))
4543, 44syl 17 . . . . 5 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ( 𝑏 ∈ Top ↔ (∀𝑐(𝑐 𝑏 𝑐 𝑏) ∧ ∀𝑐 𝑏𝑥 𝑏(𝑐𝑥) ∈ 𝑏)))
4622, 40, 45mpbir2and 712 . . . 4 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝑏 ∈ Top)
47463adant1 1127 . . 3 ((𝐵𝑉𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝑏 ∈ Top)
48 n0 4263 . . . . . . . . . . 11 (𝑏 ≠ ∅ ↔ ∃𝑥 𝑥𝑏)
4948biimpi 219 . . . . . . . . . 10 (𝑏 ≠ ∅ → ∃𝑥 𝑥𝑏)
5049ad2antlr 726 . . . . . . . . 9 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 𝑏) → ∃𝑥 𝑥𝑏)
5110sselda 3918 . . . . . . . . . . . . . . 15 ((𝑥𝑏𝑐 𝑏) → 𝑐𝑥)
5251ancoms 462 . . . . . . . . . . . . . 14 ((𝑐 𝑏𝑥𝑏) → 𝑐𝑥)
53 elssuni 4833 . . . . . . . . . . . . . 14 (𝑐𝑥𝑐 𝑥)
5452, 53syl 17 . . . . . . . . . . . . 13 ((𝑐 𝑏𝑥𝑏) → 𝑐 𝑥)
5554adantl 485 . . . . . . . . . . . 12 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥𝑏)) → 𝑐 𝑥)
565adantrl 715 . . . . . . . . . . . . 13 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥𝑏)) → 𝑥 ∈ (TopOn‘𝐵))
57 toponuni 21522 . . . . . . . . . . . . 13 (𝑥 ∈ (TopOn‘𝐵) → 𝐵 = 𝑥)
5856, 57syl 17 . . . . . . . . . . . 12 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥𝑏)) → 𝐵 = 𝑥)
5955, 58sseqtrrd 3959 . . . . . . . . . . 11 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 𝑏𝑥𝑏)) → 𝑐𝐵)
6059expr 460 . . . . . . . . . 10 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 𝑏) → (𝑥𝑏𝑐𝐵))
6160exlimdv 1934 . . . . . . . . 9 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 𝑏) → (∃𝑥 𝑥𝑏𝑐𝐵))
6250, 61mpd 15 . . . . . . . 8 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 𝑏) → 𝑐𝐵)
6362ralrimiva 3152 . . . . . . 7 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐 𝑏𝑐𝐵)
64 unissb 4835 . . . . . . 7 ( 𝑏𝐵 ↔ ∀𝑐 𝑏𝑐𝐵)
6563, 64sylibr 237 . . . . . 6 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝑏𝐵)
66653adant1 1127 . . . . 5 ((𝐵𝑉𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝑏𝐵)
674sselda 3918 . . . . . . . . . 10 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐𝑏) → 𝑐 ∈ (TopOn‘𝐵))
68 toponuni 21522 . . . . . . . . . 10 (𝑐 ∈ (TopOn‘𝐵) → 𝐵 = 𝑐)
6967, 68syl 17 . . . . . . . . 9 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐𝑏) → 𝐵 = 𝑐)
70 topontop 21521 . . . . . . . . . 10 (𝑐 ∈ (TopOn‘𝐵) → 𝑐 ∈ Top)
71 eqid 2801 . . . . . . . . . . 11 𝑐 = 𝑐
7271topopn 21514 . . . . . . . . . 10 (𝑐 ∈ Top → 𝑐𝑐)
7367, 70, 723syl 18 . . . . . . . . 9 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐𝑏) → 𝑐𝑐)
7469, 73eqeltrd 2893 . . . . . . . 8 (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐𝑏) → 𝐵𝑐)
7574ralrimiva 3152 . . . . . . 7 ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐𝑏 𝐵𝑐)
76753adant1 1127 . . . . . 6 ((𝐵𝑉𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐𝑏 𝐵𝑐)
77 elintg 4849 . . . . . . 7 (𝐵𝑉 → (𝐵 𝑏 ↔ ∀𝑐𝑏 𝐵𝑐))
78773ad2ant1 1130 . . . . . 6 ((𝐵𝑉𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → (𝐵 𝑏 ↔ ∀𝑐𝑏 𝐵𝑐))
7976, 78mpbird 260 . . . . 5 ((𝐵𝑉𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝐵 𝑏)
80 unissel 4834 . . . . 5 (( 𝑏𝐵𝐵 𝑏) → 𝑏 = 𝐵)
8166, 79, 80syl2anc 587 . . . 4 ((𝐵𝑉𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝑏 = 𝐵)
8281eqcomd 2807 . . 3 ((𝐵𝑉𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝐵 = 𝑏)
83 istopon 21520 . . 3 ( 𝑏 ∈ (TopOn‘𝐵) ↔ ( 𝑏 ∈ Top ∧ 𝐵 = 𝑏))
8447, 82, 83sylanbrc 586 . 2 ((𝐵𝑉𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝑏 ∈ (TopOn‘𝐵))
852, 3, 84ismred 16868 1 (𝐵𝑉 → (TopOn‘𝐵) ∈ (Moore‘𝒫 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084  wal 1536   = wceq 1538  wex 1781  wcel 2112  wne 2990  wral 3109  Vcvv 3444  cin 3883  wss 3884  c0 4246  𝒫 cpw 4500   cuni 4803   cint 4841  cfv 6328  Moorecmre 16848  Topctop 21501  TopOnctopon 21518
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-int 4842  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-iota 6287  df-fun 6330  df-fv 6336  df-mre 16852  df-top 21502  df-topon 21519
This theorem is referenced by:  topmtcl  33819
  Copyright terms: Public domain W3C validator