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

Theorem incexclem 13648
Description: Lemma for incexc 13649. (Contributed by Mario Carneiro, 7-Aug-2017.)
Assertion
Ref Expression
incexclem
Distinct variable groups:   ,   ,

Proof of Theorem incexclem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unieq 4257 . . . . . . . . . . 11
2 uni0 4276 . . . . . . . . . . 11
31, 2syl6eq 2514 . . . . . . . . . 10
43ineq2d 3699 . . . . . . . . 9
5 in0 3811 . . . . . . . . 9
64, 5syl6eq 2514 . . . . . . . 8
76fveq2d 5875 . . . . . . 7
8 hash0 12437 . . . . . . 7
97, 8syl6eq 2514 . . . . . 6
109oveq2d 6312 . . . . 5
11 pweq 4015 . . . . . . 7
12 pw0 4177 . . . . . . 7
1311, 12syl6eq 2514 . . . . . 6
1413sumeq1d 13523 . . . . 5
1510, 14eqeq12d 2479 . . . 4
1615ralbidv 2896 . . 3
17 unieq 4257 . . . . . . . 8
1817ineq2d 3699 . . . . . . 7
1918fveq2d 5875 . . . . . 6
2019oveq2d 6312 . . . . 5
21 pweq 4015 . . . . . 6
2221sumeq1d 13523 . . . . 5
2320, 22eqeq12d 2479 . . . 4
2423ralbidv 2896 . . 3
25 unieq 4257 . . . . . . . . 9
26 uniun 4268 . . . . . . . . . 10
27 vex 3112 . . . . . . . . . . . 12
2827unisn 4264 . . . . . . . . . . 11
2928uneq2i 3654 . . . . . . . . . 10
3026, 29eqtri 2486 . . . . . . . . 9
3125, 30syl6eq 2514 . . . . . . . 8
3231ineq2d 3699 . . . . . . 7
3332fveq2d 5875 . . . . . 6
3433oveq2d 6312 . . . . 5
35 pweq 4015 . . . . . 6
3635sumeq1d 13523 . . . . 5
3734, 36eqeq12d 2479 . . . 4
3837ralbidv 2896 . . 3
39 unieq 4257 . . . . . . . 8
4039ineq2d 3699 . . . . . . 7
4140fveq2d 5875 . . . . . 6
4241oveq2d 6312 . . . . 5
43 pweq 4015 . . . . . 6
4443sumeq1d 13523 . . . . 5
4542, 44eqeq12d 2479 . . . 4
4645ralbidv 2896 . . 3
47 hashcl 12428 . . . . . . 7
4847nn0cnd 10879 . . . . . 6
4948mulid2d 9635 . . . . 5
50 0ex 4582 . . . . . 6
5149, 48eqeltrd 2545 . . . . . 6
52 fveq2 5871 . . . . . . . . . . 11
5352, 8syl6eq 2514 . . . . . . . . . 10
5453oveq2d 6312 . . . . . . . . 9
55 neg1cn 10664 . . . . . . . . . 10
56 exp0 12170 . . . . . . . . . 10
5755, 56ax-mp 5 . . . . . . . . 9
5854, 57syl6eq 2514 . . . . . . . 8
59 rint0 4327 . . . . . . . . 9
6059fveq2d 5875 . . . . . . . 8
6158, 60oveq12d 6314 . . . . . . 7
6261sumsn 13563 . . . . . 6
6350, 51, 62sylancr 663 . . . . 5
6448subid1d 9943 . . . . 5
6549, 63, 643eqtr4rd 2509 . . . 4
6665rgen 2817 . . 3
67 fveq2 5871 . . . . . . . . . . . 12
68 ineq1 3692 . . . . . . . . . . . . 13
6968fveq2d 5875 . . . . . . . . . . . 12
7067, 69oveq12d 6314 . . . . . . . . . . 11
71 simpl 457 . . . . . . . . . . . . . . 15
7271ineq1d 3698 . . . . . . . . . . . . . 14
7372fveq2d 5875 . . . . . . . . . . . . 13
7473oveq2d 6312 . . . . . . . . . . . 12
7574sumeq2dv 13525 . . . . . . . . . . 11
7670, 75eqeq12d 2479 . . . . . . . . . 10
7776rspcva 3208 . . . . . . . . 9
7877adantll 713 . . . . . . . 8
79 simpr 461 . . . . . . . . . 10
80 inss1 3717 . . . . . . . . . 10
81 ssfi 7760 . . . . . . . . . 10
8279, 80, 81sylancl 662 . . . . . . . . 9
83 fveq2 5871 . . . . . . . . . . . 12
84 ineq1 3692 . . . . . . . . . . . . . 14
85 in32 3709 . . . . . . . . . . . . . . 15
86 inass 3707 . . . . . . . . . . . . . . 15
8785, 86eqtri 2486 . . . . . . . . . . . . . 14
8884, 87syl6eq 2514 . . . . . . . . . . . . 13
8988fveq2d 5875 . . . . . . . . . . . 12
9083, 89oveq12d 6314 . . . . . . . . . . 11
91 ineq1 3692 . . . . . . . . . . . . . . 15
92 in32 3709 . . . . . . . . . . . . . . . 16
93 inass 3707 . . . . . . . . . . . . . . . 16
9492, 93eqtri 2486 . . . . . . . . . . . . . . 15
9591, 94syl6eq 2514 . . . . . . . . . . . . . 14
9695fveq2d 5875 . . . . . . . . . . . . 13
9796oveq2d 6312 . . . . . . . . . . . 12
9897sumeq2sdv 13526 . . . . . . . . . . 11
9990, 98eqeq12d 2479 . . . . . . . . . 10
10099rspcva 3208 . . . . . . . . 9
10182, 100sylan 471 . . . . . . . 8
10278, 101oveq12d 6314 . . . . . . 7
103 inss1 3717 . . . . . . . . . . . . . 14
104 ssfi 7760 . . . . . . . . . . . . . 14
10579, 103, 104sylancl 662 . . . . . . . . . . . . 13
106 hashun3 12452 . . . . . . . . . . . . 13
107105, 82, 106syl2anc 661 . . . . . . . . . . . 12
108 indi 3743 . . . . . . . . . . . . 13
109108fveq2i 5874 . . . . . . . . . . . 12
110 inindi 3714 . . . . . . . . . . . . . 14
111110fveq2i 5874 . . . . . . . . . . . . 13
112111oveq2i 6307 . . . . . . . . . . . 12
113107, 109, 1123eqtr4g 2523 . . . . . . . . . . 11
114 hashcl 12428 . . . . . . . . . . . . . 14
115105, 114syl 16 . . . . . . . . . . . . 13
116115nn0cnd 10879 . . . . . . . . . . . 12
117 hashcl 12428 . . . . . . . . . . . . . 14
11882, 117syl 16 . . . . . . . . . . . . 13
119118nn0cnd 10879 . . . . . . . . . . . 12
120 inss1 3717 . . . . . . . . . . . . . . 15
121 ssfi 7760 . . . . . . . . . . . . . . 15
12279, 120, 121sylancl 662 . . . . . . . . . . . . . 14
123 hashcl 12428 . . . . . . . . . . . . . 14
124122, 123syl 16 . . . . . . . . . . . . 13
125124nn0cnd 10879 . . . . . . . . . . . 12
126116, 119, 125addsubassd 9974 . . . . . . . . . . 11
127113, 126eqtrd 2498 . . . . . . . . . 10
128127oveq2d 6312 . . . . . . . . 9
129 hashcl 12428 . . . . . . . . . . . 12
130129adantl 466 . . . . . . . . . . 11
131130nn0cnd 10879 . . . . . . . . . 10
132119, 125subcld 9954 . . . . . . . . . 10
133131, 116, 132subsub4d 9985 . . . . . . . . 9
134128, 133eqtr4d 2501 . . . . . . . 8
135134adantr 465 . . . . . . 7
136 disjdif 3900 . . . . . . . . . . 11
137136a1i 11 . . . . . . . . . 10
138 ssun1 3666 . . . . . . . . . . . . . 14
139 sspwb 4701 . . . . . . . . . . . . . 14
140138, 139mpbi 208 . . . . . . . . . . . . 13
141 undif 3908 . . . . . . . . . . . . 13
142140, 141mpbi 208 . . . . . . . . . . . 12
143142eqcomi 2470 . . . . . . . . . . 11
144143a1i 11 . . . . . . . . . 10
145 simpll 753 . . . . . . . . . . . 12
146 snfi 7616 . . . . . . . . . . . 12
147 unfi 7807 . . . . . . . . . . . 12
148145, 146, 147sylancl 662 . . . . . . . . . . 11
149 pwfi 7835 . . . . . . . . . . 11
150148, 149sylib 196 . . . . . . . . . 10
15155a1i 11 . . . . . . . . . . . 12
152 elpwi 4021 . . . . . . . . . . . . . 14
153 ssfi 7760 . . . . . . . . . . . . . 14
154148, 152, 153syl2an 477 . . . . . . . . . . . . 13
155 hashcl 12428 . . . . . . . . . . . . 13
156154, 155syl 16 . . . . . . . . . . . 12
157151, 156expcld 12310 . . . . . . . . . . 11
158 simplr 755 . . . . . . . . . . . . . 14
159 inss1 3717 . . . . . . . . . . . . . 14
160 ssfi 7760 . . . . . . . . . . . . . 14
161158, 159, 160sylancl 662 . . . . . . . . . . . . 13
162 hashcl 12428 . . . . . . . . . . . . 13
163161, 162syl 16 . . . . . . . . . . . 12
164163nn0cnd 10879 . . . . . . . . . . 11
165157, 164mulcld 9637 . . . . . . . . . 10
166137, 144, 150, 165fsumsplit 13562 . . . . . . . . 9
167 fveq2 5871 . . . . . . . . . . . . . 14
168167oveq2d 6312 . . . . . . . . . . . . 13
169 inteq 4289 . . . . . . . . . . . . . . . 16
17027intunsn 4326 . . . . . . . . . . . . . . . 16
171169, 170syl6eq 2514 . . . . . . . . . . . . . . 15
172171ineq2d 3699 . . . . . . . . . . . . . 14
173172fveq2d 5875 . . . . . . . . . . . . 13
174168, 173oveq12d 6314 . . . . . . . . . . . 12
175 pwfi 7835 . . . . . . . . . . . . 13
176145, 175sylib 196 . . . . . . . . . . . 12
177 eqid 2457 . . . . . . . . . . . . 13
178 elpwi 4021 . . . . . . . . . . . . . . . . 17
179178adantl 466 . . . . . . . . . . . . . . . 16
180 unss1 3672 . . . . . . . . . . . . . . . 16
181179, 180syl 16 . . . . . . . . . . . . . . 15
182 vex 3112 . . . . . . . . . . . . . . . . 17
183 snex 4693 . . . . . . . . . . . . . . . . 17
184182, 183unex 6598 . . . . . . . . . . . . . . . 16
185184elpw 4018 . . . . . . . . . . . . . . 15
186181, 185sylibr 212 . . . . . . . . . . . . . 14
187 simpllr 760 . . . . . . . . . . . . . . 15
188 elpwi 4021 . . . . . . . . . . . . . . . 16
189 ssun2 3667 . . . . . . . . . . . . . . . . . . 19
19027snss 4154 . . . . . . . . . . . . . . . . . . 19
191189, 190mpbir 209 . . . . . . . . . . . . . . . . . 18
192191a1i 11 . . . . . . . . . . . . . . . . 17
193 ssel 3497 . . . . . . . . . . . . . . . . 17
194192, 193syl5com 30 . . . . . . . . . . . . . . . 16
195188, 194syl5 32 . . . . . . . . . . . . . . 15
196187, 195mtod 177 . . . . . . . . . . . . . 14
197186, 196eldifd 3486 . . . . . . . . . . . . 13
198 eldifi 3625 . . . . . . . . . . . . . . . . . 18
199198adantl 466 . . . . . . . . . . . . . . . . 17
200199elpwid 4022 . . . . . . . . . . . . . . . 16
201 uncom 3647 . . . . . . . . . . . . . . . 16
202200, 201syl6sseq 3549 . . . . . . . . . . . . . . 15
203 ssundif 3911 . . . . . . . . . . . . . . 15
204202, 203sylib 196 . . . . . . . . . . . . . 14