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 ) )

Metamath Proof Explorer

Theorem uniiccdif

Proof