Metamath Proof Explorer

Theorem prsiga

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

Ref Expression
Assertion prsiga ⊢ O ∈ V → ∅ O ∈ sigAlgebra ⁡ O

Proof

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