Metamath Proof Explorer

Theorem prsiga

Description: The smallest possible sigma-algebra containing O . (Contributed by Thierry Arnoux, 13-Sep-2016)

Ref Expression
Assertion prsiga ( 𝑂 ∈ 𝑉 → { ∅ , 𝑂 } ∈ ( sigAlgebra ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 0elpw ⊢ ∅ ∈ 𝒫 𝑂
2 pwidg ⊢ ( 𝑂 ∈ 𝑉 → 𝑂 ∈ 𝒫 𝑂 )
3 prssi ⊢ ( ( ∅ ∈ 𝒫 𝑂 ∧ 𝑂 ∈ 𝒫 𝑂 ) → { ∅ , 𝑂 } ⊆ 𝒫 𝑂 )
4 1 2 3 sylancr ⊢ ( 𝑂 ∈ 𝑉 → { ∅ , 𝑂 } ⊆ 𝒫 𝑂 )
5 prid2g ⊢ ( 𝑂 ∈ 𝑉 → 𝑂 ∈ { ∅ , 𝑂 } )
6 dif0 ⊢ ( 𝑂 ∖ ∅ ) = 𝑂
7 6 5 eqeltrid ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑂 ∖ ∅ ) ∈ { ∅ , 𝑂 } )
8 difid ⊢ ( 𝑂 ∖ 𝑂 ) = ∅
9 0ex ⊢ ∅ ∈ V
10 9 prid1 ⊢ ∅ ∈ { ∅ , 𝑂 }
11 10 a1i ⊢ ( 𝑂 ∈ 𝑉 → ∅ ∈ { ∅ , 𝑂 } )
12 8 11 eqeltrid ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑂 ∖ 𝑂 ) ∈ { ∅ , 𝑂 } )
13 difeq2 ⊢ ( 𝑥 = ∅ → ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ ∅ ) )
14 13 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝑂 ∖ 𝑥 ) ∈ { ∅ , 𝑂 } ↔ ( 𝑂 ∖ ∅ ) ∈ { ∅ , 𝑂 } ) )
15 difeq2 ⊢ ( 𝑥 = 𝑂 → ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ 𝑂 ) )
16 15 eleq1d ⊢ ( 𝑥 = 𝑂 → ( ( 𝑂 ∖ 𝑥 ) ∈ { ∅ , 𝑂 } ↔ ( 𝑂 ∖ 𝑂 ) ∈ { ∅ , 𝑂 } ) )
17 14 16 ralprg ⊢ ( ( ∅ ∈ V ∧ 𝑂 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ { ∅ , 𝑂 } ( 𝑂 ∖ 𝑥 ) ∈ { ∅ , 𝑂 } ↔ ( ( 𝑂 ∖ ∅ ) ∈ { ∅ , 𝑂 } ∧ ( 𝑂 ∖ 𝑂 ) ∈ { ∅ , 𝑂 } ) ) )
18 9 17 mpan ⊢ ( 𝑂 ∈ 𝑉 → ( ∀ 𝑥 ∈ { ∅ , 𝑂 } ( 𝑂 ∖ 𝑥 ) ∈ { ∅ , 𝑂 } ↔ ( ( 𝑂 ∖ ∅ ) ∈ { ∅ , 𝑂 } ∧ ( 𝑂 ∖ 𝑂 ) ∈ { ∅ , 𝑂 } ) ) )
19 7 12 18 mpbir2and ⊢ ( 𝑂 ∈ 𝑉 → ∀ 𝑥 ∈ { ∅ , 𝑂 } ( 𝑂 ∖ 𝑥 ) ∈ { ∅ , 𝑂 } )
20 uni0 ⊢ ∪ ∅ = ∅
21 20 10 eqeltri ⊢ ∪ ∅ ∈ { ∅ , 𝑂 }
22 9 unisn ⊢ ∪ { ∅ } = ∅
23 22 10 eqeltri ⊢ ∪ { ∅ } ∈ { ∅ , 𝑂 }
24 21 23 pm3.2i ⊢ ( ∪ ∅ ∈ { ∅ , 𝑂 } ∧ ∪ { ∅ } ∈ { ∅ , 𝑂 } )
25 snex ⊢ { ∅ } ∈ V
26 9 25 pm3.2i ⊢ ( ∅ ∈ V ∧ { ∅ } ∈ V )
27 unieq ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∪ ∅ )
28 27 eleq1d ⊢ ( 𝑥 = ∅ → ( ∪ 𝑥 ∈ { ∅ , 𝑂 } ↔ ∪ ∅ ∈ { ∅ , 𝑂 } ) )
29 unieq ⊢ ( 𝑥 = { ∅ } → ∪ 𝑥 = ∪ { ∅ } )
30 29 eleq1d ⊢ ( 𝑥 = { ∅ } → ( ∪ 𝑥 ∈ { ∅ , 𝑂 } ↔ ∪ { ∅ } ∈ { ∅ , 𝑂 } ) )
31 28 30 ralprg ⊢ ( ( ∅ ∈ V ∧ { ∅ } ∈ V ) → ( ∀ 𝑥 ∈ { ∅ , { ∅ } } ∪ 𝑥 ∈ { ∅ , 𝑂 } ↔ ( ∪ ∅ ∈ { ∅ , 𝑂 } ∧ ∪ { ∅ } ∈ { ∅ , 𝑂 } ) ) )
32 26 31 mp1i ⊢ ( 𝑂 ∈ 𝑉 → ( ∀ 𝑥 ∈ { ∅ , { ∅ } } ∪ 𝑥 ∈ { ∅ , 𝑂 } ↔ ( ∪ ∅ ∈ { ∅ , 𝑂 } ∧ ∪ { ∅ } ∈ { ∅ , 𝑂 } ) ) )
33 24 32 mpbiri ⊢ ( 𝑂 ∈ 𝑉 → ∀ 𝑥 ∈ { ∅ , { ∅ } } ∪ 𝑥 ∈ { ∅ , 𝑂 } )
34 unisng ⊢ ( 𝑂 ∈ 𝑉 → ∪ { 𝑂 } = 𝑂 )
35 34 5 eqeltrd ⊢ ( 𝑂 ∈ 𝑉 → ∪ { 𝑂 } ∈ { ∅ , 𝑂 } )
36 uniprg ⊢ ( ( ∅ ∈ V ∧ 𝑂 ∈ 𝑉 ) → ∪ { ∅ , 𝑂 } = ( ∅ ∪ 𝑂 ) )
37 9 36 mpan ⊢ ( 𝑂 ∈ 𝑉 → ∪ { ∅ , 𝑂 } = ( ∅ ∪ 𝑂 ) )
38 uncom ⊢ ( ∅ ∪ 𝑂 ) = ( 𝑂 ∪ ∅ )
39 un0 ⊢ ( 𝑂 ∪ ∅ ) = 𝑂
40 38 39 eqtri ⊢ ( ∅ ∪ 𝑂 ) = 𝑂
41 37 40 eqtrdi ⊢ ( 𝑂 ∈ 𝑉 → ∪ { ∅ , 𝑂 } = 𝑂 )
42 41 5 eqeltrd ⊢ ( 𝑂 ∈ 𝑉 → ∪ { ∅ , 𝑂 } ∈ { ∅ , 𝑂 } )
43 snex ⊢ { 𝑂 } ∈ V
44 prex ⊢ { ∅ , 𝑂 } ∈ V
45 43 44 pm3.2i ⊢ ( { 𝑂 } ∈ V ∧ { ∅ , 𝑂 } ∈ V )
46 unieq ⊢ ( 𝑥 = { 𝑂 } → ∪ 𝑥 = ∪ { 𝑂 } )
47 46 eleq1d ⊢ ( 𝑥 = { 𝑂 } → ( ∪ 𝑥 ∈ { ∅ , 𝑂 } ↔ ∪ { 𝑂 } ∈ { ∅ , 𝑂 } ) )
48 unieq ⊢ ( 𝑥 = { ∅ , 𝑂 } → ∪ 𝑥 = ∪ { ∅ , 𝑂 } )
49 48 eleq1d ⊢ ( 𝑥 = { ∅ , 𝑂 } → ( ∪ 𝑥 ∈ { ∅ , 𝑂 } ↔ ∪ { ∅ , 𝑂 } ∈ { ∅ , 𝑂 } ) )
50 47 49 ralprg ⊢ ( ( { 𝑂 } ∈ V ∧ { ∅ , 𝑂 } ∈ V ) → ( ∀ 𝑥 ∈ { { 𝑂 } , { ∅ , 𝑂 } } ∪ 𝑥 ∈ { ∅ , 𝑂 } ↔ ( ∪ { 𝑂 } ∈ { ∅ , 𝑂 } ∧ ∪ { ∅ , 𝑂 } ∈ { ∅ , 𝑂 } ) ) )
51 45 50 mp1i ⊢ ( 𝑂 ∈ 𝑉 → ( ∀ 𝑥 ∈ { { 𝑂 } , { ∅ , 𝑂 } } ∪ 𝑥 ∈ { ∅ , 𝑂 } ↔ ( ∪ { 𝑂 } ∈ { ∅ , 𝑂 } ∧ ∪ { ∅ , 𝑂 } ∈ { ∅ , 𝑂 } ) ) )
52 35 42 51 mpbir2and ⊢ ( 𝑂 ∈ 𝑉 → ∀ 𝑥 ∈ { { 𝑂 } , { ∅ , 𝑂 } } ∪ 𝑥 ∈ { ∅ , 𝑂 } )
53 ralun ⊢ ( ( ∀ 𝑥 ∈ { ∅ , { ∅ } } ∪ 𝑥 ∈ { ∅ , 𝑂 } ∧ ∀ 𝑥 ∈ { { 𝑂 } , { ∅ , 𝑂 } } ∪ 𝑥 ∈ { ∅ , 𝑂 } ) → ∀ 𝑥 ∈ ( { ∅ , { ∅ } } ∪ { { 𝑂 } , { ∅ , 𝑂 } } ) ∪ 𝑥 ∈ { ∅ , 𝑂 } )
54 33 52 53 syl2anc ⊢ ( 𝑂 ∈ 𝑉 → ∀ 𝑥 ∈ ( { ∅ , { ∅ } } ∪ { { 𝑂 } , { ∅ , 𝑂 } } ) ∪ 𝑥 ∈ { ∅ , 𝑂 } )
55 pwpr ⊢ 𝒫 { ∅ , 𝑂 } = ( { ∅ , { ∅ } } ∪ { { 𝑂 } , { ∅ , 𝑂 } } )
56 55 raleqi ⊢ ( ∀ 𝑥 ∈ 𝒫 { ∅ , 𝑂 } ∪ 𝑥 ∈ { ∅ , 𝑂 } ↔ ∀ 𝑥 ∈ ( { ∅ , { ∅ } } ∪ { { 𝑂 } , { ∅ , 𝑂 } } ) ∪ 𝑥 ∈ { ∅ , 𝑂 } )
57 54 56 sylibr ⊢ ( 𝑂 ∈ 𝑉 → ∀ 𝑥 ∈ 𝒫 { ∅ , 𝑂 } ∪ 𝑥 ∈ { ∅ , 𝑂 } )
58 ax-1 ⊢ ( ∪ 𝑥 ∈ { ∅ , 𝑂 } → ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { ∅ , 𝑂 } ) )
59 58 ralimi ⊢ ( ∀ 𝑥 ∈ 𝒫 { ∅ , 𝑂 } ∪ 𝑥 ∈ { ∅ , 𝑂 } → ∀ 𝑥 ∈ 𝒫 { ∅ , 𝑂 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { ∅ , 𝑂 } ) )
60 57 59 syl ⊢ ( 𝑂 ∈ 𝑉 → ∀ 𝑥 ∈ 𝒫 { ∅ , 𝑂 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { ∅ , 𝑂 } ) )
61 5 19 60 3jca ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑂 ∈ { ∅ , 𝑂 } ∧ ∀ 𝑥 ∈ { ∅ , 𝑂 } ( 𝑂 ∖ 𝑥 ) ∈ { ∅ , 𝑂 } ∧ ∀ 𝑥 ∈ 𝒫 { ∅ , 𝑂 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { ∅ , 𝑂 } ) ) )
62 issiga ⊢ ( { ∅ , 𝑂 } ∈ V → ( { ∅ , 𝑂 } ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( { ∅ , 𝑂 } ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ { ∅ , 𝑂 } ∧ ∀ 𝑥 ∈ { ∅ , 𝑂 } ( 𝑂 ∖ 𝑥 ) ∈ { ∅ , 𝑂 } ∧ ∀ 𝑥 ∈ 𝒫 { ∅ , 𝑂 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { ∅ , 𝑂 } ) ) ) ) )
63 44 62 ax-mp ⊢ ( { ∅ , 𝑂 } ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( { ∅ , 𝑂 } ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ { ∅ , 𝑂 } ∧ ∀ 𝑥 ∈ { ∅ , 𝑂 } ( 𝑂 ∖ 𝑥 ) ∈ { ∅ , 𝑂 } ∧ ∀ 𝑥 ∈ 𝒫 { ∅ , 𝑂 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { ∅ , 𝑂 } ) ) ) )
64 4 61 63 sylanbrc ⊢ ( 𝑂 ∈ 𝑉 → { ∅ , 𝑂 } ∈ ( sigAlgebra ‘ 𝑂 ) )