uniioombllem2 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > uniioombllem2		Unicode version

Theorem uniioombllem2 19428

Description: Lemma for uniioombl 19434. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 11-Dec-2016.)

**Hypotheses**
Ref	Expression
uniioombl.1
uniioombl.2	Disj
uniioombl.3
uniioombl.a
uniioombl.e
uniioombl.c
uniioombl.g
uniioombl.s
uniioombl.t
uniioombl.v
uniioombllem2.h
uniioombllem2.k

**Assertion**
Ref	Expression
uniioombllem2	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem uniioombllem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 10477	. . 3
2		eqid 2404	. . 3
3		1z 10267	. . . 4
4	3	a1i 11	. . 3 $/\$
5		eqidd 2405	. . 3 $/\$ $/\$
6		uniioombl.1	. . . . . . . . . . 11
7		uniioombl.2	. . . . . . . . . . 11 Disj
8		uniioombl.3	. . . . . . . . . . 11
9		uniioombl.a	. . . . . . . . . . 11
10		uniioombl.e	. . . . . . . . . . 11
11		uniioombl.c	. . . . . . . . . . 11
12		uniioombl.g	. . . . . . . . . . 11
13		uniioombl.s	. . . . . . . . . . 11
14		uniioombl.t	. . . . . . . . . . 11
15		uniioombl.v	. . . . . . . . . . 11
16	6, 7, 8, 9, 10, 11, 12, 13, 14, 15	uniioombllem2a 19427	. . . . . . . . . 10 $/\$ $/\$
17		inss2 3522	. . . . . . . . . . . . 13
18	17	a1i 11	. . . . . . . . . . . 12 $/\$
19		inss2 3522	. . . . . . . . . . . . . . . . 17
20	12	ffvelrnda 5829	. . . . . . . . . . . . . . . . 17 $/\$
21	19, 20	sseldi 3306	. . . . . . . . . . . . . . . 16 $/\$
22		1st2nd2 6345	. . . . . . . . . . . . . . . 16
23	21, 22	syl 16	. . . . . . . . . . . . . . 15 $/\$
24	23	fveq2d 5691	. . . . . . . . . . . . . 14 $/\$
25		df-ov 6043	. . . . . . . . . . . . . 14
26	24, 25	syl6eqr 2454	. . . . . . . . . . . . 13 $/\$
27		ioossre 10928	. . . . . . . . . . . . 13
28	26, 27	syl6eqss 3358	. . . . . . . . . . . 12 $/\$
29	26	fveq2d 5691	. . . . . . . . . . . . . 14 $/\$
30		ovolfcl 19316	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
31	12, 30	sylan 458	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
32		ovolioo 19415	. . . . . . . . . . . . . . 15 $/\$ $/\$
33	31, 32	syl 16	. . . . . . . . . . . . . 14 $/\$
34	29, 33	eqtrd 2436	. . . . . . . . . . . . 13 $/\$
35	31	simp2d 970	. . . . . . . . . . . . . 14 $/\$
36	31	simp1d 969	. . . . . . . . . . . . . 14 $/\$
37	35, 36	resubcld 9421	. . . . . . . . . . . . 13 $/\$
38	34, 37	eqeltrd 2478	. . . . . . . . . . . 12 $/\$
39		ovolsscl 19335	. . . . . . . . . . . 12 $/\$ $/\$
40	18, 28, 38, 39	syl3anc 1184	. . . . . . . . . . 11 $/\$
41	40	adantr 452	. . . . . . . . . 10 $/\$ $/\$
42		uniioombllem2.k	. . . . . . . . . . 11
43	42	ioorcl 19422	. . . . . . . . . 10 $/\$
44	16, 41, 43	syl2anc 643	. . . . . . . . 9 $/\$ $/\$
45		eqid 2404	. . . . . . . . 9
46	44, 45	fmptd 5852	. . . . . . . 8 $/\$
47		uniioombllem2.h	. . . . . . . . . . 11
48	47	a1i 11	. . . . . . . . . 10 $/\$
49	42	ioorf 19418	. . . . . . . . . . . 12
50	49	a1i 11	. . . . . . . . . . 11 $/\$
51	50	feqmptd 5738	. . . . . . . . . 10 $/\$
52		fveq2 5687	. . . . . . . . . 10
53	16, 48, 51, 52	fmptco 5860	. . . . . . . . 9 $/\$
54	53	feq1d 5539	. . . . . . . 8 $/\$
55	46, 54	mpbird 224	. . . . . . 7 $/\$
56		eqid 2404	. . . . . . . 8
57	56	ovolfsf 19321	. . . . . . 7
58	55, 57	syl 16	. . . . . 6 $/\$
59	58	ffvelrnda 5829	. . . . 5 $/\$ $/\$
60		elrege0 10963	. . . . 5 $/\$
61	59, 60	sylib 189	. . . 4 $/\$ $/\$ $/\$
62	61	simpld 446	. . 3 $/\$ $/\$
63	61	simprd 450	. . 3 $/\$ $/\$
64	53	fveq1d 5689	. . . . . . . . . . . . . . 15 $/\$
65		fvex 5701	. . . . . . . . . . . . . . . 16
66	45	fvmpt2 5771	. . . . . . . . . . . . . . . 16 $/\$
67	65, 66	mpan2 653	. . . . . . . . . . . . . . 15
68	64, 67	sylan9eq 2456	. . . . . . . . . . . . . 14 $/\$ $/\$
69	68	fveq2d 5691	. . . . . . . . . . . . 13 $/\$ $/\$
70	42	ioorinv 19421	. . . . . . . . . . . . . 14
71	16, 70	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
72	69, 71	eqtrd 2436	. . . . . . . . . . . 12 $/\$ $/\$
73	72	ralrimiva 2749	. . . . . . . . . . 11 $/\$
74		fveq2 5687	. . . . . . . . . . . . . 14
75	74	fveq2d 5691	. . . . . . . . . . . . 13
76		fveq2 5687	. . . . . . . . . . . . . . 15
77	76	fveq2d 5691	. . . . . . . . . . . . . 14
78	77	ineq1d 3501	. . . . . . . . . . . . 13
79	75, 78	eqeq12d 2418	. . . . . . . . . . . 12
80	79	rspccva 3011	. . . . . . . . . . 11 $/\$
81	73, 80	sylan 458	. . . . . . . . . 10 $/\$ $/\$
82		inss1 3521	. . . . . . . . . 10
83	81, 82	syl6eqss 3358	. . . . . . . . 9 $/\$ $/\$
84	83	ralrimiva 2749	. . . . . . . 8 $/\$
85	7	adantr 452	. . . . . . . 8 $/\$ Disj
86		disjss2 4145	. . . . . . . 8 Disj Disj
87	84, 85, 86	sylc 58	. . . . . . 7 $/\$ Disj
88	55, 87, 2	uniioovol 19424	. . . . . 6 $/\$
89	71	mpteq2dva 4255	. . . . . . . . . . 11 $/\$
90		ressxr 9085	. . . . . . . . . . . . . . 15
91		xpss12 4940	. . . . . . . . . . . . . . 15 $/\$
92	90, 90, 91	mp2an 654	. . . . . . . . . . . . . 14
93	19, 92	sstri 3317	. . . . . . . . . . . . 13
94	93, 44	sseldi 3306	. . . . . . . . . . . 12 $/\$ $/\$
95		ioof 10958	. . . . . . . . . . . . . 14
96	95	a1i 11	. . . . . . . . . . . . 13 $/\$
97	96	feqmptd 5738	. . . . . . . . . . . 12 $/\$
98		fveq2 5687	. . . . . . . . . . . 12
99	94, 53, 97, 98	fmptco 5860	. . . . . . . . . . 11 $/\$
100	89, 99, 48	3eqtr4d 2446	. . . . . . . . . 10 $/\$
101	100	rneqd 5056	. . . . . . . . 9 $/\$
102	101	unieqd 3986	. . . . . . . 8 $/\$
103		fvex 5701	. . . . . . . . . . . . . 14
104	103	inex1 4304	. . . . . . . . . . . . 13
105	47	fvmpt2 5771	. . . . . . . . . . . . 13 $/\$
106	104, 105	mpan2 653	. . . . . . . . . . . 12
107		incom 3493	. . . . . . . . . . . 12
108	106, 107	syl6eq 2452	. . . . . . . . . . 11
109	108	iuneq2i 4071	. . . . . . . . . 10
110		iunin2 4115	. . . . . . . . . 10
111	109, 110	eqtri 2424	. . . . . . . . 9
112	16, 47	fmptd 5852	. . . . . . . . . . 11 $/\$
113		ffn 5550	. . . . . . . . . . 11
114	112, 113	syl 16	. . . . . . . . . 10 $/\$
115		fniunfv 5953	. . . . . . . . . 10
116	114, 115	syl 16	. . . . . . . . 9 $/\$
117	111, 116	syl5eqr 2450	. . . . . . . 8 $/\$
118	6	adantr 452	. . . . . . . . . . . 12 $/\$
119		fvco3 5759	. . . . . . . . . . . 12 $/\$
120	118, 119	sylan 458	. . . . . . . . . . 11 $/\$ $/\$
121	120	iuneq2dv 4074	. . . . . . . . . 10 $/\$
122		ffn 5550	. . . . . . . . . . . . . 14
123	95, 122	ax-mp 8	. . . . . . . . . . . . 13
124		fss 5558	. . . . . . . . . . . . . 14 $/\$
125	118, 93, 124	sylancl 644	. . . . . . . . . . . . 13 $/\$
126		fnfco 5568	. . . . . . . . . . . . 13 $/\$
127	123, 125, 126	sylancr 645	. . . . . . . . . . . 12 $/\$
128		fniunfv 5953	. . . . . . . . . . . 12
129	127, 128	syl 16	. . . . . . . . . . 11 $/\$
130	129, 9	syl6eqr 2454	. . . . . . . . . 10 $/\$
131	121, 130	eqtr3d 2438	. . . . . . . . 9 $/\$
132	131	ineq2d 3502	. . . . . . . 8 $/\$
133	102, 117, 132	3eqtr2d 2442	. . . . . . 7 $/\$
134	133	fveq2d 5691	. . . . . 6 $/\$
135	88, 134	eqtr3d 2438	. . . . 5 $/\$
136		inss1 3521	. . . . . . 7
137	136	a1i 11	. . . . . 6 $/\$
138		ovolsscl 19335	. . . . . 6 $/\$ $/\$
139	137, 28, 38, 138	syl3anc 1184	. . . . 5 $/\$
140	135, 139	eqeltrd 2478	. . . 4 $/\$
141	56, 2	ovolsf 19322	. . . . . . . . 9
142	55, 141	syl 16	. . . . . . . 8 $/\$
143		ffn 5550	. . . . . . . 8
144	142, 143	syl 16	. . . . . . 7 $/\$
145		fnfvelrn 5826	. . . . . . 7 $/\$
146	144, 145	sylan 458	. . . . . 6 $/\$ $/\$
147		frn 5556	. . . . . . . . 9
148	142, 147	syl 16	. . . . . . . 8 $/\$
149		icossxr 10951	. . . . . . . 8
150	148, 149	syl6ss 3320	. . . . . . 7 $/\$
151		supxrub 10859	. . . . . . 7 $/\$
152	150, 151	sylan 458	. . . . . 6 $/\$ $/\$
153	146, 152	syldan 457	. . . . 5 $/\$ $/\$
154	153	ralrimiva 2749	. . . 4 $/\$
155		breq2 4176	. . . . . 6
156	155	ralbidv 2686	. . . . 5
157	156	rspcev 3012	. . . 4 $/\$
158	140, 154, 157	syl2anc 643	. . 3 $/\$
159	1, 2, 4, 5, 62, 63, 158	isumsup2 12581	. 2 $/\$
160	56	ovolfs2 19416	. . . . 5
161	55, 160	syl 16	. . . 4 $/\$
162		coass 5347	. . . . 5
163	100	coeq2d 4994	. . . . 5 $/\$
164	162, 163	syl5eq 2448	. . . 4 $/\$
165	161, 164	eqtrd 2436	. . 3 $/\$
166	165	seqeq3d 11286	. 2 $/\$
167		0re 9047	. . . . . 6
168		pnfxr 10669	. . . . . 6
169		icossre 10947	. . . . . 6 $/\$
170	167, 168, 169	mp2an 654	. . . . 5
171	148, 170	syl6ss 3320	. . . 4 $/\$
172		1nn 9967	. . . . . . 7
173		fdm 5554	. . . . . . . 8
174	142, 173	syl 16	. . . . . . 7 $/\$
175	172, 174	syl5eleqr 2491	. . . . . 6 $/\$
176		ne0i 3594	. . . . . 6
177	175, 176	syl 16	. . . . 5 $/\$
178		dm0rn0 5045	. . . . . 6
179	178	necon3bii 2599	. . . . 5
180	177, 179	sylib 189	. . . 4 $/\$
181		breq1 4175	. . . . . . . 8
182	181	ralrn 5832	. . . . . . 7
183	144, 182	syl 16	. . . . . 6 $/\$
184	183	rexbidv 2687	. . . . 5 $/\$
185	158, 184	mpbird 224	. . . 4 $/\$
186		supxrre 10862	. . . 4 $/\$ $/\$
187	171, 180, 185, 186	syl3anc 1184	. . 3 $/\$
188	187, 135	eqtr3d 2438	. 2 $/\$
189	159, 166, 188	3brtr3d 4201	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667

cvv 2916

cin 3279

wss 3280

c0 3588

cif 3699

cpw 3759

cop 3777

cuni 3975

ciun 4053 Disj wdisj 4142 class class class wbr 4172

cmpt 4226

cxp 4835

ccnv 4836

cdm 4837

crn 4838

ccom 4841

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

c1st 6306

c2nd 6307

csup 7403

cr 8945

cc0 8946

c1 8947

caddc 8949

cpnf 9073

cxr 9075

clt 9076

cle 9077

cmin 9247

cn 9956

cz 10238

crp 10568

cioo 10872

cico 10874

cseq 11278

cabs 11994

cli 12233

covol 19312

This theorem is referenced by: uniioombllem6 19433

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-disj 4143 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-rlim 12238 df-sum 12435 df-rest 13605 df-topgen 13622 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-top 16918 df-bases 16920 df-topon 16921 df-cmp 17404 df-ovol 19314 df-vol 19315

W3C validator