Theorem pwsiga

Description: Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016) (Revised by Thierry Arnoux, 24-Oct-2016)

	Ref	Expression
Assertion	pwsiga	|- ( O e. V -> ~P O e. ( sigAlgebra ` O ) )

Proof

Step	Hyp	Ref	Expression
1		ssidd	|- ( O e. V -> ~P O C_ ~P O )
2		pwidg	|- ( O e. V -> O e. ~P O )
3		difss	|- ( O \ x ) C_ O
4		elpw2g	|- ( O e. V -> ( ( O \ x ) e. ~P O <-> ( O \ x ) C_ O ) )
5	3 4	mpbiri	|- ( O e. V -> ( O \ x ) e. ~P O )
6	5	a1d	|- ( O e. V -> ( x e. ~P O -> ( O \ x ) e. ~P O ) )
7	6	ralrimiv	|- ( O e. V -> A. x e. ~P O ( O \ x ) e. ~P O )
8		sspwuni	|- ( x C_ ~P O <-> U. x C_ O )
9		vuniex	|- U. x e. _V
10	9	elpw	|- ( U. x e. ~P O <-> U. x C_ O )
11	8 10	bitr4i	|- ( x C_ ~P O <-> U. x e. ~P O )
12	11	biimpi	|- ( x C_ ~P O -> U. x e. ~P O )
13	12	a1d	|- ( x C_ ~P O -> ( x ~<_ _om -> U. x e. ~P O ) )
14		elpwi	|- ( x e. ~P ~P O -> x C_ ~P O )
15	14	imim1i	|- ( ( x C_ ~P O -> ( x ~<_ _om -> U. x e. ~P O ) ) -> ( x e. ~P ~P O -> ( x ~<_ _om -> U. x e. ~P O ) ) )
16	13 15	mp1i	|- ( O e. V -> ( x e. ~P ~P O -> ( x ~<_ _om -> U. x e. ~P O ) ) )
17	16	ralrimiv	|- ( O e. V -> A. x e. ~P ~P O ( x ~<_ _om -> U. x e. ~P O ) )
18	2 7 17	3jca	|- ( O e. V -> ( O e. ~P O /\ A. x e. ~P O ( O \ x ) e. ~P O /\ A. x e. ~P ~P O ( x ~<_ _om -> U. x e. ~P O ) ) )
19		pwexg	|- ( O e. V -> ~P O e. _V )
20		issiga	|- ( ~P O e. _V -> ( ~P O e. ( sigAlgebra ` O ) <-> ( ~P O C_ ~P O /\ ( O e. ~P O /\ A. x e. ~P O ( O \ x ) e. ~P O /\ A. x e. ~P ~P O ( x ~<_ _om -> U. x e. ~P O ) ) ) ) )
21	19 20	syl	|- ( O e. V -> ( ~P O e. ( sigAlgebra ` O ) <-> ( ~P O C_ ~P O /\ ( O e. ~P O /\ A. x e. ~P O ( O \ x ) e. ~P O /\ A. x e. ~P ~P O ( x ~<_ _om -> U. x e. ~P O ) ) ) ) )
22	1 18 21	mpbir2and	|- ( O e. V -> ~P O e. ( sigAlgebra ` O ) )