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 e. V -> { (/) , O } e. ( sigAlgebra ` O ) )

Proof

Step Hyp Ref Expression
1 0elpw 
 |-  (/) e. ~P O
2 pwidg 
 |-  ( O e. V -> O e. ~P O )
3 prssi 
 |-  ( ( (/) e. ~P O /\ O e. ~P O ) -> { (/) , O } C_ ~P O )
4 1 2 3 sylancr 
 |-  ( O e. V -> { (/) , O } C_ ~P O )
5 prid2g 
 |-  ( O e. V -> O e. { (/) , O } )
6 dif0 
 |-  ( O \ (/) ) = O
7 6 5 eqeltrid 
 |-  ( O e. V -> ( O \ (/) ) e. { (/) , O } )
8 difid 
 |-  ( O \ O ) = (/)
9 0ex 
 |-  (/) e. _V
10 9 prid1 
 |-  (/) e. { (/) , O }
11 10 a1i 
 |-  ( O e. V -> (/) e. { (/) , O } )
12 8 11 eqeltrid 
 |-  ( O e. V -> ( O \ O ) e. { (/) , O } )
13 difeq2 
 |-  ( x = (/) -> ( O \ x ) = ( O \ (/) ) )
14 13 eleq1d 
 |-  ( x = (/) -> ( ( O \ x ) e. { (/) , O } <-> ( O \ (/) ) e. { (/) , O } ) )
15 difeq2 
 |-  ( x = O -> ( O \ x ) = ( O \ O ) )
16 15 eleq1d 
 |-  ( x = O -> ( ( O \ x ) e. { (/) , O } <-> ( O \ O ) e. { (/) , O } ) )
17 14 16 ralprg 
 |-  ( ( (/) e. _V /\ O e. V ) -> ( A. x e. { (/) , O } ( O \ x ) e. { (/) , O } <-> ( ( O \ (/) ) e. { (/) , O } /\ ( O \ O ) e. { (/) , O } ) ) )
18 9 17 mpan 
 |-  ( O e. V -> ( A. x e. { (/) , O } ( O \ x ) e. { (/) , O } <-> ( ( O \ (/) ) e. { (/) , O } /\ ( O \ O ) e. { (/) , O } ) ) )
19 7 12 18 mpbir2and 
 |-  ( O e. V -> A. x e. { (/) , O } ( O \ x ) e. { (/) , O } )
20 uni0 
 |-  U. (/) = (/)
21 20 10 eqeltri 
 |-  U. (/) e. { (/) , O }
22 9 unisn 
 |-  U. { (/) } = (/)
23 22 10 eqeltri 
 |-  U. { (/) } e. { (/) , O }
24 21 23 pm3.2i 
 |-  ( U. (/) e. { (/) , O } /\ U. { (/) } e. { (/) , O } )
25 snex 
 |-  { (/) } e. _V
26 9 25 pm3.2i 
 |-  ( (/) e. _V /\ { (/) } e. _V )
27 unieq 
 |-  ( x = (/) -> U. x = U. (/) )
28 27 eleq1d 
 |-  ( x = (/) -> ( U. x e. { (/) , O } <-> U. (/) e. { (/) , O } ) )
29 unieq 
 |-  ( x = { (/) } -> U. x = U. { (/) } )
30 29 eleq1d 
 |-  ( x = { (/) } -> ( U. x e. { (/) , O } <-> U. { (/) } e. { (/) , O } ) )
31 28 30 ralprg 
 |-  ( ( (/) e. _V /\ { (/) } e. _V ) -> ( A. x e. { (/) , { (/) } } U. x e. { (/) , O } <-> ( U. (/) e. { (/) , O } /\ U. { (/) } e. { (/) , O } ) ) )
32 26 31 mp1i 
 |-  ( O e. V -> ( A. x e. { (/) , { (/) } } U. x e. { (/) , O } <-> ( U. (/) e. { (/) , O } /\ U. { (/) } e. { (/) , O } ) ) )
33 24 32 mpbiri 
 |-  ( O e. V -> A. x e. { (/) , { (/) } } U. x e. { (/) , O } )
34 unisng 
 |-  ( O e. V -> U. { O } = O )
35 34 5 eqeltrd 
 |-  ( O e. V -> U. { O } e. { (/) , O } )
36 uniprg 
 |-  ( ( (/) e. _V /\ O e. V ) -> U. { (/) , O } = ( (/) u. O ) )
37 9 36 mpan 
 |-  ( O e. V -> U. { (/) , O } = ( (/) u. O ) )
38 uncom 
 |-  ( (/) u. O ) = ( O u. (/) )
39 un0 
 |-  ( O u. (/) ) = O
40 38 39 eqtri 
 |-  ( (/) u. O ) = O
41 37 40 eqtrdi 
 |-  ( O e. V -> U. { (/) , O } = O )
42 41 5 eqeltrd 
 |-  ( O e. V -> U. { (/) , O } e. { (/) , O } )
43 snex 
 |-  { O } e. _V
44 prex 
 |-  { (/) , O } e. _V
45 43 44 pm3.2i 
 |-  ( { O } e. _V /\ { (/) , O } e. _V )
46 unieq 
 |-  ( x = { O } -> U. x = U. { O } )
47 46 eleq1d 
 |-  ( x = { O } -> ( U. x e. { (/) , O } <-> U. { O } e. { (/) , O } ) )
48 unieq 
 |-  ( x = { (/) , O } -> U. x = U. { (/) , O } )
49 48 eleq1d 
 |-  ( x = { (/) , O } -> ( U. x e. { (/) , O } <-> U. { (/) , O } e. { (/) , O } ) )
50 47 49 ralprg 
 |-  ( ( { O } e. _V /\ { (/) , O } e. _V ) -> ( A. x e. { { O } , { (/) , O } } U. x e. { (/) , O } <-> ( U. { O } e. { (/) , O } /\ U. { (/) , O } e. { (/) , O } ) ) )
51 45 50 mp1i 
 |-  ( O e. V -> ( A. x e. { { O } , { (/) , O } } U. x e. { (/) , O } <-> ( U. { O } e. { (/) , O } /\ U. { (/) , O } e. { (/) , O } ) ) )
52 35 42 51 mpbir2and 
 |-  ( O e. V -> A. x e. { { O } , { (/) , O } } U. x e. { (/) , O } )
53 ralun 
 |-  ( ( A. x e. { (/) , { (/) } } U. x e. { (/) , O } /\ A. x e. { { O } , { (/) , O } } U. x e. { (/) , O } ) -> A. x e. ( { (/) , { (/) } } u. { { O } , { (/) , O } } ) U. x e. { (/) , O } )
54 33 52 53 syl2anc 
 |-  ( O e. V -> A. x e. ( { (/) , { (/) } } u. { { O } , { (/) , O } } ) U. x e. { (/) , O } )
55 pwpr 
 |-  ~P { (/) , O } = ( { (/) , { (/) } } u. { { O } , { (/) , O } } )
56 55 raleqi 
 |-  ( A. x e. ~P { (/) , O } U. x e. { (/) , O } <-> A. x e. ( { (/) , { (/) } } u. { { O } , { (/) , O } } ) U. x e. { (/) , O } )
57 54 56 sylibr 
 |-  ( O e. V -> A. x e. ~P { (/) , O } U. x e. { (/) , O } )
58 ax-1 
 |-  ( U. x e. { (/) , O } -> ( x ~<_ _om -> U. x e. { (/) , O } ) )
59 58 ralimi 
 |-  ( A. x e. ~P { (/) , O } U. x e. { (/) , O } -> A. x e. ~P { (/) , O } ( x ~<_ _om -> U. x e. { (/) , O } ) )
60 57 59 syl 
 |-  ( O e. V -> A. x e. ~P { (/) , O } ( x ~<_ _om -> U. x e. { (/) , O } ) )
61 5 19 60 3jca 
 |-  ( O e. V -> ( O e. { (/) , O } /\ A. x e. { (/) , O } ( O \ x ) e. { (/) , O } /\ A. x e. ~P { (/) , O } ( x ~<_ _om -> U. x e. { (/) , O } ) ) )
62 issiga 
 |-  ( { (/) , O } e. _V -> ( { (/) , O } e. ( sigAlgebra ` O ) <-> ( { (/) , O } C_ ~P O /\ ( O e. { (/) , O } /\ A. x e. { (/) , O } ( O \ x ) e. { (/) , O } /\ A. x e. ~P { (/) , O } ( x ~<_ _om -> U. x e. { (/) , O } ) ) ) ) )
63 44 62 ax-mp 
 |-  ( { (/) , O } e. ( sigAlgebra ` O ) <-> ( { (/) , O } C_ ~P O /\ ( O e. { (/) , O } /\ A. x e. { (/) , O } ( O \ x ) e. { (/) , O } /\ A. x e. ~P { (/) , O } ( x ~<_ _om -> U. x e. { (/) , O } ) ) ) )
64 4 61 63 sylanbrc 
 |-  ( O e. V -> { (/) , O } e. ( sigAlgebra ` O ) )