Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nnfoctbdjlem Structured version   Visualization version   Unicode version

Theorem nnfoctbdjlem 38409
 Description: There exists a mapping from onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
nnfoctbdjlem.a
nnfoctbdjlem.g
nnfoctbdjlem.dj Disj
nnfoctbdjlem.f
Assertion
Ref Expression
nnfoctbdjlem Disj
Distinct variable groups:   ,,   ,,   ,   ,,   ,,   ,   ,,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem nnfoctbdjlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iftrue 3878 . . . . . . . . 9
21adantl 473 . . . . . . . 8
3 0ex 4528 . . . . . . . . . . 11
43snid 3988 . . . . . . . . . 10
5 elun2 3593 . . . . . . . . . 10
64, 5ax-mp 5 . . . . . . . . 9
76a1i 11 . . . . . . . 8
82, 7eqeltrd 2549 . . . . . . 7
98adantll 728 . . . . . 6
10 iffalse 3881 . . . . . . . 8
1110adantl 473 . . . . . . 7
12 nnfoctbdjlem.g . . . . . . . . . . . 12
13 f1of 5828 . . . . . . . . . . . 12
1412, 13syl 17 . . . . . . . . . . 11
1514adantr 472 . . . . . . . . . 10
16 pm2.46 405 . . . . . . . . . . . 12
17 notnot2 116 . . . . . . . . . . . 12
1816, 17syl 17 . . . . . . . . . . 11
1918adantl 473 . . . . . . . . . 10
2015, 19ffvelrnd 6038 . . . . . . . . 9
2120adantlr 729 . . . . . . . 8
22 elun1 3592 . . . . . . . 8
2321, 22syl 17 . . . . . . 7
2411, 23eqeltrd 2549 . . . . . 6
259, 24pm2.61dan 808 . . . . 5
26 nnfoctbdjlem.f . . . . 5
2725, 26fmptd 6061 . . . 4
28 simpr 468 . . . . . . . . . . 11
29 f1ofo 5835 . . . . . . . . . . . . . 14
30 forn 5809 . . . . . . . . . . . . . 14
3112, 29, 303syl 18 . . . . . . . . . . . . 13
3231eqcomd 2477 . . . . . . . . . . . 12
3332adantr 472 . . . . . . . . . . 11
3428, 33eleqtrd 2551 . . . . . . . . . 10
3514ffnd 5740 . . . . . . . . . . . 12
36 fvelrnb 5926 . . . . . . . . . . . 12
3735, 36syl 17 . . . . . . . . . . 11
3837adantr 472 . . . . . . . . . 10
3934, 38mpbid 215 . . . . . . . . 9
40 nnfoctbdjlem.a . . . . . . . . . . . . . . . 16
4140sselda 3418 . . . . . . . . . . . . . . 15
42 peano2nn 10643 . . . . . . . . . . . . . . 15
4341, 42syl 17 . . . . . . . . . . . . . 14
44433adant3 1050 . . . . . . . . . . . . 13
4526a1i 11 . . . . . . . . . . . . . . . 16
46 1red 9676 . . . . . . . . . . . . . . . . . . . . . 22
47 1red 9676 . . . . . . . . . . . . . . . . . . . . . . . . 25
4841nnrpd 11362 . . . . . . . . . . . . . . . . . . . . . . . . 25
4947, 48ltaddrp2d 11395 . . . . . . . . . . . . . . . . . . . . . . . 24
5049adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
51 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25
5251eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . 24
5352adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23
5450, 53breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . 22
5546, 54gtned 9787 . . . . . . . . . . . . . . . . . . . . 21
5655neneqd 2648 . . . . . . . . . . . . . . . . . . . 20
57 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . 24
5857adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23
5941nncnd 10647 . . . . . . . . . . . . . . . . . . . . . . . . 25
60 1cnd 9677 . . . . . . . . . . . . . . . . . . . . . . . . 25
6159, 60pncand 10006 . . . . . . . . . . . . . . . . . . . . . . . 24
6261adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
6358, 62eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . 22
64 simplr 770 . . . . . . . . . . . . . . . . . . . . . 22
6563, 64eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . 21
6665notnotd 128 . . . . . . . . . . . . . . . . . . . 20
6756, 66jca 541 . . . . . . . . . . . . . . . . . . 19
68 ioran 498 . . . . . . . . . . . . . . . . . . 19
6967, 68sylibr 217 . . . . . . . . . . . . . . . . . 18
7069iffalsed 3883 . . . . . . . . . . . . . . . . 17
7163fveq2d 5883 . . . . . . . . . . . . . . . . 17
7270, 71eqtrd 2505 . . . . . . . . . . . . . . . 16
7314ffvelrnda 6037 . . . . . . . . . . . . . . . 16
7445, 72, 43, 73fvmptd 5969 . . . . . . . . . . . . . . 15
75743adant3 1050 . . . . . . . . . . . . . 14
76 simp3 1032 . . . . . . . . . . . . . 14
7775, 76eqtrd 2505 . . . . . . . . . . . . 13
78 fveq2 5879 . . . . . . . . . . . . . . 15
7978eqeq1d 2473 . . . . . . . . . . . . . 14
8079rspcev 3136 . . . . . . . . . . . . 13
8144, 77, 80syl2anc 673 . . . . . . . . . . . 12
82813exp 1230 . . . . . . . . . . 11
8382adantr 472 . . . . . . . . . 10
8483rexlimdv 2870 . . . . . . . . 9
8539, 84mpd 15 . . . . . . . 8
86 id 22 . . . . . . . . . . 11
8786eqcomd 2477 . . . . . . . . . 10
8887a1i 11 . . . . . . . . 9
8988reximdva 2858 . . . . . . . 8
9085, 89mpd 15 . . . . . . 7
9190adantlr 729 . . . . . 6
92 simpll 768 . . . . . . 7
93 elunnel1 3566 . . . . . . . . 9
94 elsni 3985 . . . . . . . . 9
9593, 94syl 17 . . . . . . . 8
9695adantll 728 . . . . . . 7
97 1nn 10642 . . . . . . . . 9
9897a1i 11 . . . . . . . 8
9926a1i 11 . . . . . . . . . . 11
1001orcs 401 . . . . . . . . . . . 12
101100adantl 473 . . . . . . . . . . 11
10297a1i 11 . . . . . . . . . . 11
1033a1i 11 . . . . . . . . . . 11
10499, 101, 102, 103fvmptd 5969 . . . . . . . . . 10
105104adantr 472 . . . . . . . . 9
106 id 22 . . . . . . . . . . 11
107106eqcomd 2477 . . . . . . . . . 10
108107adantl 473 . . . . . . . . 9
109105, 108eqtr2d 2506 . . . . . . . 8
110 fveq2 5879 . . . . . . . . . 10
111110eqeq2d 2481 . . . . . . . . 9
112111rspcev 3136 . . . . . . . 8
11398, 109, 112syl2anc 673 . . . . . . 7
11492, 96, 113syl2anc 673 . . . . . 6
11591, 114pm2.61dan 808 . . . . 5
116115ralrimiva 2809 . . . 4
11727, 116jca 541 . . 3
118 dffo3 6052 . . 3
119117, 118sylibr 217 . 2
120 orc 392 . . . . . 6
121120adantl 473 . . . . 5
122 simpl 464 . . . . . 6
123 neqne 2651 . . . . . . 7
124123adantl 473 . . . . . 6
125 simpl 464 . . . . . . . . . . . . . 14
1262, 3syl6eqel 2557 . . . . . . . . . . . . . 14
12726fvmpt2 5972 . . . . . . . . . . . . . 14
128125, 126, 127syl2anc 673 . . . . . . . . . . . . 13
129128, 2eqtrd 2505 . . . . . . . . . . . 12
130129ineq1d 3624 . . . . . . . . . . 11
131 0in 37452 . . . . . . . . . . . 12
132131a1i 11 . . . . . . . . . . 11
133130, 132eqtrd 2505 . . . . . . . . . 10
134133adantlr 729 . . . . . . . . 9
135134ad4ant24 1264 . . . . . . . 8
13626a1i 11 . . . . . . . . . . . . . . 15
137 eqeq1 2475 . . . . . . . . . . . . . . . . . 18
138 oveq1 6315 . . . . . . . . . . . . . . . . . . . 20
139138eleq1d 2533 . . . . . . . . . . . . . . . . . . 19
140139notbid 301 . . . . . . . . . . . . . . . . . 18
141137, 140orbi12d 724 . . . . . . . . . . . . . . . . 17
142 eqidd 2472 . . . . . . . . . . . . . . . . 17
143138fveq2d 5883 . . . . . . . . . . . . . . . . 17
144141, 142, 143ifbieq12d 3899 . . . . . . . . . . . . . . . 16
145144adantl 473 . . . . . . . . . . . . . . 15
146 simpl 464 . . . . . . . . . . . . . . 15
147 iftrue 3878 . . . . . . . . . . . . . . . . 17
1483a1i 11 . . . . . . . . . . . . . . . . 17
149147, 148eqeltrd 2549 . . . . . . . . . . . . . . . 16
150149adantl 473 . . . . . . . . . . . . . . 15
151136, 145, 146, 150fvmptd 5969 . . . . . . . . . . . . . 14
152147adantl 473 . . . . . . . . . . . . . 14
153151, 152eqtrd 2505 . . . . . . . . . . . . 13
154153ineq2d 3625 . . . . . . . . . . . 12
155 in0 3763 . . . . . . . . . . . . 13
156155a1i 11 . . . . . . . . . . . 12
157154, 156eqtrd 2505 . . . . . . . . . . 11
158157adantll 728 . . . . . . . . . 10
159158ad5ant25 1272 . . . . . . . . 9
160 id 22 . . . . . . . . . . . . . . . . 17
161 fvex 5889 . . . . . . . . . . . . . . . . . . 19
1623, 161ifex 3940 . . . . . . . . . . . . . . . . . 18
163162a1i 11 . . . . . . . . . . . . . . . . 17
164160, 163, 127syl2anc 673 . . . . . . . . . . . . . . . 16
165164adantr 472 . . . . . . . . . . . . . . 15
16610adantl 473 . . . . . . . . . . . . . . 15
167165, 166eqtrd 2505 . . . . . . . . . . . . . 14
168167adantlr 729 . . . . . . . . . . . . 13
1691683adant3 1050 . . . . . . . . . . . 12
17026a1i 11 . . . . . . . . . . . . . . 15
171144adantl 473 . . . . . . . . . . . . . . . 16
172 iffalse 3881 . . . . . . . . . . . . . . . . 17
173172ad2antlr 741 . . . . . . . . . . . . . . . 16
174171, 173eqtrd 2505 . . . . . . . . . . . . . . 15
175 simpl 464 . . . . . . . . . . . . . . 15
176 fvex 5889 . . . . . . . . . . . . . . . 16
177176a1i 11 . . . . . . . . . . . . . . 15
178170, 174, 175, 177fvmptd 5969 . . . . . . . . . . . . . 14
179178adantll 728 . . . . . . . . . . . . 13
1801793adant2 1049 . . . . . . . . . . . 12
181169, 180ineq12d 3626 . . . . . . . . . . 11
182181ad5ant245 1273 . . . . . . . . . 10
18318ad2antlr 741 . . . . . . . . . . . . . 14
184 pm2.46 405 . . . . . . . . . . . . . . . 16
185184notnotrd 117 . . . . . . . . . . . . . . 15
186185adantl 473 . . . . . . . . . . . . . 14
187 f1of1 5827 . . . . . . . . . . . . . . . . . . 19
18812, 187syl 17 . . . . . . . . . . . . . . . . . 18
189 dff14a 6188 . . . . . . . . . . . . . . . . . 18
190188, 189sylib 201 . . . . . . . . . . . . . . . . 17
191190simprd 470 . . . . . . . . . . . . . . . 16
192191adantr 472 . . . . . . . . . . . . . . 15
193192ad3antrrr 744 . . . . . . . . . . . . . 14
194183, 186, 193jca31 543 . . . . . . . . . . . . 13
195 nncn 10639 . . . . . . . . . . . . . . . . 17
196195adantr 472 . . . . . . . . . . . . . . . 16
197196ad2antlr 741 . . . . . . . . . . . . . . 15
198 nncn 10639 . . . . . . . . . . . . . . . . 17
199198adantl 473 . . . . . . . . . . . . . . . 16
200199ad2antlr 741 . . . . . . . . . . . . . . 15
201 1cnd 9677 . . . . . . . . . . . . . . 15
202 simpr 468 . . . . . . . . . . . . . . 15
203197, 200, 201, 202subneintr2d 10051 . . . . . . . . . . . . . 14
204203ad2antrr 740 . . . . . . . . . . . . 13
205 neeq1 2705 . . . . . . . . . . . . . . 15
206 fveq2 5879 . . . . . . . . . . . . . . . 16
207206neeq1d 2702 . . . . . . . . . . . . . . 15
208205, 207imbi12d 327 . . . . . . . . . . . . . 14
209 neeq2 2706 . . . . . . . . . . . . . . 15
210 fveq2 5879 . . . . . . . . . . . . . . . 16
211210neeq2d 2703 . . . . . . . . . . . . . . 15
212209, 211imbi12d 327 . . . . . . . . . . . . . 14
213208, 212rspc2va 3148 . . . . . . . . . . . . 13
214194, 204, 213sylc 61 . . . . . . . . . . . 12
215214neneqd 2648 . . . . . . . . . . 11
21620ad4ant13 1258 . . . . . . . . . . . . 13
217 simpl 464 . . . . . . . . . . . . . . 15
218185adantl 473 . . . . . . . . . . . . . . 15
21914ffvelrnda 6037 . . . . . . . . . . . . . . 15
220217, 218, 219syl2anc 673 . . . . . . . . . . . . . 14
221220ad4ant14 1259 . . . . . . . . . . . . 13
222 nnfoctbdjlem.dj . . . . . . . . . . . . . . 15 Disj
223 id 22 . . . . . . . . . . . . . . . 16
224223disjor 4380 . . . . . . . . . . . . . . 15 Disj
225222, 224sylib 201 . . . . . . . . . . . . . 14
226225ad3antrrr 744 . . . . . . . . . . . . 13
227 eqeq1 2475 . . . . . . . . . . . . . . 15
228 ineq1 3618 . . . . . . . . . . . . . . . 16
229228eqeq1d 2473 . . . . . . . . . . . . . . 15
230227, 229orbi12d 724 . . . . . . . . . . . . . 14
231 eqeq2 2482 . . . . . . . . . . . . . . 15
232 ineq2 3619 . . . . . . . . . . . . . . . 16
233232eqeq1d 2473 . . . . . . . . . . . . . . 15
234231, 233orbi12d 724 . . . . . . . . . . . . . 14
235230, 234rspc2va 3148 . . . . . . . . . . . . 13
236216, 221, 226, 235syl21anc 1291 . . . . . . . . . . . 12
237236adantllr 733 . . . . . . . . . . 11
238 orel1 389 . . . . . . . . . . 11
239215, 237, 238sylc 61 . . . . . . . . . 10
240182, 239eqtrd 2505 . . . . . . . . 9
241159, 240pm2.61dan 808 . . . . . . . 8
242135, 241pm2.61dan 808 . . . . . . 7
243 olc 391 . . . . . . 7
244242, 243syl 17 . . . . . 6
245122, 124, 244syl2anc 673 . . . . 5
246121, 245pm2.61dan 808 . . . 4
247246ralrimivva 2814 . . 3
248 fveq2 5879 . . . 4
249248disjor 4380 . . 3 Disj
250247, 249sylibr 217 . 2 Disj
251 nnex 10637 . . . . 5
252251mptex 6152 . . . 4
25326, 252eqeltri 2545 . . 3
254 foeq1 5802 . . . 4
255 simpl 464 . . . . . 6
256255fveq1d 5881 . . . . 5
257256disjeq2dv 4371 . . . 4 Disj Disj
258254, 257anbi12d 725 . . 3 Disj Disj
259253, 258spcev 3127 . 2 Disj Disj
260119, 250, 259syl2anc 673 1 Disj
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904   wne 2641  wral 2756  wrex 2757  cvv 3031   cun 3388   cin 3389   wss 3390  c0 3722  cif 3872  csn 3959  Disj wdisj 4366   class class class wbr 4395   cmpt 4454   crn 4840   wfn 5584  wf 5585  wf1 5586  wfo 5587  wf1o 5588  cfv 5589  (class class class)co 6308  cc 9555  c1 9558   caddc 9560   clt 9693   cmin 9880  cn 10631 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-disj 4367  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-rp 11326 This theorem is referenced by:  nnfoctbdj  38410
 Copyright terms: Public domain W3C validator