Theorem issald

Description: Sufficient condition to prove that S is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	issald.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	issald.z	⊢ ( 𝜑 → ∅ ∈ 𝑆 )
	issald.x	⊢ 𝑋 = ∪ 𝑆
	issald.d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑋 ∖ 𝑦 ) ∈ 𝑆 )
	issald.u	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) → ∪ 𝑦 ∈ 𝑆 )
Assertion	issald	⊢ ( 𝜑 → 𝑆 ∈ SAlg )

Proof

Step	Hyp	Ref	Expression
1		issald.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
2		issald.z	⊢ ( 𝜑 → ∅ ∈ 𝑆 )
3		issald.x	⊢ 𝑋 = ∪ 𝑆
4		issald.d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑋 ∖ 𝑦 ) ∈ 𝑆 )
5		issald.u	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) → ∪ 𝑦 ∈ 𝑆 )
6	3	eqcomi	⊢ ∪ 𝑆 = 𝑋
7	6	difeq1i	⊢ ( ∪ 𝑆 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑦 )
8	7 4	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 )
9	8	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 )
10	5	3expia	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ) → ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) )
11	10	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) )
12		issal	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )
13	1 12	syl	⊢ ( 𝜑 → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )
14	2 9 11 13	mpbir3and	⊢ ( 𝜑 → 𝑆 ∈ SAlg )