Metamath Proof Explorer

Theorem prsal

Description: The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion prsal ( 𝑋 ∈ 𝑉 → { ∅ , 𝑋 } ∈ SAlg )

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 1 prid1 ⊢ ∅ ∈ { ∅ , 𝑋 }
3 2 a1i ⊢ ( 𝑋 ∈ 𝑉 → ∅ ∈ { ∅ , 𝑋 } )
4 uniprg ⊢ ( ( ∅ ∈ V ∧ 𝑋 ∈ 𝑉 ) → ∪ { ∅ , 𝑋 } = ( ∅ ∪ 𝑋 ) )
5 1 4 mpan ⊢ ( 𝑋 ∈ 𝑉 → ∪ { ∅ , 𝑋 } = ( ∅ ∪ 𝑋 ) )
6 0un ⊢ ( ∅ ∪ 𝑋 ) = 𝑋
7 5 6 eqtrdi ⊢ ( 𝑋 ∈ 𝑉 → ∪ { ∅ , 𝑋 } = 𝑋 )
8 7 difeq1d ⊢ ( 𝑋 ∈ 𝑉 → ( ∪ { ∅ , 𝑋 } ∖ 𝑦 ) = ( 𝑋 ∖ 𝑦 ) )
9 8 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { ∅ , 𝑋 } ) → ( ∪ { ∅ , 𝑋 } ∖ 𝑦 ) = ( 𝑋 ∖ 𝑦 ) )
10 difeq2 ⊢ ( 𝑦 = ∅ → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ ∅ ) )
11 10 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = ∅ ) → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ ∅ ) )
12 dif0 ⊢ ( 𝑋 ∖ ∅ ) = 𝑋
13 11 12 eqtrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = ∅ ) → ( 𝑋 ∖ 𝑦 ) = 𝑋 )
14 prid2g ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { ∅ , 𝑋 } )
15 14 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = ∅ ) → 𝑋 ∈ { ∅ , 𝑋 } )
16 13 15 eqeltrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = ∅ ) → ( 𝑋 ∖ 𝑦 ) ∈ { ∅ , 𝑋 } )
17 16 adantlr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { ∅ , 𝑋 } ) ∧ 𝑦 = ∅ ) → ( 𝑋 ∖ 𝑦 ) ∈ { ∅ , 𝑋 } )
18 neqne ⊢ ( ¬ 𝑦 = ∅ → 𝑦 ≠ ∅ )
19 elprn1 ⊢ ( ( 𝑦 ∈ { ∅ , 𝑋 } ∧ 𝑦 ≠ ∅ ) → 𝑦 = 𝑋 )
20 18 19 sylan2 ⊢ ( ( 𝑦 ∈ { ∅ , 𝑋 } ∧ ¬ 𝑦 = ∅ ) → 𝑦 = 𝑋 )
21 20 adantll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { ∅ , 𝑋 } ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 = 𝑋 )
22 difeq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑋 ) )
23 difid ⊢ ( 𝑋 ∖ 𝑋 ) = ∅
24 22 23 eqtrdi ⊢ ( 𝑦 = 𝑋 → ( 𝑋 ∖ 𝑦 ) = ∅ )
25 2 a1i ⊢ ( 𝑦 = 𝑋 → ∅ ∈ { ∅ , 𝑋 } )
26 24 25 eqeltrd ⊢ ( 𝑦 = 𝑋 → ( 𝑋 ∖ 𝑦 ) ∈ { ∅ , 𝑋 } )
27 21 26 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { ∅ , 𝑋 } ) ∧ ¬ 𝑦 = ∅ ) → ( 𝑋 ∖ 𝑦 ) ∈ { ∅ , 𝑋 } )
28 17 27 pm2.61dan ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { ∅ , 𝑋 } ) → ( 𝑋 ∖ 𝑦 ) ∈ { ∅ , 𝑋 } )
29 9 28 eqeltrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { ∅ , 𝑋 } ) → ( ∪ { ∅ , 𝑋 } ∖ 𝑦 ) ∈ { ∅ , 𝑋 } )
30 29 ralrimiva ⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑦 ∈ { ∅ , 𝑋 } ( ∪ { ∅ , 𝑋 } ∖ 𝑦 ) ∈ { ∅ , 𝑋 } )
31 elpwi ⊢ ( 𝑦 ∈ 𝒫 { ∅ , 𝑋 } → 𝑦 ⊆ { ∅ , 𝑋 } )
32 31 unissd ⊢ ( 𝑦 ∈ 𝒫 { ∅ , 𝑋 } → ∪ 𝑦 ⊆ ∪ { ∅ , 𝑋 } )
33 32 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) → ∪ 𝑦 ⊆ ∪ { ∅ , 𝑋 } )
34 7 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) → ∪ { ∅ , 𝑋 } = 𝑋 )
35 33 34 sseqtrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) → ∪ 𝑦 ⊆ 𝑋 )
36 35 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ 𝑋 ∈ 𝑦 ) → ∪ 𝑦 ⊆ 𝑋 )
37 elssuni ⊢ ( 𝑋 ∈ 𝑦 → 𝑋 ⊆ ∪ 𝑦 )
38 37 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ 𝑋 ∈ 𝑦 ) → 𝑋 ⊆ ∪ 𝑦 )
39 36 38 eqssd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ 𝑋 ∈ 𝑦 ) → ∪ 𝑦 = 𝑋 )
40 14 ad2antrr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ 𝑋 ∈ 𝑦 ) → 𝑋 ∈ { ∅ , 𝑋 } )
41 39 40 eqeltrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ 𝑋 ∈ 𝑦 ) → ∪ 𝑦 ∈ { ∅ , 𝑋 } )
42 id ⊢ ( 𝑦 ∈ 𝒫 { ∅ , 𝑋 } → 𝑦 ∈ 𝒫 { ∅ , 𝑋 } )
43 pwpr ⊢ 𝒫 { ∅ , 𝑋 } = ( { ∅ , { ∅ } } ∪ { { 𝑋 } , { ∅ , 𝑋 } } )
44 42 43 eleqtrdi ⊢ ( 𝑦 ∈ 𝒫 { ∅ , 𝑋 } → 𝑦 ∈ ( { ∅ , { ∅ } } ∪ { { 𝑋 } , { ∅ , 𝑋 } } ) )
45 44 adantr ⊢ ( ( 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ∧ ¬ 𝑋 ∈ 𝑦 ) → 𝑦 ∈ ( { ∅ , { ∅ } } ∪ { { 𝑋 } , { ∅ , 𝑋 } } ) )
46 45 adantll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ ¬ 𝑋 ∈ 𝑦 ) → 𝑦 ∈ ( { ∅ , { ∅ } } ∪ { { 𝑋 } , { ∅ , 𝑋 } } ) )
47 snidg ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
48 47 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = { 𝑋 } ) → 𝑋 ∈ { 𝑋 } )
49 id ⊢ ( 𝑦 = { 𝑋 } → 𝑦 = { 𝑋 } )
50 49 eqcomd ⊢ ( 𝑦 = { 𝑋 } → { 𝑋 } = 𝑦 )
51 50 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = { 𝑋 } ) → { 𝑋 } = 𝑦 )
52 48 51 eleqtrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = { 𝑋 } ) → 𝑋 ∈ 𝑦 )
53 52 adantlr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } ) ∧ 𝑦 = { 𝑋 } ) → 𝑋 ∈ 𝑦 )
54 id ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ 𝑉 )
55 54 ad2antrr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } ) ∧ ¬ 𝑦 = { 𝑋 } ) → 𝑋 ∈ 𝑉 )
56 neqne ⊢ ( ¬ 𝑦 = { 𝑋 } → 𝑦 ≠ { 𝑋 } )
57 elprn1 ⊢ ( ( 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } ∧ 𝑦 ≠ { 𝑋 } ) → 𝑦 = { ∅ , 𝑋 } )
58 56 57 sylan2 ⊢ ( ( 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } ∧ ¬ 𝑦 = { 𝑋 } ) → 𝑦 = { ∅ , 𝑋 } )
59 58 adantll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } ) ∧ ¬ 𝑦 = { 𝑋 } ) → 𝑦 = { ∅ , 𝑋 } )
60 14 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = { ∅ , 𝑋 } ) → 𝑋 ∈ { ∅ , 𝑋 } )
61 id ⊢ ( 𝑦 = { ∅ , 𝑋 } → 𝑦 = { ∅ , 𝑋 } )
62 61 eqcomd ⊢ ( 𝑦 = { ∅ , 𝑋 } → { ∅ , 𝑋 } = 𝑦 )
63 62 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = { ∅ , 𝑋 } ) → { ∅ , 𝑋 } = 𝑦 )
64 60 63 eleqtrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = { ∅ , 𝑋 } ) → 𝑋 ∈ 𝑦 )
65 55 59 64 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } ) ∧ ¬ 𝑦 = { 𝑋 } ) → 𝑋 ∈ 𝑦 )
66 53 65 pm2.61dan ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } ) → 𝑋 ∈ 𝑦 )
67 66 stoic1a ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑦 ) → ¬ 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } )
68 67 adantlr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ ¬ 𝑋 ∈ 𝑦 ) → ¬ 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } )
69 elunnel2 ⊢ ( ( 𝑦 ∈ ( { ∅ , { ∅ } } ∪ { { 𝑋 } , { ∅ , 𝑋 } } ) ∧ ¬ 𝑦 ∈ { { 𝑋 } , { ∅ , 𝑋 } } ) → 𝑦 ∈ { ∅ , { ∅ } } )
70 46 68 69 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ ¬ 𝑋 ∈ 𝑦 ) → 𝑦 ∈ { ∅ , { ∅ } } )
71 unieq ⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∪ ∅ )
72 uni0 ⊢ ∪ ∅ = ∅
73 71 72 eqtrdi ⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∅ )
74 73 adantl ⊢ ( ( 𝑦 ∈ { ∅ , { ∅ } } ∧ 𝑦 = ∅ ) → ∪ 𝑦 = ∅ )
75 elprn1 ⊢ ( ( 𝑦 ∈ { ∅ , { ∅ } } ∧ 𝑦 ≠ ∅ ) → 𝑦 = { ∅ } )
76 18 75 sylan2 ⊢ ( ( 𝑦 ∈ { ∅ , { ∅ } } ∧ ¬ 𝑦 = ∅ ) → 𝑦 = { ∅ } )
77 unieq ⊢ ( 𝑦 = { ∅ } → ∪ 𝑦 = ∪ { ∅ } )
78 unisn0 ⊢ ∪ { ∅ } = ∅
79 77 78 eqtrdi ⊢ ( 𝑦 = { ∅ } → ∪ 𝑦 = ∅ )
80 76 79 syl ⊢ ( ( 𝑦 ∈ { ∅ , { ∅ } } ∧ ¬ 𝑦 = ∅ ) → ∪ 𝑦 = ∅ )
81 74 80 pm2.61dan ⊢ ( 𝑦 ∈ { ∅ , { ∅ } } → ∪ 𝑦 = ∅ )
82 70 81 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ ¬ 𝑋 ∈ 𝑦 ) → ∪ 𝑦 = ∅ )
83 2 a1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ ¬ 𝑋 ∈ 𝑦 ) → ∅ ∈ { ∅ , 𝑋 } )
84 82 83 eqeltrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) ∧ ¬ 𝑋 ∈ 𝑦 ) → ∪ 𝑦 ∈ { ∅ , 𝑋 } )
85 41 84 pm2.61dan ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) → ∪ 𝑦 ∈ { ∅ , 𝑋 } )
86 85 a1d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ) → ( 𝑦 ≼ ω → ∪ 𝑦 ∈ { ∅ , 𝑋 } ) )
87 86 ralrimiva ⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ( 𝑦 ≼ ω → ∪ 𝑦 ∈ { ∅ , 𝑋 } ) )
88 prex ⊢ { ∅ , 𝑋 } ∈ V
89 issal ⊢ ( { ∅ , 𝑋 } ∈ V → ( { ∅ , 𝑋 } ∈ SAlg ↔ ( ∅ ∈ { ∅ , 𝑋 } ∧ ∀ 𝑦 ∈ { ∅ , 𝑋 } ( ∪ { ∅ , 𝑋 } ∖ 𝑦 ) ∈ { ∅ , 𝑋 } ∧ ∀ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ( 𝑦 ≼ ω → ∪ 𝑦 ∈ { ∅ , 𝑋 } ) ) ) )
90 88 89 mp1i ⊢ ( 𝑋 ∈ 𝑉 → ( { ∅ , 𝑋 } ∈ SAlg ↔ ( ∅ ∈ { ∅ , 𝑋 } ∧ ∀ 𝑦 ∈ { ∅ , 𝑋 } ( ∪ { ∅ , 𝑋 } ∖ 𝑦 ) ∈ { ∅ , 𝑋 } ∧ ∀ 𝑦 ∈ 𝒫 { ∅ , 𝑋 } ( 𝑦 ≼ ω → ∪ 𝑦 ∈ { ∅ , 𝑋 } ) ) ) )
91 3 30 87 90 mpbir3and ⊢ ( 𝑋 ∈ 𝑉 → { ∅ , 𝑋 } ∈ SAlg )