Metamath Proof Explorer

Theorem sigaldsys

Description: All sigma-algebras are lambda-systems. (Contributed by Thierry Arnoux, 13-Jun-2020)

Ref Expression
Hypothesis isldsys.l 
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
Assertion sigaldsys 
|- ( sigAlgebra ` O ) C_ L

Proof

Step Hyp Ref Expression
1 isldsys.l 
 |-  L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
2 sigasspw 
 |-  ( t e. ( sigAlgebra ` O ) -> t C_ ~P O )
3 velpw 
 |-  ( t e. ~P ~P O <-> t C_ ~P O )
4 2 3 sylibr 
 |-  ( t e. ( sigAlgebra ` O ) -> t e. ~P ~P O )
5 elrnsiga 
 |-  ( t e. ( sigAlgebra ` O ) -> t e. U. ran sigAlgebra )
6 0elsiga 
 |-  ( t e. U. ran sigAlgebra -> (/) e. t )
7 5 6 syl 
 |-  ( t e. ( sigAlgebra ` O ) -> (/) e. t )
8 5 adantr 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. t ) -> t e. U. ran sigAlgebra )
9 baselsiga 
 |-  ( t e. ( sigAlgebra ` O ) -> O e. t )
10 9 adantr 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. t ) -> O e. t )
11 simpr 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. t ) -> x e. t )
12 difelsiga 
 |-  ( ( t e. U. ran sigAlgebra /\ O e. t /\ x e. t ) -> ( O \ x ) e. t )
13 8 10 11 12 syl3anc 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. t ) -> ( O \ x ) e. t )
14 13 ralrimiva 
 |-  ( t e. ( sigAlgebra ` O ) -> A. x e. t ( O \ x ) e. t )
15 5 ad2antrr 
 |-  ( ( ( t e. ( sigAlgebra ` O ) /\ x e. ~P t ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> t e. U. ran sigAlgebra )
16 simplr 
 |-  ( ( ( t e. ( sigAlgebra ` O ) /\ x e. ~P t ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> x e. ~P t )
17 simprl 
 |-  ( ( ( t e. ( sigAlgebra ` O ) /\ x e. ~P t ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> x ~<_ _om )
18 sigaclcu 
 |-  ( ( t e. U. ran sigAlgebra /\ x e. ~P t /\ x ~<_ _om ) -> U. x e. t )
19 15 16 17 18 syl3anc 
 |-  ( ( ( t e. ( sigAlgebra ` O ) /\ x e. ~P t ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> U. x e. t )
20 19 ex 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. ~P t ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) )
21 20 ralrimiva 
 |-  ( t e. ( sigAlgebra ` O ) -> A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) )
22 7 14 21 3jca 
 |-  ( t e. ( sigAlgebra ` O ) -> ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) )
23 4 22 jca 
 |-  ( t e. ( sigAlgebra ` O ) -> ( t e. ~P ~P O /\ ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) ) )
24 1 isldsys 
 |-  ( t e. L <-> ( t e. ~P ~P O /\ ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) ) )
25 23 24 sylibr 
 |-  ( t e. ( sigAlgebra ` O ) -> t e. L )
26 25 ssriv 
 |-  ( sigAlgebra ` O ) C_ L