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	biimpi	⊢ ( 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) → ( 𝑥 ∈ ( 𝒫 𝑡 ∩ Fin ) ∧ 𝑥 ≠ ∅ ) )
9	8	adantl	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑥 ∈ ( 𝒫 𝑡 ∩ Fin ) ∧ 𝑥 ≠ ∅ ) )
10	9	simpld	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ ( 𝒫 𝑡 ∩ Fin ) )
11	10	elin1d	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ 𝒫 𝑡 )
12	10	elin2d	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ Fin )
13		fict	⊢ ( 𝑥 ∈ Fin → 𝑥 ≼ ω )
14	12 13	syl	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ≼ ω )
15	9	simprd	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ≠ ∅ )
16		sigaclci	⊢ ( ( ( 𝑡 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ ( 𝑥 ≼ ω ∧ 𝑥 ≠ ∅ ) ) → ∩ 𝑥 ∈ 𝑡 )
17	6 11 14 15 16	syl22anc	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑥 ∈ 𝑡 )
18	17	ralrimiva	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → ∀ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑡 )
19	4 18	jca	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑡 ) )
20	1	ispisys2	⊢ ( 𝑡 ∈ 𝑃 ↔ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑡 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑡 ) )
21	19 20	sylibr	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑡 ∈ 𝑃 )
22	21	ssriv	⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ 𝑃