Metamath Proof Explorer


Theorem issalnnd

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

Ref Expression
Hypotheses issalnnd.s φ S V
issalnnd.z φ S
issalnnd.x X = S
issalnnd.d φ y S X y S
issalnnd.i φ e : S n e n S
Assertion issalnnd φ S SAlg

Proof

Step Hyp Ref Expression
1 issalnnd.s φ S V
2 issalnnd.z φ S
3 issalnnd.x X = S
4 issalnnd.d φ y S X y S
5 issalnnd.i φ e : S n e n S
6 unieq y = y =
7 uni0 =
8 7 a1i y = =
9 6 8 eqtrd y = y =
10 9 adantl φ y = y =
11 2 adantr φ y = S
12 10 11 eqeltrd φ y = y S
13 12 3ad2antl1 φ y 𝒫 S y ω y = y S
14 neqne ¬ y = y
15 14 adantl φ y 𝒫 S y ω ¬ y = y
16 nnfoctb y ω y e e : onto y
17 16 3ad2antl3 φ y 𝒫 S y ω y e e : onto y
18 founiiun e : onto y y = n e n
19 18 adantl φ y 𝒫 S e : onto y y = n e n
20 simpll φ y 𝒫 S e : onto y φ
21 fof e : onto y e : y
22 21 adantl y 𝒫 S e : onto y e : y
23 elpwi y 𝒫 S y S
24 23 adantr y 𝒫 S e : onto y y S
25 22 24 fssd y 𝒫 S e : onto y e : S
26 25 adantll φ y 𝒫 S e : onto y e : S
27 20 26 5 syl2anc φ y 𝒫 S e : onto y n e n S
28 19 27 eqeltrd φ y 𝒫 S e : onto y y S
29 28 ex φ y 𝒫 S e : onto y y S
30 29 adantr φ y 𝒫 S y e : onto y y S
31 30 3adantl3 φ y 𝒫 S y ω y e : onto y y S
32 31 exlimdv φ y 𝒫 S y ω y e e : onto y y S
33 17 32 mpd φ y 𝒫 S y ω y y S
34 15 33 syldan φ y 𝒫 S y ω ¬ y = y S
35 13 34 pm2.61dan φ y 𝒫 S y ω y S
36 1 2 3 4 35 issald φ S SAlg