Theorem sigapisys

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

	Ref	Expression
Hypothesis	ispisys.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
Assertion	sigapisys	⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ 𝑃

Proof

Step	Hyp	Ref	Expression
1		ispisys.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2		sigasspw	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑡 ⊆ 𝒫 𝑂 )
3		velpw	⊢ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ↔ 𝑡 ⊆ 𝒫 𝑂 )
4	2 3	sylibr	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑡 ∈ 𝒫 𝒫 𝑂 )
5		elrnsiga	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑡 ∈ ∪ ran sigAlgebra )
6	5	adantr	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑡 ∈ ∪ ran sigAlgebra )
7		eldifsn	⊢ ( 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ↔ ( 𝑥 ∈ ( 𝒫 𝑡 ∩ Fin ) ∧ 𝑥 ≠ ∅ ) )
8	7	bilani	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑥 ∈ ( 𝒫 𝑡 ∩ Fin ) ∧ 𝑥 ≠ ∅ ) )
9	8	simpld	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ ( 𝒫 𝑡 ∩ Fin ) )
10	9	elin1d	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ 𝒫 𝑡 )
11	9	elin2d	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ Fin )
12		fict	⊢ ( 𝑥 ∈ Fin → 𝑥 ≼ ω )
13	11 12	syl	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ≼ ω )
14	8	simprd	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ≠ ∅ )
15		sigaclci	⊢ ( ( ( 𝑡 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ ( 𝑥 ≼ ω ∧ 𝑥 ≠ ∅ ) ) → ∩ 𝑥 ∈ 𝑡 )
16	6 10 13 14 15	syl22anc	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑥 ∈ 𝑡 )
17	16	ralrimiva	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → ∀ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑡 )
18	4 17	jca	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑡 ) )
19	1	ispisys2	⊢ ( 𝑡 ∈ 𝑃 ↔ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑡 ) )
20	18 19	sylibr	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑡 ∈ 𝑃 )
21	20	ssriv	⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ 𝑃