Metamath Proof Explorer

Theorem uniiccdif

Description: A union of closed intervals differs from the equivalent union of open intervals by a nullset. (Contributed by Mario Carneiro, 25-Mar-2015)

Ref Expression
Hypothesis uniioombl.1 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
Assertion uniiccdif 
|- ( ph -> ( U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) /\ ( vol* ` ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
2 ssun1 
 |-  U. ran ( (,) o. F ) C_ ( U. ran ( (,) o. F ) u. ( ( 1st " ran F ) u. ( 2nd " ran F ) ) )
3 ovolfcl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) )
4 1 3 sylan 
 |-  ( ( ph /\ x e. NN ) -> ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) )
5 rexr 
 |-  ( ( 1st ` ( F ` x ) ) e. RR -> ( 1st ` ( F ` x ) ) e. RR* )
6 rexr 
 |-  ( ( 2nd ` ( F ` x ) ) e. RR -> ( 2nd ` ( F ` x ) ) e. RR* )
7 id 
 |-  ( ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) -> ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) )
8 prunioo 
 |-  ( ( ( 1st ` ( F ` x ) ) e. RR* /\ ( 2nd ` ( F ` x ) ) e. RR* /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) -> ( ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) u. { ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) } ) = ( ( 1st ` ( F ` x ) ) [,] ( 2nd ` ( F ` x ) ) ) )
9 5 6 7 8 syl3an 
 |-  ( ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) -> ( ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) u. { ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) } ) = ( ( 1st ` ( F ` x ) ) [,] ( 2nd ` ( F ` x ) ) ) )
10 4 9 syl 
 |-  ( ( ph /\ x e. NN ) -> ( ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) u. { ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) } ) = ( ( 1st ` ( F ` x ) ) [,] ( 2nd ` ( F ` x ) ) ) )
11 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( (,) o. F ) ` x ) = ( (,) ` ( F ` x ) ) )
12 1 11 sylan 
 |-  ( ( ph /\ x e. NN ) -> ( ( (,) o. F ) ` x ) = ( (,) ` ( F ` x ) ) )
13 1 ffvelcdmda 
 |-  ( ( ph /\ x e. NN ) -> ( F ` x ) e. ( <_ i^i ( RR X. RR ) ) )
14 13 elin2d 
 |-  ( ( ph /\ x e. NN ) -> ( F ` x ) e. ( RR X. RR ) )
15 1st2nd2 
 |-  ( ( F ` x ) e. ( RR X. RR ) -> ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
16 14 15 syl 
 |-  ( ( ph /\ x e. NN ) -> ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
17 16 fveq2d 
 |-  ( ( ph /\ x e. NN ) -> ( (,) ` ( F ` x ) ) = ( (,) ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) )
18 df-ov 
 |-  ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) = ( (,) ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
19 17 18 eqtr4di 
 |-  ( ( ph /\ x e. NN ) -> ( (,) ` ( F ` x ) ) = ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) )
20 12 19 eqtrd 
 |-  ( ( ph /\ x e. NN ) -> ( ( (,) o. F ) ` x ) = ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) )
21 df-pr 
 |-  { ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) } = ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } )
22 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( 1st o. F ) ` x ) = ( 1st ` ( F ` x ) ) )
23 1 22 sylan 
 |-  ( ( ph /\ x e. NN ) -> ( ( 1st o. F ) ` x ) = ( 1st ` ( F ` x ) ) )
24 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( 2nd o. F ) ` x ) = ( 2nd ` ( F ` x ) ) )
25 1 24 sylan 
 |-  ( ( ph /\ x e. NN ) -> ( ( 2nd o. F ) ` x ) = ( 2nd ` ( F ` x ) ) )
26 23 25 preq12d 
 |-  ( ( ph /\ x e. NN ) -> { ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) } = { ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) } )
27 21 26 eqtr3id 
 |-  ( ( ph /\ x e. NN ) -> ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) = { ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) } )
28 20 27 uneq12d 
 |-  ( ( ph /\ x e. NN ) -> ( ( ( (,) o. F ) ` x ) u. ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) ) = ( ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) u. { ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) } ) )
29 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( [,] o. F ) ` x ) = ( [,] ` ( F ` x ) ) )
30 1 29 sylan 
 |-  ( ( ph /\ x e. NN ) -> ( ( [,] o. F ) ` x ) = ( [,] ` ( F ` x ) ) )
31 16 fveq2d 
 |-  ( ( ph /\ x e. NN ) -> ( [,] ` ( F ` x ) ) = ( [,] ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) )
32 df-ov 
 |-  ( ( 1st ` ( F ` x ) ) [,] ( 2nd ` ( F ` x ) ) ) = ( [,] ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
33 31 32 eqtr4di 
 |-  ( ( ph /\ x e. NN ) -> ( [,] ` ( F ` x ) ) = ( ( 1st ` ( F ` x ) ) [,] ( 2nd ` ( F ` x ) ) ) )
