Metamath Proof Explorer

Theorem dyadmbl

Description: Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses dyadmbl.1 
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
dyadmbl.2 
|- G = { z e. A | A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) }
dyadmbl.3 
|- ( ph -> A C_ ran F )
Assertion dyadmbl 
|- ( ph -> U. ( [,] " A ) e. dom vol )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 dyadmbl.2 
 |-  G = { z e. A | A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) }
3 dyadmbl.3 
 |-  ( ph -> A C_ ran F )
4 1 2 3 dyadmbllem 
 |-  ( ph -> U. ( [,] " A ) = U. ( [,] " G ) )
5 isfinite 
 |-  ( G e. Fin <-> G ~< _om )
6 iccf 
 |-  [,] : ( RR* X. RR* ) --> ~P RR*
7 ffun 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> Fun [,] )
8 funiunfv 
 |-  ( Fun [,] -> U_ n e. G ( [,] ` n ) = U. ( [,] " G ) )
9 6 7 8 mp2b 
 |-  U_ n e. G ( [,] ` n ) = U. ( [,] " G )
10 simpr 
 |-  ( ( ph /\ G e. Fin ) -> G e. Fin )
11 2 ssrab3 
 |-  G C_ A
12 11 3 sstrid 
 |-  ( ph -> G C_ ran F )
13 1 dyadf 
 |-  F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) )
14 frn 
 |-  ( F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> ran F C_ ( <_ i^i ( RR X. RR ) ) )
15 13 14 ax-mp 
 |-  ran F C_ ( <_ i^i ( RR X. RR ) )
16 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
17 15 16 sstri 
 |-  ran F C_ ( RR X. RR )
18 12 17 sstrdi 
 |-  ( ph -> G C_ ( RR X. RR ) )
19 18 adantr 
 |-  ( ( ph /\ G e. Fin ) -> G C_ ( RR X. RR ) )
20 19 sselda 
 |-  ( ( ( ph /\ G e. Fin ) /\ n e. G ) -> n e. ( RR X. RR ) )
21 1st2nd2 
 |-  ( n e. ( RR X. RR ) -> n = <. ( 1st ` n ) , ( 2nd ` n ) >. )
22 20 21 syl 
 |-  ( ( ( ph /\ G e. Fin ) /\ n e. G ) -> n = <. ( 1st ` n ) , ( 2nd ` n ) >. )
23 22 fveq2d 
 |-  ( ( ( ph /\ G e. Fin ) /\ n e. G ) -> ( [,] ` n ) = ( [,] ` <. ( 1st ` n ) , ( 2nd ` n ) >. ) )
24 df-ov 
 |-  ( ( 1st ` n ) [,] ( 2nd ` n ) ) = ( [,] ` <. ( 1st ` n ) , ( 2nd ` n ) >. )
25 23 24 eqtr4di 
 |-  ( ( ( ph /\ G e. Fin ) /\ n e. G ) -> ( [,] ` n ) = ( ( 1st ` n ) [,] ( 2nd ` n ) ) )
26 xp1st 
 |-  ( n e. ( RR X. RR ) -> ( 1st ` n ) e. RR )
27 20 26 syl 
 |-  ( ( ( ph /\ G e. Fin ) /\ n e. G ) -> ( 1st ` n ) e. RR )
28 xp2nd 
 |-  ( n e. ( RR X. RR ) -> ( 2nd ` n ) e. RR )
29 20 28 syl 
 |-  ( ( ( ph /\ G e. Fin ) /\ n e. G ) -> ( 2nd ` n ) e. RR )
30 iccmbl 
 |-  ( ( ( 1st ` n ) e. RR /\ ( 2nd ` n ) e. RR ) -> ( ( 1st ` n ) [,] ( 2nd ` n ) ) e. dom vol )
31 27 29 30 syl2anc 
 |-  ( ( ( ph /\ G e. Fin ) /\ n e. G ) -> ( ( 1st ` n ) [,] ( 2nd ` n ) ) e. dom vol )
