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 
|- ( ph -> S e. V )
issalnnd.z 
|- ( ph -> (/) e. S )
issalnnd.x 
|- X = U. S
issalnnd.d 
|- ( ( ph /\ y e. S ) -> ( X \ y ) e. S )
issalnnd.i 
|- ( ( ph /\ e : NN --> S ) -> U_ n e. NN ( e ` n ) e. S )
Assertion issalnnd 
|- ( ph -> S e. SAlg )

Proof

Step Hyp Ref Expression
1 issalnnd.s 
 |-  ( ph -> S e. V )
2 issalnnd.z 
 |-  ( ph -> (/) e. S )
3 issalnnd.x 
 |-  X = U. S
4 issalnnd.d 
 |-  ( ( ph /\ y e. S ) -> ( X \ y ) e. S )
5 issalnnd.i 
 |-  ( ( ph /\ e : NN --> S ) -> U_ n e. NN ( e ` n ) e. S )
6 unieq 
 |-  ( y = (/) -> U. y = U. (/) )
7 uni0 
 |-  U. (/) = (/)
8 7 a1i 
 |-  ( y = (/) -> U. (/) = (/) )
9 6 8 eqtrd 
 |-  ( y = (/) -> U. y = (/) )
10 9 adantl 
 |-  ( ( ph /\ y = (/) ) -> U. y = (/) )
11 2 adantr 
 |-  ( ( ph /\ y = (/) ) -> (/) e. S )
12 10 11 eqeltrd 
 |-  ( ( ph /\ y = (/) ) -> U. y e. S )
13 12 3ad2antl1 
 |-  ( ( ( ph /\ y e. ~P S /\ y ~<_ _om ) /\ y = (/) ) -> U. y e. S )
14 neqne 
 |-  ( -. y = (/) -> y =/= (/) )
15 14 adantl 
 |-  ( ( ( ph /\ y e. ~P S /\ y ~<_ _om ) /\ -. y = (/) ) -> y =/= (/) )
16 nnfoctb 
 |-  ( ( y ~<_ _om /\ y =/= (/) ) -> E. e e : NN -onto-> y )
17 16 3ad2antl3 
 |-  ( ( ( ph /\ y e. ~P S /\ y ~<_ _om ) /\ y =/= (/) ) -> E. e e : NN -onto-> y )
18 founiiun 
 |-  ( e : NN -onto-> y -> U. y = U_ n e. NN ( e ` n ) )
19 18 adantl 
 |-  ( ( ( ph /\ y e. ~P S ) /\ e : NN -onto-> y ) -> U. y = U_ n e. NN ( e ` n ) )
20 simpll 
 |-  ( ( ( ph /\ y e. ~P S ) /\ e : NN -onto-> y ) -> ph )
21 fof 
 |-  ( e : NN -onto-> y -> e : NN --> y )
22 21 adantl 
 |-  ( ( y e. ~P S /\ e : NN -onto-> y ) -> e : NN --> y )
23 elpwi 
 |-  ( y e. ~P S -> y C_ S )
24 23 adantr 
 |-  ( ( y e. ~P S /\ e : NN -onto-> y ) -> y C_ S )
25 22 24 fssd 
 |-  ( ( y e. ~P S /\ e : NN -onto-> y ) -> e : NN --> S )
26 25 adantll 
 |-  ( ( ( ph /\ y e. ~P S ) /\ e : NN -onto-> y ) -> e : NN --> S )
27 20 26 5 syl2anc 
 |-  ( ( ( ph /\ y e. ~P S ) /\ e : NN -onto-> y ) -> U_ n e. NN ( e ` n ) e. S )
28 19 27 eqeltrd 
 |-  ( ( ( ph /\ y e. ~P S ) /\ e : NN -onto-> y ) -> U. y e. S )
29 28 ex 
 |-  ( ( ph /\ y e. ~P S ) -> ( e : NN -onto-> y -> U. y e. S ) )
30 29 adantr 
 |-  ( ( ( ph /\ y e. ~P S ) /\ y =/= (/) ) -> ( e : NN -onto-> y -> U. y e. S ) )
31 30 3adantl3 
 |-  ( ( ( ph /\ y e. ~P S /\ y ~<_ _om ) /\ y =/= (/) ) -> ( e : NN -onto-> y -> U. y e. S ) )
32 31 exlimdv 
 |-  ( ( ( ph /\ y e. ~P S /\ y ~<_ _om ) /\ y =/= (/) ) -> ( E. e e : NN -onto-> y -> U. y e. S ) )
33 17 32 mpd 
 |-  ( ( ( ph /\ y e. ~P S /\ y ~<_ _om ) /\ y =/= (/) ) -> U. y e. S )
34 15 33 syldan 
 |-  ( ( ( ph /\ y e. ~P S /\ y ~<_ _om ) /\ -. y = (/) ) -> U. y e. S )
35 13 34 pm2.61dan 
 |-  ( ( ph /\ y e. ~P S /\ y ~<_ _om ) -> U. y e. S )
36 1 2 3 4 35 issald 
 |-  ( ph -> S e. SAlg )