34 30 33 eqtrd 
 |-  ( ( ph /\ x e. NN ) -> ( ( [,] o. F ) ` x ) = ( ( 1st ` ( F ` x ) ) [,] ( 2nd ` ( F ` x ) ) ) )
35 10 28 34 3eqtr4rd 
 |-  ( ( ph /\ x e. NN ) -> ( ( [,] o. F ) ` x ) = ( ( ( (,) o. F ) ` x ) u. ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) ) )
36 35 iuneq2dv 
 |-  ( ph -> U_ x e. NN ( ( [,] o. F ) ` x ) = U_ x e. NN ( ( ( (,) o. F ) ` x ) u. ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) ) )
37 iccf 
 |-  [,] : ( RR* X. RR* ) --> ~P RR*
38 ffn 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> [,] Fn ( RR* X. RR* ) )
39 37 38 ax-mp 
 |-  [,] Fn ( RR* X. RR* )
40 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
41 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
42 40 41 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
43 fss 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) )
44 1 42 43 sylancl 
 |-  ( ph -> F : NN --> ( RR* X. RR* ) )
45 fnfco 
 |-  ( ( [,] Fn ( RR* X. RR* ) /\ F : NN --> ( RR* X. RR* ) ) -> ( [,] o. F ) Fn NN )
46 39 44 45 sylancr 
 |-  ( ph -> ( [,] o. F ) Fn NN )
47 fniunfv 
 |-  ( ( [,] o. F ) Fn NN -> U_ x e. NN ( ( [,] o. F ) ` x ) = U. ran ( [,] o. F ) )
48 46 47 syl 
 |-  ( ph -> U_ x e. NN ( ( [,] o. F ) ` x ) = U. ran ( [,] o. F ) )
49 iunun 
 |-  U_ x e. NN ( ( ( (,) o. F ) ` x ) u. ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) ) = ( U_ x e. NN ( ( (,) o. F ) ` x ) u. U_ x e. NN ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) )
50 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
51 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
52 50 51 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
53 fnfco 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) Fn NN )
54 52 44 53 sylancr 
 |-  ( ph -> ( (,) o. F ) Fn NN )
55 fniunfv 
 |-  ( ( (,) o. F ) Fn NN -> U_ x e. NN ( ( (,) o. F ) ` x ) = U. ran ( (,) o. F ) )
56 54 55 syl 
 |-  ( ph -> U_ x e. NN ( ( (,) o. F ) ` x ) = U. ran ( (,) o. F ) )
57 iunun 
 |-  U_ x e. NN ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) = ( U_ x e. NN { ( ( 1st o. F ) ` x ) } u. U_ x e. NN { ( ( 2nd o. F ) ` x ) } )
58 fo1st 
 |-  1st : _V -onto-> _V
59 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
60 58 59 ax-mp 
 |-  1st Fn _V
61 ssv 
 |-  ( <_ i^i ( RR X. RR ) ) C_ _V
62 fss 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ _V ) -> F : NN --> _V )
63 1 61 62 sylancl 
 |-  ( ph -> F : NN --> _V )
64 fnfco 
 |-  ( ( 1st Fn _V /\ F : NN --> _V ) -> ( 1st o. F ) Fn NN )
65 60 63 64 sylancr 
 |-  ( ph -> ( 1st o. F ) Fn NN )
66 fnfun 
 |-  ( ( 1st o. F ) Fn NN -> Fun ( 1st o. F ) )
67 65 66 syl 
 |-  ( ph -> Fun ( 1st o. F ) )
68 fndm 
 |-  ( ( 1st o. F ) Fn NN -> dom ( 1st o. F ) = NN )
69 eqimss2 
 |-  ( dom ( 1st o. F ) = NN -> NN C_ dom ( 1st o. F ) )
70 65 68 69 3syl 
 |-  ( ph -> NN C_ dom ( 1st o. F ) )
71 dfimafn2 
 |-  ( ( Fun ( 1st o. F ) /\ NN C_ dom ( 1st o. F ) ) -> ( ( 1st o. F ) " NN ) = U_ x e. NN { ( ( 1st o. F ) ` x ) } )
72 67 70 71 syl2anc 
 |-  ( ph -> ( ( 1st o. F ) " NN ) = U_ x e. NN { ( ( 1st o. F ) ` x ) } )
73 fnima 
 |-  ( ( 1st o. F ) Fn NN -> ( ( 1st o. F ) " NN ) = ran ( 1st o. F ) )
74 65 73 syl 
 |-  ( ph -> ( ( 1st o. F ) " NN ) = ran ( 1st o. F ) )
75 72 74 eqtr3d 
 |-  ( ph -> U_ x e. NN { ( ( 1st o. F ) ` x ) } = ran ( 1st o. F ) )
76 rnco2 
 |-  ran ( 1st o. F ) = ( 1st " ran F )
77 75 76 eqtrdi 
 |-  ( ph -> U_ x e. NN { ( ( 1st o. F ) ` x ) } = ( 1st " ran F ) )
78 fo2nd 
 |-  2nd : _V -onto-> _V
79 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
80 78 79 ax-mp 
 |-  2nd Fn _V
81 fnfco 
 |-  ( ( 2nd Fn _V /\ F : NN --> _V ) -> ( 2nd o. F ) Fn NN )
82 80 63 81 sylancr 
 |-  ( ph -> ( 2nd o. F ) Fn NN )
83 fnfun 
 |-  ( ( 2nd o. F ) Fn NN -> Fun ( 2nd o. F ) )
84 82 83 syl 
 |-  ( ph -> Fun ( 2nd o. F ) )
85 fndm 
 |-  ( ( 2nd o. F ) Fn NN -> dom ( 2nd o. F ) = NN )
86 eqimss2 
 |-  ( dom ( 2nd o. F ) = NN -> NN C_ dom ( 2nd o. F ) )
87 82 85 86 3syl 
 |-  ( ph -> NN C_ dom ( 2nd o. F ) )
88 dfimafn2 
 |-  ( ( Fun ( 2nd o. F ) /\ NN C_ dom ( 2nd o. F ) ) -> ( ( 2nd o. F ) " NN ) = U_ x e. NN { ( ( 2nd o. F ) ` x ) } )
89 84 87 88 syl2anc 
 |-  ( ph -> ( ( 2nd o. F ) " NN ) = U_ x e. NN { ( ( 2nd o. F ) ` x ) } )
90 fnima 
 |-  ( ( 2nd o. F ) Fn NN -> ( ( 2nd o. F ) " NN ) = ran ( 2nd o. F ) )
91 82 90 syl 
 |-  ( ph -> ( ( 2nd o. F ) " NN ) = ran ( 2nd o. F ) )
92 89 91 eqtr3d 
 |-  ( ph -> U_ x e. NN { ( ( 2nd o. F ) ` x ) } = ran ( 2nd o. F ) )
93 rnco2 
 |-  ran ( 2nd o. F ) = ( 2nd " ran F )
94 92 93 eqtrdi 
 |-  ( ph -> U_ x e. NN { ( ( 2nd o. F ) ` x ) } = ( 2nd " ran F ) )
95 77 94 uneq12d 
 |-  ( ph -> ( U_ x e. NN { ( ( 1st o. F ) ` x ) } u. U_ x e. NN { ( ( 2nd o. F ) ` x ) } ) = ( ( 1st " ran F ) u. ( 2nd " ran F ) ) )
96 57 95 eqtrid 
 |-  ( ph -> U_ x e. NN ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) = ( ( 1st " ran F ) u. ( 2nd " ran F ) ) )
97 56 96 uneq12d 
 |-  ( ph -> ( U_ x e. NN ( ( (,) o. F ) ` x ) u. U_ x e. NN ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) ) = ( U. ran ( (,) o. F ) u. ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ) )
98 49 97 eqtrid 
 |-  ( ph -> U_ x e. NN ( ( ( (,) o. F ) ` x ) u. ( { ( ( 1st o. F ) ` x ) } u. { ( ( 2nd o. F ) ` x ) } ) ) = ( U. ran ( (,) o. F ) u. ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ) )
99 36 48 98 3eqtr3d 
 |-  ( ph -> U. ran ( [,] o. F ) = ( U. ran ( (,) o. F ) u. ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ) )
100 2 99 sseqtrrid 
 |-  ( ph -> U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) )
101 ovolficcss 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. F ) C_ RR )
102 1 101 syl 
 |-  ( ph -> U. ran ( [,] o. F ) C_ RR )
103 102 ssdifssd 
 |-  ( ph -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) C_ RR )
104 omelon 
 |-  _om e. On
105 nnenom 
 |-  NN ~~ _om
106 105 ensymi 
 |-  _om ~~ NN
107 isnumi 
 |-  ( ( _om e. On /\ _om ~~ NN ) -> NN e. dom card )
108 104 106 107 mp2an 
 |-  NN e. dom card
109 fofun 
 |-  ( 1st : _V -onto-> _V -> Fun 1st )
110 58 109 ax-mp 
 |-  Fun 1st
111 ssv 
 |-  ran F C_ _V
112 fof 
 |-  ( 1st : _V -onto-> _V -> 1st : _V --> _V )
113 58 112 ax-mp 
 |-  1st : _V --> _V
114 113 fdmi 
 |-  dom 1st = _V
115 111 114 sseqtrri 
 |-  ran F C_ dom 1st
116 fores 
 |-  ( ( Fun 1st /\ ran F C_ dom 1st ) -> ( 1st |` ran F ) : ran F -onto-> ( 1st " ran F ) )
117 110 115 116 mp2an 
 |-  ( 1st |` ran F ) : ran F -onto-> ( 1st " ran F )
118 1 ffnd 
 |-  ( ph -> F Fn NN )
119 dffn4 
 |-  ( F Fn NN <-> F : NN -onto-> ran F )
120 118 119 sylib 
 |-  ( ph -> F : NN -onto-> ran F )
121 foco 
 |-  ( ( ( 1st |` ran F ) : ran F -onto-> ( 1st " ran F ) /\ F : NN -onto-> ran F ) -> ( ( 1st |` ran F ) o. F ) : NN -onto-> ( 1st " ran F ) )
122 117 120 121 sylancr 
 |-  ( ph -> ( ( 1st |` ran F ) o. F ) : NN -onto-> ( 1st " ran F ) )
123 fodomnum 
 |-  ( NN e. dom card -> ( ( ( 1st |` ran F ) o. F ) : NN -onto-> ( 1st " ran F ) -> ( 1st " ran F ) ~<_ NN ) )
124 108 122 123 mpsyl 
 |-  ( ph -> ( 1st " ran F ) ~<_ NN )
125 domentr 
 |-  ( ( ( 1st " ran F ) ~<_ NN /\ NN ~~ _om ) -> ( 1st " ran F ) ~<_ _om )
126 124 105 125 sylancl 
 |-  ( ph -> ( 1st " ran F ) ~<_ _om )
127 fofun 
 |-  ( 2nd : _V -onto-> _V -> Fun 2nd )
128 78 127 ax-mp 
 |-  Fun 2nd
129 fof 
 |-  ( 2nd : _V -onto-> _V -> 2nd : _V --> _V )
130 78 129 ax-mp 
 |-  2nd : _V --> _V
131 130 fdmi 
 |-  dom 2nd = _V
132 111 131 sseqtrri 
 |-  ran F C_ dom 2nd
133 fores 
 |-  ( ( Fun 2nd /\ ran F C_ dom 2nd ) -> ( 2nd |` ran F ) : ran F -onto-> ( 2nd " ran F ) )
134 128 132 133 mp2an 
 |-  ( 2nd |` ran F ) : ran F -onto-> ( 2nd " ran F )
135 foco 
 |-  ( ( ( 2nd |` ran F ) : ran F -onto-> ( 2nd " ran F ) /\ F : NN -onto-> ran F ) -> ( ( 2nd |` ran F ) o. F ) : NN -onto-> ( 2nd " ran F ) )
136 134 120 135 sylancr 
 |-  ( ph -> ( ( 2nd |` ran F ) o. F ) : NN -onto-> ( 2nd " ran F ) )
137 fodomnum 
 |-  ( NN e. dom card -> ( ( ( 2nd |` ran F ) o. F ) : NN -onto-> ( 2nd " ran F ) -> ( 2nd " ran F ) ~<_ NN ) )
138 108 136 137 mpsyl 
 |-  ( ph -> ( 2nd " ran F ) ~<_ NN )
139 domentr 
 |-  ( ( ( 2nd " ran F ) ~<_ NN /\ NN ~~ _om ) -> ( 2nd " ran F ) ~<_ _om )
140 138 105 139 sylancl 
 |-  ( ph -> ( 2nd " ran F ) ~<_ _om )
141 unctb 
 |-  ( ( ( 1st " ran F ) ~<_ _om /\ ( 2nd " ran F ) ~<_ _om ) -> ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ~<_ _om )
142 126 140 141 syl2anc 
 |-  ( ph -> ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ~<_ _om )
143 ctex 
 |-  ( ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ~<_ _om -> ( ( 1st " ran F ) u. ( 2nd " ran F ) ) e. _V )
144 142 143 syl 
 |-  ( ph -> ( ( 1st " ran F ) u. ( 2nd " ran F ) ) e. _V )
145 ssid 
 |-  U. ran ( [,] o. F ) C_ U. ran ( [,] o. F )
146 145 99 sseqtrid 
 |-  ( ph -> U. ran ( [,] o. F ) C_ ( U. ran ( (,) o. F ) u. ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ) )
147 ssundif 
 |-  ( U. ran ( [,] o. F ) C_ ( U. ran ( (,) o. F ) u. ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ) <-> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) C_ ( ( 1st " ran F ) u. ( 2nd " ran F ) ) )
148 146 147 sylib 
 |-  ( ph -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) C_ ( ( 1st " ran F ) u. ( 2nd " ran F ) ) )
149 ssdomg 
 |-  ( ( ( 1st " ran F ) u. ( 2nd " ran F ) ) e. _V -> ( ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) C_ ( ( 1st " ran F ) u. ( 2nd " ran F ) ) -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ~<_ ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ) )
150 144 148 149 sylc 
 |-  ( ph -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ~<_ ( ( 1st " ran F ) u. ( 2nd " ran F ) ) )
151 domtr 
 |-  ( ( ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ~<_ ( ( 1st " ran F ) u. ( 2nd " ran F ) ) /\ ( ( 1st " ran F ) u. ( 2nd " ran F ) ) ~<_ _om ) -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ~<_ _om )
152 150 142 151 syl2anc 
 |-  ( ph -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ~<_ _om )
153 domentr 
 |-  ( ( ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ~<_ _om /\ _om ~~ NN ) -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ~<_ NN )
154 152 106 153 sylancl 
 |-  ( ph -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ~<_ NN )
155 ovolctb2 
 |-  ( ( ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) C_ RR /\ ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ~<_ NN ) -> ( vol* ` ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = 0 )
156 103 154 155 syl2anc 
 |-  ( ph -> ( vol* ` ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = 0 )
157 100 156 jca 
 |-  ( ph -> ( U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) /\ ( vol* ` ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = 0 ) )