32 25 31 eqeltrd 
 |-  ( ( ( ph /\ G e. Fin ) /\ n e. G ) -> ( [,] ` n ) e. dom vol )
33 32 ralrimiva 
 |-  ( ( ph /\ G e. Fin ) -> A. n e. G ( [,] ` n ) e. dom vol )
34 finiunmbl 
 |-  ( ( G e. Fin /\ A. n e. G ( [,] ` n ) e. dom vol ) -> U_ n e. G ( [,] ` n ) e. dom vol )
35 10 33 34 syl2anc 
 |-  ( ( ph /\ G e. Fin ) -> U_ n e. G ( [,] ` n ) e. dom vol )
36 9 35 eqeltrrid 
 |-  ( ( ph /\ G e. Fin ) -> U. ( [,] " G ) e. dom vol )
37 5 36 sylan2br 
 |-  ( ( ph /\ G ~< _om ) -> U. ( [,] " G ) e. dom vol )
38 rnco2 
 |-  ran ( [,] o. f ) = ( [,] " ran f )
39 f1ofo 
 |-  ( f : NN -1-1-onto-> G -> f : NN -onto-> G )
40 39 adantl 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> f : NN -onto-> G )
41 forn 
 |-  ( f : NN -onto-> G -> ran f = G )
42 40 41 syl 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> ran f = G )
43 42 imaeq2d 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> ( [,] " ran f ) = ( [,] " G ) )
44 38 43 eqtrid 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> ran ( [,] o. f ) = ( [,] " G ) )
45 44 unieqd 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> U. ran ( [,] o. f ) = U. ( [,] " G ) )
46 f1of 
 |-  ( f : NN -1-1-onto-> G -> f : NN --> G )
47 12 15 sstrdi 
 |-  ( ph -> G C_ ( <_ i^i ( RR X. RR ) ) )
48 fss 
 |-  ( ( f : NN --> G /\ G C_ ( <_ i^i ( RR X. RR ) ) ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
49 46 47 48 syl2anr 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
50 fss 
 |-  ( ( f : NN --> G /\ G C_ ran F ) -> f : NN --> ran F )
51 46 12 50 syl2anr 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> f : NN --> ran F )
52 simpl 
 |-  ( ( a e. NN /\ b e. NN ) -> a e. NN )
53 ffvelrn 
 |-  ( ( f : NN --> ran F /\ a e. NN ) -> ( f ` a ) e. ran F )
54 51 52 53 syl2an 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( f ` a ) e. ran F )
55 simpr 
 |-  ( ( a e. NN /\ b e. NN ) -> b e. NN )
56 ffvelrn 
 |-  ( ( f : NN --> ran F /\ b e. NN ) -> ( f ` b ) e. ran F )
