Metamath Proof Explorer


Theorem issald

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

Ref Expression
Hypotheses issald.s φ S V
issald.z φ S
issald.x X = S
issald.d φ y S X y S
issald.u φ y 𝒫 S y ω y S
Assertion issald φ S SAlg

Proof

Step Hyp Ref Expression
1 issald.s φ S V
2 issald.z φ S
3 issald.x X = S
4 issald.d φ y S X y S
5 issald.u φ y 𝒫 S y ω y S
6 3 eqcomi S = X
7 6 difeq1i S y = X y
8 7 4 eqeltrid φ y S S y S
9 8 ralrimiva φ y S S y S
10 5 3expia φ y 𝒫 S y ω y S
11 10 ralrimiva φ y 𝒫 S y ω y S
12 issal S V S SAlg S y S S y S y 𝒫 S y ω y S
13 1 12 syl φ S SAlg S y S S y S y 𝒫 S y ω y S
14 2 9 11 13 mpbir3and φ S SAlg