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 ∈ 𝒫 𝒫 O | fi ⁡ s ⊆ s
Assertion sigapisys ⊢ sigAlgebra ⁡ O ⊆ P

Proof

Step Hyp Ref Expression
1 ispisys.p ⊢ P = s ∈ 𝒫 𝒫 O | fi ⁡ s ⊆ s
2 sigasspw ⊢ t ∈ sigAlgebra ⁡ O → t ⊆ 𝒫 O
3 velpw ⊢ t ∈ 𝒫 𝒫 O ↔ t ⊆ 𝒫 O
4 2 3 sylibr ⊢ t ∈ sigAlgebra ⁡ O → t ∈ 𝒫 𝒫 O
5 elrnsiga ⊢ t ∈ sigAlgebra ⁡ O → t ∈ ⋃ ran ⁡ sigAlgebra
6 5 adantr ⊢ t ∈ sigAlgebra ⁡ O ∧ x ∈ 𝒫 t ∩ Fin ∖ ∅ → t ∈ ⋃ ran ⁡ sigAlgebra
7 eldifsn ⊢ x ∈ 𝒫 t ∩ Fin ∖ ∅ ↔ x ∈ 𝒫 t ∩ Fin ∧ x ≠ ∅
8 7 bilani ⊢ t ∈ sigAlgebra ⁡ O ∧ x ∈ 𝒫 t ∩ Fin ∖ ∅ → x ∈ 𝒫 t ∩ Fin ∧ x ≠ ∅
9 8 simpld ⊢ t ∈ sigAlgebra ⁡ O ∧ x ∈ 𝒫 t ∩ Fin ∖ ∅ → x ∈ 𝒫 t ∩ Fin
10 9 elin1d ⊢ t ∈ sigAlgebra ⁡ O ∧ x ∈ 𝒫 t ∩ Fin ∖ ∅ → x ∈ 𝒫 t
11 9 elin2d ⊢ t ∈ sigAlgebra ⁡ O ∧ x ∈ 𝒫 t ∩ Fin ∖ ∅ → x ∈ Fin
12 fict ⊢ x ∈ Fin → x ≼ ω
13 11 12 syl ⊢ t ∈ sigAlgebra ⁡ O ∧ x ∈ 𝒫 t ∩ Fin ∖ ∅ → x ≼ ω
14 8 simprd ⊢ t ∈ sigAlgebra ⁡ O ∧ x ∈ 𝒫 t ∩ Fin ∖ ∅ → x ≠ ∅
15 sigaclci ⊢ t ∈ ⋃ ran ⁡ sigAlgebra ∧ x ∈ 𝒫 t ∧ x ≼ ω ∧ x ≠ ∅ → ⋂ x ∈ t
16 6 10 13 14 15 syl22anc ⊢ t ∈ sigAlgebra ⁡ O ∧ x ∈ 𝒫 t ∩ Fin ∖ ∅ → ⋂ x ∈ t
17 16 ralrimiva ⊢ t ∈ sigAlgebra ⁡ O → ∀ x ∈ 𝒫 t ∩ Fin ∖ ∅ ⋂ x ∈ t
18 4 17 jca ⊢ t ∈ sigAlgebra ⁡ O → t ∈ 𝒫 𝒫 O ∧ ∀ x ∈ 𝒫 t ∩ Fin ∖ ∅ ⋂ x ∈ t
19 1 ispisys2 ⊢ t ∈ P ↔ t ∈ 𝒫 𝒫 O ∧ ∀ x ∈ 𝒫 t ∩ Fin ∖ ∅ ⋂ x ∈ t
20 18 19 sylibr ⊢ t ∈ sigAlgebra ⁡ O → t ∈ P
21 20 ssriv ⊢ sigAlgebra ⁡ O ⊆ P