57 51 55 56 syl2an 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( f ` b ) e. ran F )
58 1 dyaddisj 
 |-  ( ( ( f ` a ) e. ran F /\ ( f ` b ) e. ran F ) -> ( ( [,] ` ( f ` a ) ) C_ ( [,] ` ( f ` b ) ) \/ ( [,] ` ( f ` b ) ) C_ ( [,] ` ( f ` a ) ) \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) )
59 54 57 58 syl2anc 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( [,] ` ( f ` a ) ) C_ ( [,] ` ( f ` b ) ) \/ ( [,] ` ( f ` b ) ) C_ ( [,] ` ( f ` a ) ) \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) )
60 fveq2 
 |-  ( w = ( f ` b ) -> ( [,] ` w ) = ( [,] ` ( f ` b ) ) )
61 60 sseq2d 
 |-  ( w = ( f ` b ) -> ( ( [,] ` ( f ` a ) ) C_ ( [,] ` w ) <-> ( [,] ` ( f ` a ) ) C_ ( [,] ` ( f ` b ) ) ) )
62 eqeq2 
 |-  ( w = ( f ` b ) -> ( ( f ` a ) = w <-> ( f ` a ) = ( f ` b ) ) )
63 61 62 imbi12d 
 |-  ( w = ( f ` b ) -> ( ( ( [,] ` ( f ` a ) ) C_ ( [,] ` w ) -> ( f ` a ) = w ) <-> ( ( [,] ` ( f ` a ) ) C_ ( [,] ` ( f ` b ) ) -> ( f ` a ) = ( f ` b ) ) ) )
64 46 adantl 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> f : NN --> G )
65 ffvelrn 
 |-  ( ( f : NN --> G /\ a e. NN ) -> ( f ` a ) e. G )
66 64 52 65 syl2an 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( f ` a ) e. G )
67 fveq2 
 |-  ( z = ( f ` a ) -> ( [,] ` z ) = ( [,] ` ( f ` a ) ) )
68 67 sseq1d 
 |-  ( z = ( f ` a ) -> ( ( [,] ` z ) C_ ( [,] ` w ) <-> ( [,] ` ( f ` a ) ) C_ ( [,] ` w ) ) )
69 eqeq1 
 |-  ( z = ( f ` a ) -> ( z = w <-> ( f ` a ) = w ) )
70 68 69 imbi12d 
 |-  ( z = ( f ` a ) -> ( ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) <-> ( ( [,] ` ( f ` a ) ) C_ ( [,] ` w ) -> ( f ` a ) = w ) ) )
71 70 ralbidv 
 |-  ( z = ( f ` a ) -> ( A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) <-> A. w e. A ( ( [,] ` ( f ` a ) ) C_ ( [,] ` w ) -> ( f ` a ) = w ) ) )
72 71 2 elrab2 
 |-  ( ( f ` a ) e. G <-> ( ( f ` a ) e. A /\ A. w e. A ( ( [,] ` ( f ` a ) ) C_ ( [,] ` w ) -> ( f ` a ) = w ) ) )
73 72 simprbi 
 |-  ( ( f ` a ) e. G -> A. w e. A ( ( [,] ` ( f ` a ) ) C_ ( [,] ` w ) -> ( f ` a ) = w ) )
74 66 73 syl 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> A. w e. A ( ( [,] ` ( f ` a ) ) C_ ( [,] ` w ) -> ( f ` a ) = w ) )
75 ffvelrn 
 |-  ( ( f : NN --> G /\ b e. NN ) -> ( f ` b ) e. G )
76 64 55 75 syl2an 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( f ` b ) e. G )
77 11 76 sselid 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( f ` b ) e. A )
78 63 74 77 rspcdva 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( [,] ` ( f ` a ) ) C_ ( [,] ` ( f ` b ) ) -> ( f ` a ) = ( f ` b ) ) )
79 f1of1 
 |-  ( f : NN -1-1-onto-> G -> f : NN -1-1-> G )
80 79 adantl 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> f : NN -1-1-> G )
81 f1fveq 
 |-  ( ( f : NN -1-1-> G /\ ( a e. NN /\ b e. NN ) ) -> ( ( f ` a ) = ( f ` b ) <-> a = b ) )
82 80 81 sylan 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( f ` a ) = ( f ` b ) <-> a = b ) )
83 orc 
 |-  ( a = b -> ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) )
84 82 83 syl6bi 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( f ` a ) = ( f ` b ) -> ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) ) )
85 78 84 syld 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( [,] ` ( f ` a ) ) C_ ( [,] ` ( f ` b ) ) -> ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) ) )
86 fveq2 
 |-  ( w = ( f ` a ) -> ( [,] ` w ) = ( [,] ` ( f ` a ) ) )
87 86 sseq2d 
 |-  ( w = ( f ` a ) -> ( ( [,] ` ( f ` b ) ) C_ ( [,] ` w ) <-> ( [,] ` ( f ` b ) ) C_ ( [,] ` ( f ` a ) ) ) )
88 eqeq2 
 |-  ( w = ( f ` a ) -> ( ( f ` b ) = w <-> ( f ` b ) = ( f ` a ) ) )
89 eqcom 
 |-  ( ( f ` b ) = ( f ` a ) <-> ( f ` a ) = ( f ` b ) )
90 88 89 bitrdi 
 |-  ( w = ( f ` a ) -> ( ( f ` b ) = w <-> ( f ` a ) = ( f ` b ) ) )
