Metamath Proof Explorer

Theorem sigapildsys

Description: Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020)

Ref Expression
Hypotheses dynkin.p 
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }
dynkin.l 
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
Assertion sigapildsys 
|- ( sigAlgebra ` O ) = ( P i^i L )

Proof

Step Hyp Ref Expression
1 dynkin.p 
 |-  P = { s e. ~P ~P O | ( fi ` s ) C_ s }
2 dynkin.l 
 |-  L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
3 1 sigapisys 
 |-  ( sigAlgebra ` O ) C_ P
4 2 sigaldsys 
 |-  ( sigAlgebra ` O ) C_ L
5 3 4 ssini 
 |-  ( sigAlgebra ` O ) C_ ( P i^i L )
6 id 
 |-  ( t e. ( P i^i L ) -> t e. ( P i^i L ) )
7 6 elin1d 
 |-  ( t e. ( P i^i L ) -> t e. P )
8 1 ispisys 
 |-  ( t e. P <-> ( t e. ~P ~P O /\ ( fi ` t ) C_ t ) )
9 7 8 sylib 
 |-  ( t e. ( P i^i L ) -> ( t e. ~P ~P O /\ ( fi ` t ) C_ t ) )
10 9 simpld 
 |-  ( t e. ( P i^i L ) -> t e. ~P ~P O )
11 10 elpwid 
 |-  ( t e. ( P i^i L ) -> t C_ ~P O )
12 dif0 
 |-  ( O \ (/) ) = O
13 6 elin2d 
 |-  ( t e. ( P i^i L ) -> t e. L )
14 2 isldsys 
 |-  ( t e. L <-> ( t e. ~P ~P O /\ ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) ) )
15 13 14 sylib 
 |-  ( t e. ( P i^i L ) -> ( t e. ~P ~P O /\ ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) ) )
16 15 simprd 
 |-  ( t e. ( P i^i L ) -> ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) )
17 16 simp2d 
 |-  ( t e. ( P i^i L ) -> A. x e. t ( O \ x ) e. t )
18 16 simp1d 
 |-  ( t e. ( P i^i L ) -> (/) e. t )
19 difeq2 
 |-  ( x = (/) -> ( O \ x ) = ( O \ (/) ) )
20 eqidd 
 |-  ( x = (/) -> t = t )
21 19 20 eleq12d 
 |-  ( x = (/) -> ( ( O \ x ) e. t <-> ( O \ (/) ) e. t ) )
22 21 rspcv 
 |-  ( (/) e. t -> ( A. x e. t ( O \ x ) e. t -> ( O \ (/) ) e. t ) )
23 18 22 syl 
 |-  ( t e. ( P i^i L ) -> ( A. x e. t ( O \ x ) e. t -> ( O \ (/) ) e. t ) )
24 17 23 mpd 
 |-  ( t e. ( P i^i L ) -> ( O \ (/) ) e. t )
25 12 24 eqeltrrid 
 |-  ( t e. ( P i^i L ) -> O e. t )
26 unieq 
 |-  ( x = (/) -> U. x = U. (/) )
27 uni0 
 |-  U. (/) = (/)
28 26 27 eqtrdi 
 |-  ( x = (/) -> U. x = (/) )
29 28 adantl 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x = (/) ) -> U. x = (/) )
30 18 ad3antrrr 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x = (/) ) -> (/) e. t )
31 29 30 eqeltrd 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x = (/) ) -> U. x e. t )
32 vex 
 |-  x e. _V
33 32 0sdom 
 |-  ( (/) ~< x <-> x =/= (/) )
34 33 bilanri 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> (/) ~< x )
35 simplr 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> x ~<_ _om )
36 nnenom 
 |-  NN ~~ _om
37 36 ensymi 
 |-  _om ~~ NN
38 domentr 
 |-  ( ( x ~<_ _om /\ _om ~~ NN ) -> x ~<_ NN )
39 35 37 38 sylancl 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> x ~<_ NN )
40 fodomr 
 |-  ( ( (/) ~< x /\ x ~<_ NN ) -> E. f f : NN -onto-> x )
41 34 39 40 syl2anc 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> E. f f : NN -onto-> x )
42 fveq2 
 |-  ( n = i -> ( f ` n ) = ( f ` i ) )
43 42 iundisj 
 |-  U_ n e. NN ( f ` n ) = U_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) )
