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

Theorem uniioombllem4 21466
Description: Lemma for uniioombl 21469. (Contributed by Mario Carneiro, 26-Mar-2015.)
Hypotheses
Ref Expression
uniioombl.1
uniioombl.2
uniioombl.3
uniioombl.a
uniioombl.e
uniioombl.c
uniioombl.g
uniioombl.s
uniioombl.t
uniioombl.v
uniioombl.m
uniioombl.m2
uniioombl.k
uniioombl.n
uniioombl.n2
uniioombl.l
Assertion
Ref Expression
uniioombllem4
Distinct variable groups:   , , ,   , , ,   , ,   , ,   , , ,   ,M, ,   ,N,   , , ,   , , ,

Proof of Theorem uniioombllem4
StepHypRef Expression
1 inss1 3684 . . . 4
21a1i 11 . . 3
3 uniioombl.k . . . . . 6
4 imassrn 5299 . . . . . . 7
54unissi 4231 . . . . . 6
63, 5eqsstri 3500 . . . . 5
76a1i 11 . . . 4
8 uniioombl.g . . . . . . 7
98uniiccdif 21458 . . . . . 6
109simpld 459 . . . . 5
11 ovolficcss 21352 . . . . . 6
128, 11syl 16 . . . . 5
1310, 12sstrd 3480 . . . 4
147, 13sstrd 3480 . . 3
15 uniioombl.1 . . . . . 6
16 uniioombl.2 . . . . . 6
17 uniioombl.3 . . . . . 6
18 uniioombl.a . . . . . 6
19 uniioombl.e . . . . . 6
20 uniioombl.c . . . . . 6
21 uniioombl.s . . . . . 6
22 uniioombl.t . . . . . 6
23 uniioombl.v . . . . . 6
2415, 16, 17, 18, 19, 20, 8, 21, 22, 23uniioombllem1 21461 . . . . 5
25 ssid 3489 . . . . . 6
2622ovollb 21361 . . . . . 6
278, 25, 26sylancl 662 . . . . 5
28 ovollecl 21365 . . . . 5
2913, 24, 27, 28syl3anc 1219 . . . 4
30 ovolsscl 21368 . . . 4
317, 13, 29, 30syl3anc 1219 . . 3
32 ovolsscl 21368 . . 3
332, 14, 31, 32syl3anc 1219 . 2
34 inss1 3684 . . . . 5
3534a1i 11 . . . 4
36 ovolsscl 21368 . . . 4
3735, 14, 31, 36syl3anc 1219 . . 3
38 ssun2 3634 . . . . . 6
39 nnuz 11035 . . . . . . . . . . . . . 14
40 uniioombl.n . . . . . . . . . . . . . . . . 17
4140peano2nnd 10477 . . . . . . . . . . . . . . . 16
4241, 39syl6eleq 2552 . . . . . . . . . . . . . . 15
43 uzsplit 11675 . . . . . . . . . . . . . . 15
4442, 43syl 16 . . . . . . . . . . . . . 14
4539, 44syl5eq 2507 . . . . . . . . . . . . 13
4640nncnd 10476 . . . . . . . . . . . . . . . 16
47 ax-1cn 9477 . . . . . . . . . . . . . . . 16
48 pncan 9753 . . . . . . . . . . . . . . . 16
4946, 47, 48sylancl 662 . . . . . . . . . . . . . . 15
5049oveq2d 6238 . . . . . . . . . . . . . 14
5150uneq1d 3623 . . . . . . . . . . . . 13
5245, 51eqtrd 2495 . . . . . . . . . . . 12
5352iuneq1d 4312 . . . . . . . . . . 11
54 iunxun 4369 . . . . . . . . . . 11
5553, 54syl6eq 2511 . . . . . . . . . 10
56 ioof 11532 . . . . . . . . . . . . . 14
57 inss2 3685 . . . . . . . . . . . . . . . 16
58 rexpssxrxp 9565 . . . . . . . . . . . . . . . 16
5957, 58sstri 3479 . . . . . . . . . . . . . . 15
60 fss 5687 . . . . . . . . . . . . . . 15
6115, 59, 60sylancl 662 . . . . . . . . . . . . . 14
62 fco 5689 . . . . . . . . . . . . . 14
6356, 61, 62sylancr 663 . . . . . . . . . . . . 13
64 ffn 5679 . . . . . . . . . . . . 13
65 fniunfv 6089 . . . . . . . . . . . . 13
6663, 64, 653syl 20 . . . . . . . . . . . 12
67 fvco3 5891 . . . . . . . . . . . . . 14
6815, 67sylan 471 . . . . . . . . . . . . 13
6968iuneq2dv 4309 . . . . . . . . . . . 12
7066, 69eqtr3d 2497 . . . . . . . . . . 11
7118, 70syl5eq 2507 . . . . . . . . . 10
72 uniioombl.l . . . . . . . . . . . 12
73 ffun 5681 . . . . . . . . . . . . . 14
74 funiunfv 6090 . . . . . . . . . . . . . 14
7563, 73, 743syl 20 . . . . . . . . . . . . 13
76 elfznn 11623 . . . . . . . . . . . . . . 15
7715, 76, 67syl2an 477 . . . . . . . . . . . . . 14
7877iuneq2dv 4309 . . . . . . . . . . . . 13
7975, 78eqtr3d 2497 . . . . . . . . . . . 12
8072, 79syl5eq 2507 . . . . . . . . . . 11
8180uneq1d 3623 . . . . . . . . . 10
8255, 71, 813eqtr4d 2505 . . . . . . . . 9
8382ineq2d 3666 . . . . . . . 8
84 indi 3710 . . . . . . . 8
8583, 84syl6eq 2511 . . . . . . 7
86 fss 5687 . . . . . . . . . . . . . . 15
878, 59, 86sylancl 662 . . . . . . . . . . . . . 14
88 fco 5689 . . . . . . . . . . . . . 14
8956, 87, 88sylancr 663 . . . . . . . . . . . . 13
90 ffun 5681 . . . . . . . . . . . . 13
91 funiunfv 6090 . . . . . . . . . . . . 13
9289, 90, 913syl 20 . . . . . . . . . . . 12
93 elfznn 11623 . . . . . . . . . . . . . 14
94 fvco3 5891 . . . . . . . . . . . . . 14
958, 93, 94syl2an 477 . . . . . . . . . . . . 13
9695iuneq2dv 4309 . . . . . . . . . . . 12
9792, 96eqtr3d 2497 . . . . . . . . . . 11
983, 97syl5eq 2507 . . . . . . . . . 10
9998ineq2d 3666 . . . . . . . . 9
100 incom 3657 . . . . . . . . 9
101 iunin2 4351 . . . . . . . . . . . . 13
102 incom 3657 . . . . . . . . . . . . . . 15
103102a1i 11 . . . . . . . . . . . . . 14
104103iuneq2i 4306 . . . . . . . . . . . . 13
105 incom 3657 . . . . . . . . . . . . 13
106101, 104, 1053eqtr4ri 2494 . . . . . . . . . . . 12
107106a1i 11 . . . . . . . . . . 11
108107iuneq2i 4306 . . . . . . . . . 10
109 iunin2 4351 . . . . . . . . . 10
110108, 109eqtr3i 2485 . . . . . . . . 9
11199, 100, 1103eqtr4g 2520 . . . . . . . 8
112111uneq2d 3624 . . . . . . 7
11385, 112eqtrd 2495 . . . . . 6
11438, 113syl5sseqr 3519 . . . . 5
115114, 1syl6ss 3482 . . . 4
116 ovolsscl 21368 . . . 4
117115, 14, 31, 116syl3anc 1219 . . 3
11837, 117readdcld 9550 . 2
11920rpred 11166 . . 3
12037, 119readdcld 9550 . 2
121113fveq2d 5817 . . 3
12235, 14sstrd 3480 . . . 4
123115, 14sstrd 3480 . . . 4
124 ovolun 21381 . . . 4
125122, 37, 123, 117, 124syl22anc 1220 . . 3
126121, 125eqbrtrd 4429 . 2
127 fzfid 11940 . . . . 5
128 iunss 4328 . . . . . . . 8
129115, 128sylib 196 . . . . . . 7
130129r19.21bi 2922 . . . . . 6
13114adantr 465 . . . . . 6
13231adantr 465 . . . . . 6
133 ovolsscl 21368 . . . . . 6
134130, 131, 132, 133syl3anc 1219 . . . . 5
135127, 134fsumrecl 13369 . . . 4
136130, 131sstrd 3480 . . . . . . 7
137136, 134jca 532 . . . . . 6
138137ralrimiva 2831 . . . . 5
139 ovolfiniun 21383 . . . . 5
140127, 138, 139syl2anc 661 . . . 4
141 uniioombl.m . . . . . . . 8
142119, 141nndivred 10508 . . . . . . 7
143142adantr 465 . . . . . 6
14480ineq2d 3666 . . . . . . . . . . . . 13
145144adantr 465 . . . . . . . . . . . 12
146102a1i 11 . . . . . . . . . . . . . 14
147146iuneq2i 4306 . . . . . . . . . . . . 13
148 iunin2 4351 . . . . . . . . . . . . 13
149147, 148eqtri 2483 . . . . . . . . . . . 12
150145, 149syl6eqr 2513 . . . . . . . . . . 11
151 fzfid 11940 . . . . . . . . . . . 12
152 ffvelrn 5964 . . . . . . . . . . . . . . . . . . . . 21
15315, 76, 152syl2an 477 . . . . . . . . . . . . . . . . . . . 20
15457, 153sseldi 3468 . . . . . . . . . . . . . . . . . . 19
155 1st2nd2 6746 . . . . . . . . . . . . . . . . . . 19
156154, 155syl 16 . . . . . . . . . . . . . . . . . 18
157156fveq2d 5817 . . . . . . . . . . . . . . . . 17
158 df-ov 6225 . . . . . . . . . . . . . . . . 17
159157, 158syl6eqr 2513 . . . . . . . . . . . . . . . 16
160 ioombl 21446 . . . . . . . . . . . . . . . 16
161159, 160syl6eqel 2550 . . . . . . . . . . . . . . 15
162161adantlr 714 . . . . . . . . . . . . . 14
163 ffvelrn 5964 . . . . . . . . . . . . . . . . . . . . 21
1648, 93, 163syl2an 477 . . . . . . . . . . . . . . . . . . . 20
16557, 164sseldi 3468 . . . . . . . . . . . . . . . . . . 19
166 1st2nd2 6746 . . . . . . . . . . . . . . . . . . 19
167165, 166syl 16 . . . . . . . . . . . . . . . . . 18
168167fveq2d 5817 . . . . . . . . . . . . . . . . 17
169 df-ov 6225 . . . . . . . . . . . . . . . . 17
170168, 169syl6eqr 2513 . . . . . . . . . . . . . . . 16
171 ioombl 21446 . . . . . . . . . . . . . . . 16
172170, 171syl6eqel 2550 . . . . . . . . . . . . . . 15
173172adantr 465 . . . . . . . . . . . . . 14
174 inmbl 21423 . . . . . . . . . . . . . 14
175162, 173, 174syl2anc 661 . . . . . . . . . . . . 13
176175ralrimiva 2831 . . . . . . . . . . . 12
177 finiunmbl 21425 . . . . . . . . . . . 12
178151, 176, 177syl2anc 661 . . . . . . . . . . 11
179150, 178eqeltrd 2542 . . . . . . . . . 10
180 inss2 3685 . . . . . . . . . . 11 <