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