Theorem difelsiga

Description: A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016)

	Ref	Expression
Assertion	difelsiga	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )

Proof

Step	Hyp	Ref	Expression
1		simp2	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> A e. S )
2		elssuni	|- ( A e. S -> A C_ U. S )
3		difin2	|- ( A C_ U. S -> ( A \ B ) = ( ( U. S \ B ) i^i A ) )
4	1 2 3	3syl	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ B ) = ( ( U. S \ B ) i^i A ) )
5		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 ) ) ) )
6	5	simprd	|- ( S e. U. ran sigAlgebra -> ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
7	6	simp2d	|- ( S e. U. ran sigAlgebra -> A. x e. S ( U. S \ x ) e. S )
8		difeq2	|- ( x = B -> ( U. S \ x ) = ( U. S \ B ) )
9	8	eleq1d	|- ( x = B -> ( ( U. S \ x ) e. S <-> ( U. S \ B ) e. S ) )
10	9	rspccva	|- ( ( A. x e. S ( U. S \ x ) e. S /\ B e. S ) -> ( U. S \ B ) e. S )
11	7 10	sylan	|- ( ( S e. U. ran sigAlgebra /\ B e. S ) -> ( U. S \ B ) e. S )
12	11	3adant2	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( U. S \ B ) e. S )
13		intprg	|- ( ( ( U. S \ B ) e. S /\ A e. S ) -> |^| { ( U. S \ B ) , A } = ( ( U. S \ B ) i^i A ) )
14	12 1 13	syl2anc	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> |^| { ( U. S \ B ) , A } = ( ( U. S \ B ) i^i A ) )
15	4 14	eqtr4d	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ B ) = |^| { ( U. S \ B ) , A } )
16		simp1	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> S e. U. ran sigAlgebra )
17		prssi	|- ( ( ( U. S \ B ) e. S /\ A e. S ) -> { ( U. S \ B ) , A } C_ S )
18	12 1 17	syl2anc	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> { ( U. S \ B ) , A } C_ S )
19		prex	|- { ( U. S \ B ) , A } e. _V
20	19	elpw	|- ( { ( U. S \ B ) , A } e. ~P S <-> { ( U. S \ B ) , A } C_ S )
21	18 20	sylibr	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> { ( U. S \ B ) , A } e. ~P S )
22		prct	|- ( ( ( U. S \ B ) e. S /\ A e. S ) -> { ( U. S \ B ) , A } ~<_ _om )
23	12 1 22	syl2anc	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> { ( U. S \ B ) , A } ~<_ _om )
24		prnzg	|- ( ( U. S \ B ) e. S -> { ( U. S \ B ) , A } =/= (/) )
25	12 24	syl	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> { ( U. S \ B ) , A } =/= (/) )
26		sigaclci	|- ( ( ( S e. U. ran sigAlgebra /\ { ( U. S \ B ) , A } e. ~P S ) /\ ( { ( U. S \ B ) , A } ~<_ _om /\ { ( U. S \ B ) , A } =/= (/) ) ) -> |^| { ( U. S \ B ) , A } e. S )
27	16 21 23 25 26	syl22anc	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> |^| { ( U. S \ B ) , A } e. S )
28	15 27	eqeltrd	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )