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

Theorem indistopon 21297
Description: The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
indistopon (𝐴𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴))

Proof of Theorem indistopon
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sspr 4679 . . . . 5 (𝑥 ⊆ {∅, 𝐴} ↔ ((𝑥 = ∅ ∨ 𝑥 = {∅}) ∨ (𝑥 = {𝐴} ∨ 𝑥 = {∅, 𝐴})))
2 unieq 4759 . . . . . . . . 9 (𝑥 = ∅ → 𝑥 = ∅)
3 uni0 4778 . . . . . . . . . 10 ∅ = ∅
4 0ex 5109 . . . . . . . . . . 11 ∅ ∈ V
54prid1 4611 . . . . . . . . . 10 ∅ ∈ {∅, 𝐴}
63, 5eqeltri 2881 . . . . . . . . 9 ∅ ∈ {∅, 𝐴}
72, 6syl6eqel 2893 . . . . . . . 8 (𝑥 = ∅ → 𝑥 ∈ {∅, 𝐴})
87a1i 11 . . . . . . 7 (𝐴𝑉 → (𝑥 = ∅ → 𝑥 ∈ {∅, 𝐴}))
9 unieq 4759 . . . . . . . . 9 (𝑥 = {∅} → 𝑥 = {∅})
104unisn 4767 . . . . . . . . . 10 {∅} = ∅
1110, 5eqeltri 2881 . . . . . . . . 9 {∅} ∈ {∅, 𝐴}
129, 11syl6eqel 2893 . . . . . . . 8 (𝑥 = {∅} → 𝑥 ∈ {∅, 𝐴})
1312a1i 11 . . . . . . 7 (𝐴𝑉 → (𝑥 = {∅} → 𝑥 ∈ {∅, 𝐴}))
148, 13jaod 854 . . . . . 6 (𝐴𝑉 → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 ∈ {∅, 𝐴}))
15 unieq 4759 . . . . . . . . . 10 (𝑥 = {𝐴} → 𝑥 = {𝐴})
16 unisng 4766 . . . . . . . . . 10 (𝐴𝑉 {𝐴} = 𝐴)
1715, 16sylan9eqr 2855 . . . . . . . . 9 ((𝐴𝑉𝑥 = {𝐴}) → 𝑥 = 𝐴)
18 prid2g 4610 . . . . . . . . . 10 (𝐴𝑉𝐴 ∈ {∅, 𝐴})
1918adantr 481 . . . . . . . . 9 ((𝐴𝑉𝑥 = {𝐴}) → 𝐴 ∈ {∅, 𝐴})
2017, 19eqeltrd 2885 . . . . . . . 8 ((𝐴𝑉𝑥 = {𝐴}) → 𝑥 ∈ {∅, 𝐴})
2120ex 413 . . . . . . 7 (𝐴𝑉 → (𝑥 = {𝐴} → 𝑥 ∈ {∅, 𝐴}))
22 unieq 4759 . . . . . . . . . 10 (𝑥 = {∅, 𝐴} → 𝑥 = {∅, 𝐴})
23 uniprg 4765 . . . . . . . . . . . 12 ((∅ ∈ V ∧ 𝐴𝑉) → {∅, 𝐴} = (∅ ∪ 𝐴))
244, 23mpan 686 . . . . . . . . . . 11 (𝐴𝑉 {∅, 𝐴} = (∅ ∪ 𝐴))
25 uncom 4056 . . . . . . . . . . . 12 (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
26 un0 4270 . . . . . . . . . . . 12 (𝐴 ∪ ∅) = 𝐴
2725, 26eqtri 2821 . . . . . . . . . . 11 (∅ ∪ 𝐴) = 𝐴
2824, 27syl6eq 2849 . . . . . . . . . 10 (𝐴𝑉 {∅, 𝐴} = 𝐴)
2922, 28sylan9eqr 2855 . . . . . . . . 9 ((𝐴𝑉𝑥 = {∅, 𝐴}) → 𝑥 = 𝐴)
3018adantr 481 . . . . . . . . 9 ((𝐴𝑉𝑥 = {∅, 𝐴}) → 𝐴 ∈ {∅, 𝐴})
3129, 30eqeltrd 2885 . . . . . . . 8 ((𝐴𝑉𝑥 = {∅, 𝐴}) → 𝑥 ∈ {∅, 𝐴})
3231ex 413 . . . . . . 7 (𝐴𝑉 → (𝑥 = {∅, 𝐴} → 𝑥 ∈ {∅, 𝐴}))
3321, 32jaod 854 . . . . . 6 (𝐴𝑉 → ((𝑥 = {𝐴} ∨ 𝑥 = {∅, 𝐴}) → 𝑥 ∈ {∅, 𝐴}))
3414, 33jaod 854 . . . . 5 (𝐴𝑉 → (((𝑥 = ∅ ∨ 𝑥 = {∅}) ∨ (𝑥 = {𝐴} ∨ 𝑥 = {∅, 𝐴})) → 𝑥 ∈ {∅, 𝐴}))
351, 34syl5bi 243 . . . 4 (𝐴𝑉 → (𝑥 ⊆ {∅, 𝐴} → 𝑥 ∈ {∅, 𝐴}))
3635alrimiv 1909 . . 3 (𝐴𝑉 → ∀𝑥(𝑥 ⊆ {∅, 𝐴} → 𝑥 ∈ {∅, 𝐴}))
37 vex 3443 . . . . . 6 𝑥 ∈ V
3837elpr 4501 . . . . 5 (𝑥 ∈ {∅, 𝐴} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝐴))
39 vex 3443 . . . . . . . . 9 𝑦 ∈ V
4039elpr 4501 . . . . . . . 8 (𝑦 ∈ {∅, 𝐴} ↔ (𝑦 = ∅ ∨ 𝑦 = 𝐴))
41 simpr 485 . . . . . . . . . . . . . 14 ((𝑥 = ∅ ∧ 𝑦 = ∅) → 𝑦 = ∅)
4241ineq2d 4115 . . . . . . . . . . . . 13 ((𝑥 = ∅ ∧ 𝑦 = ∅) → (𝑥𝑦) = (𝑥 ∩ ∅))
43 in0 4271 . . . . . . . . . . . . 13 (𝑥 ∩ ∅) = ∅
4442, 43syl6eq 2849 . . . . . . . . . . . 12 ((𝑥 = ∅ ∧ 𝑦 = ∅) → (𝑥𝑦) = ∅)
4544, 5syl6eqel 2893 . . . . . . . . . . 11 ((𝑥 = ∅ ∧ 𝑦 = ∅) → (𝑥𝑦) ∈ {∅, 𝐴})
4645a1i 11 . . . . . . . . . 10 (𝐴𝑉 → ((𝑥 = ∅ ∧ 𝑦 = ∅) → (𝑥𝑦) ∈ {∅, 𝐴}))
47 simpr 485 . . . . . . . . . . . . . 14 ((𝑥 = 𝐴𝑦 = ∅) → 𝑦 = ∅)
4847ineq2d 4115 . . . . . . . . . . . . 13 ((𝑥 = 𝐴𝑦 = ∅) → (𝑥𝑦) = (𝑥 ∩ ∅))
4948, 43syl6eq 2849 . . . . . . . . . . . 12 ((𝑥 = 𝐴𝑦 = ∅) → (𝑥𝑦) = ∅)
5049, 5syl6eqel 2893 . . . . . . . . . . 11 ((𝑥 = 𝐴𝑦 = ∅) → (𝑥𝑦) ∈ {∅, 𝐴})
5150a1i 11 . . . . . . . . . 10 (𝐴𝑉 → ((𝑥 = 𝐴𝑦 = ∅) → (𝑥𝑦) ∈ {∅, 𝐴}))
52 simpl 483 . . . . . . . . . . . . . 14 ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → 𝑥 = ∅)
5352ineq1d 4114 . . . . . . . . . . . . 13 ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → (𝑥𝑦) = (∅ ∩ 𝑦))
54 0in 4273 . . . . . . . . . . . . 13 (∅ ∩ 𝑦) = ∅
5553, 54syl6eq 2849 . . . . . . . . . . . 12 ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → (𝑥𝑦) = ∅)
5655, 5syl6eqel 2893 . . . . . . . . . . 11 ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → (𝑥𝑦) ∈ {∅, 𝐴})
5756a1i 11 . . . . . . . . . 10 (𝐴𝑉 → ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → (𝑥𝑦) ∈ {∅, 𝐴}))
58 ineq12 4110 . . . . . . . . . . . . . 14 ((𝑥 = 𝐴𝑦 = 𝐴) → (𝑥𝑦) = (𝐴𝐴))
5958adantl 482 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑥 = 𝐴𝑦 = 𝐴)) → (𝑥𝑦) = (𝐴𝐴))
60 inidm 4121 . . . . . . . . . . . . 13 (𝐴𝐴) = 𝐴
6159, 60syl6eq 2849 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑥 = 𝐴𝑦 = 𝐴)) → (𝑥𝑦) = 𝐴)
6218adantr 481 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑥 = 𝐴𝑦 = 𝐴)) → 𝐴 ∈ {∅, 𝐴})
6361, 62eqeltrd 2885 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑥 = 𝐴𝑦 = 𝐴)) → (𝑥𝑦) ∈ {∅, 𝐴})
6463ex 413 . . . . . . . . . 10 (𝐴𝑉 → ((𝑥 = 𝐴𝑦 = 𝐴) → (𝑥𝑦) ∈ {∅, 𝐴}))
6546, 51, 57, 64ccased 1031 . . . . . . . . 9 (𝐴𝑉 → (((𝑥 = ∅ ∨ 𝑥 = 𝐴) ∧ (𝑦 = ∅ ∨ 𝑦 = 𝐴)) → (𝑥𝑦) ∈ {∅, 𝐴}))
6665expdimp 453 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) → ((𝑦 = ∅ ∨ 𝑦 = 𝐴) → (𝑥𝑦) ∈ {∅, 𝐴}))
6740, 66syl5bi 243 . . . . . . 7 ((𝐴𝑉 ∧ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) → (𝑦 ∈ {∅, 𝐴} → (𝑥𝑦) ∈ {∅, 𝐴}))
6867ralrimiv 3150 . . . . . 6 ((𝐴𝑉 ∧ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) → ∀𝑦 ∈ {∅, 𝐴} (𝑥𝑦) ∈ {∅, 𝐴})
6968ex 413 . . . . 5 (𝐴𝑉 → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) → ∀𝑦 ∈ {∅, 𝐴} (𝑥𝑦) ∈ {∅, 𝐴}))
7038, 69syl5bi 243 . . . 4 (𝐴𝑉 → (𝑥 ∈ {∅, 𝐴} → ∀𝑦 ∈ {∅, 𝐴} (𝑥𝑦) ∈ {∅, 𝐴}))
7170ralrimiv 3150 . . 3 (𝐴𝑉 → ∀𝑥 ∈ {∅, 𝐴}∀𝑦 ∈ {∅, 𝐴} (𝑥𝑦) ∈ {∅, 𝐴})
72 prex 5231 . . . 4 {∅, 𝐴} ∈ V
73 istopg 21191 . . . 4 ({∅, 𝐴} ∈ V → ({∅, 𝐴} ∈ Top ↔ (∀𝑥(𝑥 ⊆ {∅, 𝐴} → 𝑥 ∈ {∅, 𝐴}) ∧ ∀𝑥 ∈ {∅, 𝐴}∀𝑦 ∈ {∅, 𝐴} (𝑥𝑦) ∈ {∅, 𝐴})))
7472, 73mp1i 13 . . 3 (𝐴𝑉 → ({∅, 𝐴} ∈ Top ↔ (∀𝑥(𝑥 ⊆ {∅, 𝐴} → 𝑥 ∈ {∅, 𝐴}) ∧ ∀𝑥 ∈ {∅, 𝐴}∀𝑦 ∈ {∅, 𝐴} (𝑥𝑦) ∈ {∅, 𝐴})))
7536, 71, 74mpbir2and 709 . 2 (𝐴𝑉 → {∅, 𝐴} ∈ Top)
7628eqcomd 2803 . 2 (𝐴𝑉𝐴 = {∅, 𝐴})
77 istopon 21208 . 2 ({∅, 𝐴} ∈ (TopOn‘𝐴) ↔ ({∅, 𝐴} ∈ Top ∧ 𝐴 = {∅, 𝐴}))
7875, 76, 77sylanbrc 583 1 (𝐴𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 842  wal 1523   = wceq 1525  wcel 2083  wral 3107  Vcvv 3440  cun 3863  cin 3864  wss 3865  c0 4217  {csn 4478  {cpr 4480   cuni 4751  cfv 6232  Topctop 21189  TopOnctopon 21206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-iota 6196  df-fun 6234  df-fv 6240  df-top 21190  df-topon 21207
This theorem is referenced by:  indistop  21298  indisuni  21299  indistpsx  21306  indistpsALT  21309  indistps2ALT  21310  cnindis  21588  indishmph  22094  indistgp  22396  topdifinf  34182
  Copyright terms: Public domain W3C validator