91 87 90 imbi12d 
 |-  ( w = ( f ` a ) -> ( ( ( [,] ` ( f ` b ) ) C_ ( [,] ` w ) -> ( f ` b ) = w ) <-> ( ( [,] ` ( f ` b ) ) C_ ( [,] ` ( f ` a ) ) -> ( f ` a ) = ( f ` b ) ) ) )
92 fveq2 
 |-  ( z = ( f ` b ) -> ( [,] ` z ) = ( [,] ` ( f ` b ) ) )
93 92 sseq1d 
 |-  ( z = ( f ` b ) -> ( ( [,] ` z ) C_ ( [,] ` w ) <-> ( [,] ` ( f ` b ) ) C_ ( [,] ` w ) ) )
94 eqeq1 
 |-  ( z = ( f ` b ) -> ( z = w <-> ( f ` b ) = w ) )
95 93 94 imbi12d 
 |-  ( z = ( f ` b ) -> ( ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) <-> ( ( [,] ` ( f ` b ) ) C_ ( [,] ` w ) -> ( f ` b ) = w ) ) )
96 95 ralbidv 
 |-  ( z = ( f ` b ) -> ( A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) <-> A. w e. A ( ( [,] ` ( f ` b ) ) C_ ( [,] ` w ) -> ( f ` b ) = w ) ) )
97 96 2 elrab2 
 |-  ( ( f ` b ) e. G <-> ( ( f ` b ) e. A /\ A. w e. A ( ( [,] ` ( f ` b ) ) C_ ( [,] ` w ) -> ( f ` b ) = w ) ) )
98 97 simprbi 
 |-  ( ( f ` b ) e. G -> A. w e. A ( ( [,] ` ( f ` b ) ) C_ ( [,] ` w ) -> ( f ` b ) = w ) )
99 76 98 syl 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> A. w e. A ( ( [,] ` ( f ` b ) ) C_ ( [,] ` w ) -> ( f ` b ) = w ) )
100 11 66 sselid 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( f ` a ) e. A )
101 91 99 100 rspcdva 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( [,] ` ( f ` b ) ) C_ ( [,] ` ( f ` a ) ) -> ( f ` a ) = ( f ` b ) ) )
102 101 84 syld 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( [,] ` ( f ` b ) ) C_ ( [,] ` ( f ` a ) ) -> ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) ) )
103 olc 
 |-  ( ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) -> ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) )
104 103 a1i 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) -> ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) ) )
105 85 102 104 3jaod 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( ( [,] ` ( f ` a ) ) C_ ( [,] ` ( f ` b ) ) \/ ( [,] ` ( f ` b ) ) C_ ( [,] ` ( f ` a ) ) \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) -> ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) ) )
106 59 105 mpd 
 |-  ( ( ( ph /\ f : NN -1-1-onto-> G ) /\ ( a e. NN /\ b e. NN ) ) -> ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) )
107 106 ralrimivva 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> A. a e. NN A. b e. NN ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) )
108 2fveq3 
 |-  ( a = b -> ( (,) ` ( f ` a ) ) = ( (,) ` ( f ` b ) ) )
109 108 disjor 
 |-  ( Disj_ a e. NN ( (,) ` ( f ` a ) ) <-> A. a e. NN A. b e. NN ( a = b \/ ( ( (,) ` ( f ` a ) ) i^i ( (,) ` ( f ` b ) ) ) = (/) ) )
110 107 109 sylibr 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> Disj_ a e. NN ( (,) ` ( f ` a ) ) )
111 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
112 49 110 111 uniiccmbl 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> U. ran ( [,] o. f ) e. dom vol )
113 45 112 eqeltrrd 
 |-  ( ( ph /\ f : NN -1-1-onto-> G ) -> U. ( [,] " G ) e. dom vol )
114 113 ex 
 |-  ( ph -> ( f : NN -1-1-onto-> G -> U. ( [,] " G ) e. dom vol ) )
115 114 exlimdv 
 |-  ( ph -> ( E. f f : NN -1-1-onto-> G -> U. ( [,] " G ) e. dom vol ) )
116 nnenom 
 |-  NN ~~ _om
117 ensym 
 |-  ( G ~~ _om -> _om ~~ G )
118 entr 
 |-  ( ( NN ~~ _om /\ _om ~~ G ) -> NN ~~ G )
119 116 117 118 sylancr 
 |-  ( G ~~ _om -> NN ~~ G )
120 bren 
 |-  ( NN ~~ G <-> E. f f : NN -1-1-onto-> G )
121 119 120 sylib 
 |-  ( G ~~ _om -> E. f f : NN -1-1-onto-> G )
122 115 121 impel 
 |-  ( ( ph /\ G ~~ _om ) -> U. ( [,] " G ) e. dom vol )
123 reex 
 |-  RR e. _V
124 123 123 xpex 
 |-  ( RR X. RR ) e. _V
125 124 inex2 
 |-  ( <_ i^i ( RR X. RR ) ) e. _V
126 125 15 ssexi 
 |-  ran F e. _V
127 ssdomg 
 |-  ( ran F e. _V -> ( G C_ ran F -> G ~<_ ran F ) )
128 126 12 127 mpsyl 
 |-  ( ph -> G ~<_ ran F )
129 omelon 
 |-  _om e. On
130 znnen 
 |-  ZZ ~~ NN
131 130 116 entri 
 |-  ZZ ~~ _om
132 nn0ennn 
 |-  NN0 ~~ NN
133 132 116 entri 
 |-  NN0 ~~ _om
134 xpen 
 |-  ( ( ZZ ~~ _om /\ NN0 ~~ _om ) -> ( ZZ X. NN0 ) ~~ ( _om X. _om ) )
135 131 133 134 mp2an 
 |-  ( ZZ X. NN0 ) ~~ ( _om X. _om )
136 xpomen 
 |-  ( _om X. _om ) ~~ _om
137 135 136 entri 
 |-  ( ZZ X. NN0 ) ~~ _om
138 137 ensymi 
 |-  _om ~~ ( ZZ X. NN0 )
139 isnumi 
 |-  ( ( _om e. On /\ _om ~~ ( ZZ X. NN0 ) ) -> ( ZZ X. NN0 ) e. dom card )
140 129 138 139 mp2an 
 |-  ( ZZ X. NN0 ) e. dom card
141 ffn 
 |-  ( F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> F Fn ( ZZ X. NN0 ) )
142 13 141 ax-mp 
 |-  F Fn ( ZZ X. NN0 )
143 dffn4 
 |-  ( F Fn ( ZZ X. NN0 ) <-> F : ( ZZ X. NN0 ) -onto-> ran F )
144 142 143 mpbi 
 |-  F : ( ZZ X. NN0 ) -onto-> ran F
145 fodomnum 
 |-  ( ( ZZ X. NN0 ) e. dom card -> ( F : ( ZZ X. NN0 ) -onto-> ran F -> ran F ~<_ ( ZZ X. NN0 ) ) )
146 140 144 145 mp2 
 |-  ran F ~<_ ( ZZ X. NN0 )
147 domentr 
 |-  ( ( ran F ~<_ ( ZZ X. NN0 ) /\ ( ZZ X. NN0 ) ~~ _om ) -> ran F ~<_ _om )
148 146 137 147 mp2an 
 |-  ran F ~<_ _om
149 domtr 
 |-  ( ( G ~<_ ran F /\ ran F ~<_ _om ) -> G ~<_ _om )
150 128 148 149 sylancl 
 |-  ( ph -> G ~<_ _om )
151 brdom2 
 |-  ( G ~<_ _om <-> ( G ~< _om \/ G ~~ _om ) )
152 150 151 sylib 
 |-  ( ph -> ( G ~< _om \/ G ~~ _om ) )
153 37 122 152 mpjaodan 
 |-  ( ph -> U. ( [,] " G ) e. dom vol )
154 4 153 eqeltrd 
 |-  ( ph -> U. ( [,] " A ) e. dom vol )