Theorem sigaldsys

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

	Ref	Expression
Hypothesis	isldsys.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
Assertion	sigaldsys	⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ 𝐿

Proof

Step	Hyp	Ref	Expression
1		isldsys.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
2		sigasspw	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑡 ⊆ 𝒫 𝑂 )
3		velpw	⊢ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ↔ 𝑡 ⊆ 𝒫 𝑂 )
4	2 3	sylibr	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑡 ∈ 𝒫 𝒫 𝑂 )
5		elrnsiga	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑡 ∈ ∪ ran sigAlgebra )
6		0elsiga	⊢ ( 𝑡 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑡 )
7	5 6	syl	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → ∅ ∈ 𝑡 )
8	5	adantr	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ 𝑡 ) → 𝑡 ∈ ∪ ran sigAlgebra )
9		baselsiga	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑂 ∈ 𝑡 )
10	9	adantr	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ 𝑡 ) → 𝑂 ∈ 𝑡 )
11		simpr	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ 𝑡 ) → 𝑥 ∈ 𝑡 )
12		difelsiga	⊢ ( ( 𝑡 ∈ ∪ ran sigAlgebra ∧ 𝑂 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
13	8 10 11 12	syl3anc	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ 𝑡 ) → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
14	13	ralrimiva	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
15	5	ad2antrr	⊢ ( ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑡 ∈ ∪ ran sigAlgebra )
16		simplr	⊢ ( ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑥 ∈ 𝒫 𝑡 )
17		simprl	⊢ ( ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑥 ≼ ω )
18		sigaclcu	⊢ ( ( 𝑡 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑡 ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑡 )
19	15 16 17 18	syl3anc	⊢ ( ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ∪ 𝑥 ∈ 𝑡 )
20	19	ex	⊢ ( ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) )
21	20	ralrimiva	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) )
22	7 14 21	3jca	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) )
23	4 22	jca	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ) )
24	1	isldsys	⊢ ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ) )
25	23 24	sylibr	⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑡 ∈ 𝐿 )
26	25	ssriv	⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ 𝐿