44 fofn 
 |-  ( f : NN -onto-> x -> f Fn NN )
45 fniunfv 
 |-  ( f Fn NN -> U_ n e. NN ( f ` n ) = U. ran f )
46 44 45 syl 
 |-  ( f : NN -onto-> x -> U_ n e. NN ( f ` n ) = U. ran f )
47 forn 
 |-  ( f : NN -onto-> x -> ran f = x )
48 47 unieqd 
 |-  ( f : NN -onto-> x -> U. ran f = U. x )
49 46 48 eqtrd 
 |-  ( f : NN -onto-> x -> U_ n e. NN ( f ` n ) = U. x )
50 43 49 eqtr3id 
 |-  ( f : NN -onto-> x -> U_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) = U. x )
51 50 adantl 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> U_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) = U. x )
52 fvex 
 |-  ( f ` n ) e. _V
53 difexg 
 |-  ( ( f ` n ) e. _V -> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) e. _V )
54 52 53 ax-mp 
 |-  ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) e. _V
55 54 dfiun3 
 |-  U_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) = U. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
56 nfv 
 |-  F/ n ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x )
57 nfcv 
 |-  F/_ n y
58 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
59 58 nfrn 
 |-  F/_ n ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
60 57 59 nfel 
 |-  F/ n y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
61 56 60 nfan 
 |-  F/ n ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) )
62 simpr 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
63 nfv 
 |-  F/ i ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x )
64 nfcv 
 |-  F/_ i y
65 nfcv 
 |-  F/_ i NN
66 nfcv 
 |-  F/_ i ( f ` n )
67 nfiu1 
 |-  F/_ i U_ i e. ( 1 ..^ n ) ( f ` i )
68 66 67 nfdif 
 |-  F/_ i ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) )
69 65 68 nfmpt 
 |-  F/_ i ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
70 69 nfrn 
 |-  F/_ i ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
71 64 70 nfel 
 |-  F/ i y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
72 63 71 nfan 
 |-  F/ i ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) )
73 nfv 
 |-  F/ i n e. NN
74 72 73 nfan 
 |-  F/ i ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN )
75 64 68 nfeq 
 |-  F/ i y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) )
76 74 75 nfan 
 |-  F/ i ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
77 6 ad7antr 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> t e. ( P i^i L ) )
78 simp-4r 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> x e. ~P t )
79 78 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> x e. ~P t )
80 79 elpwid 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> x C_ t )
81 fof 
 |-  ( f : NN -onto-> x -> f : NN --> x )
82 81 ad4antlr 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> f : NN --> x )
83 simplr 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> n e. NN )
84 82 83 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( f ` n ) e. x )
85 80 84 sseldd 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( f ` n ) e. t )
86 fzofi 
 |-  ( 1 ..^ n ) e. Fin
87 86 a1i 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( 1 ..^ n ) e. Fin )
88 80 adantr 
 |-  ( ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) /\ i e. ( 1 ..^ n ) ) -> x C_ t )
89 82 adantr 
 |-  ( ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) /\ i e. ( 1 ..^ n ) ) -> f : NN --> x )
90 fzossnn 
 |-  ( 1 ..^ n ) C_ NN
91 90 a1i 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( 1 ..^ n ) C_ NN )
92 91 sselda 
 |-  ( ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) /\ i e. ( 1 ..^ n ) ) -> i e. NN )
93 89 92 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) /\ i e. ( 1 ..^ n ) ) -> ( f ` i ) e. x )
94 88 93 sseldd 
 |-  ( ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) /\ i e. ( 1 ..^ n ) ) -> ( f ` i ) e. t )
95 1 2 76 77 85 87 94 sigapildsyslem 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) e. t )
96 62 95 eqeltrd 
 |-  ( ( ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) /\ n e. NN ) /\ y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> y e. t )
97 eqid 
 |-  ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) = ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
98 97 54 elrnmpti 
 |-  ( y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) <-> E. n e. NN y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
99 98 bilani 
 |-  ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) -> E. n e. NN y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
100 61 96 99 r19.29af 
 |-  ( ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) /\ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ) -> y e. t )
101 100 ex 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> ( y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> y e. t ) )
102 101 ssrdv 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) C_ t )
103 nnex 
 |-  NN e. _V
104 103 mptex 
 |-  ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. _V
105 104 rnex 
 |-  ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. _V
106 elpwg 
 |-  ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. _V -> ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. ~P t <-> ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) C_ t ) )
107 105 106 ax-mp 
 |-  ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. ~P t <-> ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) C_ t )
108 102 107 sylibr 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. ~P t )
109 16 simp3d 
 |-  ( t e. ( P i^i L ) -> A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) )
110 109 ad4antr 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) )
111 nnct 
 |-  NN ~<_ _om
112 mptct 
 |-  ( NN ~<_ _om -> ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om )
113 111 112 ax-mp 
 |-  ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om
114 rnct 
 |-  ( ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om -> ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om )
115 113 114 mp1i 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om )
116 42 iundisj2 
 |-  Disj_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) )
117 disjrnmpt 
 |-  ( Disj_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) -> Disj_ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) y )
118 116 117 mp1i 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> Disj_ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) y )
119 breq1 
 |-  ( x = ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( x ~<_ _om <-> ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om ) )
120 disjeq1 
 |-  ( x = ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( Disj_ y e. x y <-> Disj_ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) y ) )
121 119 120 anbi12d 
 |-  ( x = ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) <-> ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om /\ Disj_ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) y ) ) )
122 unieq 
 |-  ( x = ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> U. x = U. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) )
123 122 eleq1d 
 |-  ( x = ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( U. x e. t <-> U. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. t ) )
124 121 123 imbi12d 
 |-  ( x = ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) -> ( ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) <-> ( ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om /\ Disj_ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) y ) -> U. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. t ) ) )
125 124 rspcv 
 |-  ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. ~P t -> ( A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) -> ( ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om /\ Disj_ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) y ) -> U. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. t ) ) )
126 125 imp 
 |-  ( ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. ~P t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) -> ( ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om /\ Disj_ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) y ) -> U. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. t ) )
127 126 imp 
 |-  ( ( ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. ~P t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) /\ ( ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om /\ Disj_ y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) y ) ) -> U. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. t )
128 108 110 115 118 127 syl22anc 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> U. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. t )
129 55 128 eqeltrid 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> U_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) e. t )
130 51 129 eqeltrrd 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> U. x e. t )
131 41 130 exlimddv 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> U. x e. t )
132 31 131 pm2.61dane 
 |-  ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) -> U. x e. t )
133 132 ex 
 |-  ( ( t e. ( P i^i L ) /\ x e. ~P t ) -> ( x ~<_ _om -> U. x e. t ) )
134 133 ralrimiva 
 |-  ( t e. ( P i^i L ) -> A. x e. ~P t ( x ~<_ _om -> U. x e. t ) )
135 25 17 134 3jca 
 |-  ( t e. ( P i^i L ) -> ( O e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( x ~<_ _om -> U. x e. t ) ) )
136 11 135 jca 
 |-  ( t e. ( P i^i L ) -> ( t C_ ~P O /\ ( O e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( x ~<_ _om -> U. x e. t ) ) ) )
137 vex 
 |-  t e. _V
138 issiga 
 |-  ( t e. _V -> ( t e. ( sigAlgebra ` O ) <-> ( t C_ ~P O /\ ( O e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( x ~<_ _om -> U. x e. t ) ) ) ) )
139 137 138 ax-mp 
 |-  ( t e. ( sigAlgebra ` O ) <-> ( t C_ ~P O /\ ( O e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( x ~<_ _om -> U. x e. t ) ) ) )
140 136 139 sylibr 
 |-  ( t e. ( P i^i L ) -> t e. ( sigAlgebra ` O ) )
141 140 ssriv 
 |-  ( P i^i L ) C_ ( sigAlgebra ` O )
142 5 141 eqssi 
 |-  ( sigAlgebra ` O ) = ( P i^i L )