Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prsal Structured version   Visualization version   GIF version

Theorem prsal 42753
 Description: The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Assertion
Ref Expression
prsal (𝑋𝑉 → {∅, 𝑋} ∈ SAlg)

Proof of Theorem prsal
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 0ex 5184 . . . 4 ∅ ∈ V
21prid1 4671 . . 3 ∅ ∈ {∅, 𝑋}
32a1i 11 . 2 (𝑋𝑉 → ∅ ∈ {∅, 𝑋})
4 uniprg 4829 . . . . . . . 8 ((∅ ∈ V ∧ 𝑋𝑉) → {∅, 𝑋} = (∅ ∪ 𝑋))
51, 4mpan 689 . . . . . . 7 (𝑋𝑉 {∅, 𝑋} = (∅ ∪ 𝑋))
6 0un 4319 . . . . . . 7 (∅ ∪ 𝑋) = 𝑋
75, 6syl6eq 2872 . . . . . 6 (𝑋𝑉 {∅, 𝑋} = 𝑋)
87difeq1d 4074 . . . . 5 (𝑋𝑉 → ( {∅, 𝑋} ∖ 𝑦) = (𝑋𝑦))
98adantr 484 . . . 4 ((𝑋𝑉𝑦 ∈ {∅, 𝑋}) → ( {∅, 𝑋} ∖ 𝑦) = (𝑋𝑦))
10 difeq2 4069 . . . . . . . . 9 (𝑦 = ∅ → (𝑋𝑦) = (𝑋 ∖ ∅))
1110adantl 485 . . . . . . . 8 ((𝑋𝑉𝑦 = ∅) → (𝑋𝑦) = (𝑋 ∖ ∅))
12 dif0 4305 . . . . . . . 8 (𝑋 ∖ ∅) = 𝑋
1311, 12syl6eq 2872 . . . . . . 7 ((𝑋𝑉𝑦 = ∅) → (𝑋𝑦) = 𝑋)
14 prid2g 4670 . . . . . . . 8 (𝑋𝑉𝑋 ∈ {∅, 𝑋})
1514adantr 484 . . . . . . 7 ((𝑋𝑉𝑦 = ∅) → 𝑋 ∈ {∅, 𝑋})
1613, 15eqeltrd 2912 . . . . . 6 ((𝑋𝑉𝑦 = ∅) → (𝑋𝑦) ∈ {∅, 𝑋})
1716adantlr 714 . . . . 5 (((𝑋𝑉𝑦 ∈ {∅, 𝑋}) ∧ 𝑦 = ∅) → (𝑋𝑦) ∈ {∅, 𝑋})
18 neqne 3015 . . . . . . . 8 𝑦 = ∅ → 𝑦 ≠ ∅)
19 elprn1 42068 . . . . . . . 8 ((𝑦 ∈ {∅, 𝑋} ∧ 𝑦 ≠ ∅) → 𝑦 = 𝑋)
2018, 19sylan2 595 . . . . . . 7 ((𝑦 ∈ {∅, 𝑋} ∧ ¬ 𝑦 = ∅) → 𝑦 = 𝑋)
2120adantll 713 . . . . . 6 (((𝑋𝑉𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → 𝑦 = 𝑋)
22 difeq2 4069 . . . . . . . 8 (𝑦 = 𝑋 → (𝑋𝑦) = (𝑋𝑋))
23 difid 4303 . . . . . . . 8 (𝑋𝑋) = ∅
2422, 23syl6eq 2872 . . . . . . 7 (𝑦 = 𝑋 → (𝑋𝑦) = ∅)
252a1i 11 . . . . . . 7 (𝑦 = 𝑋 → ∅ ∈ {∅, 𝑋})
2624, 25eqeltrd 2912 . . . . . 6 (𝑦 = 𝑋 → (𝑋𝑦) ∈ {∅, 𝑋})
2721, 26syl 17 . . . . 5 (((𝑋𝑉𝑦 ∈ {∅, 𝑋}) ∧ ¬ 𝑦 = ∅) → (𝑋𝑦) ∈ {∅, 𝑋})
2817, 27pm2.61dan 812 . . . 4 ((𝑋𝑉𝑦 ∈ {∅, 𝑋}) → (𝑋𝑦) ∈ {∅, 𝑋})
299, 28eqeltrd 2912 . . 3 ((𝑋𝑉𝑦 ∈ {∅, 𝑋}) → ( {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋})
3029ralrimiva 3170 . 2 (𝑋𝑉 → ∀𝑦 ∈ {∅, 𝑋} ( {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋})
31 elpwi 4521 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ⊆ {∅, 𝑋})
3231unissd 4821 . . . . . . . . . 10 (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 {∅, 𝑋})
3332adantl 485 . . . . . . . . 9 ((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) → 𝑦 {∅, 𝑋})
347adantr 484 . . . . . . . . 9 ((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) → {∅, 𝑋} = 𝑋)
3533, 34sseqtrd 3983 . . . . . . . 8 ((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) → 𝑦𝑋)
3635adantr 484 . . . . . . 7 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋𝑦) → 𝑦𝑋)
37 elssuni 4841 . . . . . . . 8 (𝑋𝑦𝑋 𝑦)
3837adantl 485 . . . . . . 7 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋𝑦) → 𝑋 𝑦)
3936, 38eqssd 3960 . . . . . 6 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋𝑦) → 𝑦 = 𝑋)
4014ad2antrr 725 . . . . . 6 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋𝑦) → 𝑋 ∈ {∅, 𝑋})
4139, 40eqeltrd 2912 . . . . 5 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ 𝑋𝑦) → 𝑦 ∈ {∅, 𝑋})
42 id 22 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ∈ 𝒫 {∅, 𝑋})
43 pwpr 4805 . . . . . . . . . . 11 𝒫 {∅, 𝑋} = ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}})
4442, 43eleqtrdi 2922 . . . . . . . . . 10 (𝑦 ∈ 𝒫 {∅, 𝑋} → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
4544adantr 484 . . . . . . . . 9 ((𝑦 ∈ 𝒫 {∅, 𝑋} ∧ ¬ 𝑋𝑦) → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
4645adantll 713 . . . . . . . 8 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋𝑦) → 𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}))
47 snidg 4572 . . . . . . . . . . . . . 14 (𝑋𝑉𝑋 ∈ {𝑋})
4847adantr 484 . . . . . . . . . . . . 13 ((𝑋𝑉𝑦 = {𝑋}) → 𝑋 ∈ {𝑋})
49 id 22 . . . . . . . . . . . . . . 15 (𝑦 = {𝑋} → 𝑦 = {𝑋})
5049eqcomd 2827 . . . . . . . . . . . . . 14 (𝑦 = {𝑋} → {𝑋} = 𝑦)
5150adantl 485 . . . . . . . . . . . . 13 ((𝑋𝑉𝑦 = {𝑋}) → {𝑋} = 𝑦)
5248, 51eleqtrd 2914 . . . . . . . . . . . 12 ((𝑋𝑉𝑦 = {𝑋}) → 𝑋𝑦)
5352adantlr 714 . . . . . . . . . . 11 (((𝑋𝑉𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ 𝑦 = {𝑋}) → 𝑋𝑦)
54 id 22 . . . . . . . . . . . . 13 (𝑋𝑉𝑋𝑉)
5554ad2antrr 725 . . . . . . . . . . . 12 (((𝑋𝑉𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑋𝑉)
56 neqne 3015 . . . . . . . . . . . . . 14 𝑦 = {𝑋} → 𝑦 ≠ {𝑋})
57 elprn1 42068 . . . . . . . . . . . . . 14 ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ 𝑦 ≠ {𝑋}) → 𝑦 = {∅, 𝑋})
5856, 57sylan2 595 . . . . . . . . . . . . 13 ((𝑦 ∈ {{𝑋}, {∅, 𝑋}} ∧ ¬ 𝑦 = {𝑋}) → 𝑦 = {∅, 𝑋})
5958adantll 713 . . . . . . . . . . . 12 (((𝑋𝑉𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑦 = {∅, 𝑋})
6014adantr 484 . . . . . . . . . . . . 13 ((𝑋𝑉𝑦 = {∅, 𝑋}) → 𝑋 ∈ {∅, 𝑋})
61 id 22 . . . . . . . . . . . . . . 15 (𝑦 = {∅, 𝑋} → 𝑦 = {∅, 𝑋})
6261eqcomd 2827 . . . . . . . . . . . . . 14 (𝑦 = {∅, 𝑋} → {∅, 𝑋} = 𝑦)
6362adantl 485 . . . . . . . . . . . . 13 ((𝑋𝑉𝑦 = {∅, 𝑋}) → {∅, 𝑋} = 𝑦)
6460, 63eleqtrd 2914 . . . . . . . . . . . 12 ((𝑋𝑉𝑦 = {∅, 𝑋}) → 𝑋𝑦)
6555, 59, 64syl2anc 587 . . . . . . . . . . 11 (((𝑋𝑉𝑦 ∈ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 = {𝑋}) → 𝑋𝑦)
6653, 65pm2.61dan 812 . . . . . . . . . 10 ((𝑋𝑉𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑋𝑦)
6766stoic1a 1774 . . . . . . . . 9 ((𝑋𝑉 ∧ ¬ 𝑋𝑦) → ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
6867adantlr 714 . . . . . . . 8 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋𝑦) → ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}})
69 elunnel2 41453 . . . . . . . 8 ((𝑦 ∈ ({∅, {∅}} ∪ {{𝑋}, {∅, 𝑋}}) ∧ ¬ 𝑦 ∈ {{𝑋}, {∅, 𝑋}}) → 𝑦 ∈ {∅, {∅}})
7046, 68, 69syl2anc 587 . . . . . . 7 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋𝑦) → 𝑦 ∈ {∅, {∅}})
71 unieq 4822 . . . . . . . . . 10 (𝑦 = ∅ → 𝑦 = ∅)
72 uni0 4839 . . . . . . . . . 10 ∅ = ∅
7371, 72syl6eq 2872 . . . . . . . . 9 (𝑦 = ∅ → 𝑦 = ∅)
7473adantl 485 . . . . . . . 8 ((𝑦 ∈ {∅, {∅}} ∧ 𝑦 = ∅) → 𝑦 = ∅)
75 elprn1 42068 . . . . . . . . . 10 ((𝑦 ∈ {∅, {∅}} ∧ 𝑦 ≠ ∅) → 𝑦 = {∅})
7618, 75sylan2 595 . . . . . . . . 9 ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 = {∅})
77 unieq 4822 . . . . . . . . . 10 (𝑦 = {∅} → 𝑦 = {∅})
78 unisn0 41473 . . . . . . . . . 10 {∅} = ∅
7977, 78syl6eq 2872 . . . . . . . . 9 (𝑦 = {∅} → 𝑦 = ∅)
8076, 79syl 17 . . . . . . . 8 ((𝑦 ∈ {∅, {∅}} ∧ ¬ 𝑦 = ∅) → 𝑦 = ∅)
8174, 80pm2.61dan 812 . . . . . . 7 (𝑦 ∈ {∅, {∅}} → 𝑦 = ∅)
8270, 81syl 17 . . . . . 6 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋𝑦) → 𝑦 = ∅)
832a1i 11 . . . . . 6 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋𝑦) → ∅ ∈ {∅, 𝑋})
8482, 83eqeltrd 2912 . . . . 5 (((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) ∧ ¬ 𝑋𝑦) → 𝑦 ∈ {∅, 𝑋})
8541, 84pm2.61dan 812 . . . 4 ((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) → 𝑦 ∈ {∅, 𝑋})
8685a1d 25 . . 3 ((𝑋𝑉𝑦 ∈ 𝒫 {∅, 𝑋}) → (𝑦 ≼ ω → 𝑦 ∈ {∅, 𝑋}))
8786ralrimiva 3170 . 2 (𝑋𝑉 → ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → 𝑦 ∈ {∅, 𝑋}))
88 prex 5306 . . 3 {∅, 𝑋} ∈ V
89 issal 42749 . . 3 ({∅, 𝑋} ∈ V → ({∅, 𝑋} ∈ SAlg ↔ (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} ( {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → 𝑦 ∈ {∅, 𝑋}))))
9088, 89mp1i 13 . 2 (𝑋𝑉 → ({∅, 𝑋} ∈ SAlg ↔ (∅ ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ {∅, 𝑋} ( {∅, 𝑋} ∖ 𝑦) ∈ {∅, 𝑋} ∧ ∀𝑦 ∈ 𝒫 {∅, 𝑋} (𝑦 ≼ ω → 𝑦 ∈ {∅, 𝑋}))))
913, 30, 87, 90mpbir3and 1339 1 (𝑋𝑉 → {∅, 𝑋} ∈ SAlg)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   ≠ wne 3007  ∀wral 3126  Vcvv 3471   ∖ cdif 3907   ∪ cun 3908   ⊆ wss 3910  ∅c0 4266  𝒫 cpw 4512  {csn 4540  {cpr 4542  ∪ cuni 4811   class class class wbr 5039  ωcom 7555   ≼ cdom 8482  SAlgcsalg 42743 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303 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 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-pw 4514  df-sn 4541  df-pr 4543  df-uni 4812  df-salg 42744 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator