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 biimpri 
 |-  ( x =/= (/) -> (/) ~< x )
35 34 adantl 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> (/) ~< x )
36 simplr 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> x ~<_ _om )
37 nnenom 
 |-  NN ~~ _om
38 37 ensymi 
 |-  _om ~~ NN
39 domentr 
 |-  ( ( x ~<_ _om /\ _om ~~ NN ) -> x ~<_ NN )
40 36 38 39 sylancl 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> x ~<_ NN )
41 fodomr 
 |-  ( ( (/) ~< x /\ x ~<_ NN ) -> E. f f : NN -onto-> x )
42 35 40 41 syl2anc 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> E. f f : NN -onto-> x )
43 fveq2 
 |-  ( n = i -> ( f ` n ) = ( f ` i ) )
44 43 iundisj 
 |-  U_ n e. NN ( f ` n ) = U_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) )
45 fofn 
 |-  ( f : NN -onto-> x -> f Fn NN )
46 fniunfv 
 |-  ( f Fn NN -> U_ n e. NN ( f ` n ) = U. ran f )
47 45 46 syl 
 |-  ( f : NN -onto-> x -> U_ n e. NN ( f ` n ) = U. ran f )
48 forn 
 |-  ( f : NN -onto-> x -> ran f = x )
49 48 unieqd 
 |-  ( f : NN -onto-> x -> U. ran f = U. x )
50 47 49 eqtrd 
 |-  ( f : NN -onto-> x -> U_ n e. NN ( f ` n ) = U. x )
51 44 50 eqtr3id 
 |-  ( f : NN -onto-> x -> U_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) = U. x )
52 51 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 )
53 fvex 
 |-  ( f ` n ) e. _V
54 difexg 
 |-  ( ( f ` n ) e. _V -> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) e. _V )
55 53 54 ax-mp 
 |-  ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) e. _V
56 55 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 ) ) )
57 nfv 
 |-  F/ n ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x )
58 nfcv 
 |-  F/_ n y
59 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
60 59 nfrn 
 |-  F/_ n ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
61 58 60 nfel 
 |-  F/ n y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
62 57 61 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 ) ) ) )
63 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 ) ) )
64 nfv 
 |-  F/ i ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x )
65 nfcv 
 |-  F/_ i y
66 nfcv 
 |-  F/_ i NN
67 nfcv 
 |-  F/_ i ( f ` n )
68 nfiu1 
 |-  F/_ i U_ i e. ( 1 ..^ n ) ( f ` i )
69 67 68 nfdif 
 |-  F/_ i ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) )
70 66 69 nfmpt 
 |-  F/_ i ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
71 70 nfrn 
 |-  F/_ i ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
72 65 71 nfel 
 |-  F/ i y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) )
73 64 72 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 ) ) ) )
74 nfv 
 |-  F/ i n e. NN
75 73 74 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 )
76 65 69 nfeq 
 |-  F/ i y = ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) )
77 75 76 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 ) ) )
78 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 ) )
79 simp-4r 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> x e. ~P t )
80 79 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 )
81 80 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 )
82 fof 
 |-  ( f : NN -onto-> x -> f : NN --> x )
83 82 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 )
84 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 )
85 83 84 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 )
86 81 85 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 )
87 fzofi 
 |-  ( 1 ..^ n ) e. Fin
88 87 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 )
89 81 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 )
90 83 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 )
91 fzossnn 
 |-  ( 1 ..^ n ) C_ NN
92 91 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 )
93 92 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 )
94 90 93 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 )
95 89 94 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 )
96 1 2 77 78 86 88 95 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 )
97 63 96 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 )
98 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 ) ) ) ) -> y e. ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) )
99 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 ) ) )
100 99 55 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 ) ) )
101 98 100 sylib 
 |-  ( ( ( ( ( ( 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 ) ) )
102 62 97 101 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 )
103 102 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 ) )
104 103 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 )
105 nnex 
 |-  NN e. _V
106 105 mptex 
 |-  ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. _V
107 106 rnex 
 |-  ran ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) e. _V
108 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 ) )
109 107 108 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 )
110 104 109 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 )
111 16 simp3d 
 |-  ( t e. ( P i^i L ) -> A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) )
112 111 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 ) )
113 nnct 
 |-  NN ~<_ _om
114 mptct 
 |-  ( NN ~<_ _om -> ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om )
115 113 114 ax-mp 
 |-  ( n e. NN |-> ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) ) ) ~<_ _om
116 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 )
117 115 116 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 )
118 43 iundisj2 
 |-  Disj_ n e. NN ( ( f ` n ) \ U_ i e. ( 1 ..^ n ) ( f ` i ) )
119 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 )
120 118 119 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 )
121 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 ) )
122 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 ) )
123 121 122 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 ) ) )
124 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 ) ) ) )
125 124 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 ) )
126 123 125 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 ) ) )
127 126 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 ) ) )
128 127 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 ) )
129 128 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 )
130 110 112 117 120 129 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 )
131 56 130 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 )
132 52 131 eqeltrrd 
 |-  ( ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) /\ f : NN -onto-> x ) -> U. x e. t )
133 42 132 exlimddv 
 |-  ( ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) /\ x =/= (/) ) -> U. x e. t )
134 31 133 pm2.61dane 
 |-  ( ( ( t e. ( P i^i L ) /\ x e. ~P t ) /\ x ~<_ _om ) -> U. x e. t )
135 134 ex 
 |-  ( ( t e. ( P i^i L ) /\ x e. ~P t ) -> ( x ~<_ _om -> U. x e. t ) )
136 135 ralrimiva 
 |-  ( t e. ( P i^i L ) -> A. x e. ~P t ( x ~<_ _om -> U. x e. t ) )
137 25 17 136 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 ) ) )
138 11 137 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 ) ) ) )
139 vex 
 |-  t e. _V
140 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 ) ) ) ) )
141 139 140 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 ) ) ) )
142 138 141 sylibr 
 |-  ( t e. ( P i^i L ) -> t e. ( sigAlgebra ` O ) )
143 142 ssriv 
 |-  ( P i^i L ) C_ ( sigAlgebra ` O )
144 5 143 eqssi 
 |-  ( sigAlgebra ` O ) = ( P i^i L )