Theorem isrnsigau

Description: The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016)

	Ref	Expression
Assertion	isrnsigau	|- ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sgon	|- ( S e. U. ran sigAlgebra -> S e. ( sigAlgebra ` U. S ) )
2		elex	|- ( S e. U. ran sigAlgebra -> S e. _V )
3		issiga	|- ( S e. _V -> ( S e. ( sigAlgebra ` U. S ) <-> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) ) )
4	2 3	syl	|- ( S e. U. ran sigAlgebra -> ( S e. ( sigAlgebra ` U. S ) <-> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) ) )
5	1 4	mpbid	|- ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )