Metamath Proof Explorer

Theorem sigapisys

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

Ref Expression
Hypothesis ispisys.p 
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }
Assertion sigapisys 
|- ( sigAlgebra ` O ) C_ P

Proof

Step Hyp Ref Expression
1 ispisys.p 
 |-  P = { s e. ~P ~P O | ( fi ` s ) C_ 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 5 adantr 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. ( ( ~P t i^i Fin ) \ { (/) } ) ) -> t e. U. ran sigAlgebra )
7 eldifsn 
 |-  ( x e. ( ( ~P t i^i Fin ) \ { (/) } ) <-> ( x e. ( ~P t i^i Fin ) /\ x =/= (/) ) )
8 7 bilani 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. ( ( ~P t i^i Fin ) \ { (/) } ) ) -> ( x e. ( ~P t i^i Fin ) /\ x =/= (/) ) )
9 8 simpld 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. ( ( ~P t i^i Fin ) \ { (/) } ) ) -> x e. ( ~P t i^i Fin ) )
10 9 elin1d 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. ( ( ~P t i^i Fin ) \ { (/) } ) ) -> x e. ~P t )
11 9 elin2d 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. ( ( ~P t i^i Fin ) \ { (/) } ) ) -> x e. Fin )
12 fict 
 |-  ( x e. Fin -> x ~<_ _om )
13 11 12 syl 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. ( ( ~P t i^i Fin ) \ { (/) } ) ) -> x ~<_ _om )
14 8 simprd 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. ( ( ~P t i^i Fin ) \ { (/) } ) ) -> x =/= (/) )
15 sigaclci 
 |-  ( ( ( t e. U. ran sigAlgebra /\ x e. ~P t ) /\ ( x ~<_ _om /\ x =/= (/) ) ) -> |^| x e. t )
16 6 10 13 14 15 syl22anc 
 |-  ( ( t e. ( sigAlgebra ` O ) /\ x e. ( ( ~P t i^i Fin ) \ { (/) } ) ) -> |^| x e. t )
17 16 ralrimiva 
 |-  ( t e. ( sigAlgebra ` O ) -> A. x e. ( ( ~P t i^i Fin ) \ { (/) } ) |^| x e. t )
18 4 17 jca 
 |-  ( t e. ( sigAlgebra ` O ) -> ( t e. ~P ~P O /\ A. x e. ( ( ~P t i^i Fin ) \ { (/) } ) |^| x e. t ) )
19 1 ispisys2 
 |-  ( t e. P <-> ( t e. ~P ~P O /\ A. x e. ( ( ~P t i^i Fin ) \ { (/) } ) |^| x e. t ) )
20 18 19 sylibr 
 |-  ( t e. ( sigAlgebra ` O ) -> t e. P )
21 20 ssriv 
 |-  ( sigAlgebra ` O ) C_ P