Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  frecuzrdgtcl Unicode version

Theorem frecuzrdgtcl 9968
 Description: The recursive definition generator on upper integers is a function. See comment in frec2uz0d 9955 for the description of as the mapping from to . (Contributed by Jim Kingdon, 26-May-2020.)
Hypotheses
Ref Expression
frec2uz.1
frec2uz.2 frec
frecuzrdgrrn.a
frecuzrdgrrn.f
frecuzrdgrrn.2 frec
frecuzrdgtcl.3
Assertion
Ref Expression
frecuzrdgtcl
Distinct variable groups:   ,   ,,   ,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)   (,)   ()

Proof of Theorem frecuzrdgtcl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frecuzrdgtcl.3 . . . . . . . . . 10
21eleq2d 2164 . . . . . . . . 9
3 frec2uz.1 . . . . . . . . . . 11
4 frec2uz.2 . . . . . . . . . . 11 frec
5 frecuzrdgrrn.a . . . . . . . . . . 11
6 frecuzrdgrrn.f . . . . . . . . . . 11
7 frecuzrdgrrn.2 . . . . . . . . . . 11 frec
83, 4, 5, 6, 7frecuzrdgrcl 9966 . . . . . . . . . 10
9 ffn 5195 . . . . . . . . . 10
10 fvelrnb 5387 . . . . . . . . . 10
118, 9, 103syl 17 . . . . . . . . 9
122, 11bitrd 187 . . . . . . . 8
133, 4, 5, 6, 7frecuzrdgrrn 9964 . . . . . . . . . 10
14 eleq1 2157 . . . . . . . . . 10
1513, 14syl5ibcom 154 . . . . . . . . 9
1615rexlimdva 2502 . . . . . . . 8
1712, 16sylbid 149 . . . . . . 7
1817ssrdv 3045 . . . . . 6
19 xpss 4575 . . . . . 6
2018, 19syl6ss 3051 . . . . 5
21 df-rel 4474 . . . . 5
2220, 21sylibr 133 . . . 4
233, 4frec2uzf1od 9962 . . . . . . . . . . 11
24 f1ocnvdm 5598 . . . . . . . . . . 11
2523, 24sylan 278 . . . . . . . . . 10
263, 4, 5, 6, 7frecuzrdgrrn 9964 . . . . . . . . . 10
2725, 26syldan 277 . . . . . . . . 9
28 xp2nd 5975 . . . . . . . . 9
2927, 28syl 14 . . . . . . . 8
301eleq2d 2164 . . . . . . . . . . . 12
31 fvelrnb 5387 . . . . . . . . . . . . 13
328, 9, 313syl 17 . . . . . . . . . . . 12
3330, 32bitrd 187 . . . . . . . . . . 11
343adantr 271 . . . . . . . . . . . . . . . . . . . 20
355adantr 271 . . . . . . . . . . . . . . . . . . . 20
366adantlr 462 . . . . . . . . . . . . . . . . . . . 20
37 simpr 109 . . . . . . . . . . . . . . . . . . . 20
3834, 4, 35, 36, 7, 37frec2uzrdg 9965 . . . . . . . . . . . . . . . . . . 19
3938eqeq1d 2103 . . . . . . . . . . . . . . . . . 18
40 vex 2636 . . . . . . . . . . . . . . . . . . . 20
41 vex 2636 . . . . . . . . . . . . . . . . . . . 20
4240, 41opth2 4091 . . . . . . . . . . . . . . . . . . 19
4342simplbi 269 . . . . . . . . . . . . . . . . . 18
4439, 43syl6bi 162 . . . . . . . . . . . . . . . . 17
45 f1ocnvfv 5596 . . . . . . . . . . . . . . . . . 18
4623, 45sylan 278 . . . . . . . . . . . . . . . . 17
4744, 46syld 45 . . . . . . . . . . . . . . . 16
48 fveq2 5340 . . . . . . . . . . . . . . . . 17
4948fveq2d 5344 . . . . . . . . . . . . . . . 16
5047, 49syl6 33 . . . . . . . . . . . . . . 15
5150imp 123 . . . . . . . . . . . . . 14
5240, 41op2ndd 5958 . . . . . . . . . . . . . . 15
5352adantl 272 . . . . . . . . . . . . . 14
5451, 53eqtr2d 2128 . . . . . . . . . . . . 13
5554ex 114 . . . . . . . . . . . 12
5655rexlimdva 2502 . . . . . . . . . . 11
5733, 56sylbid 149 . . . . . . . . . 10
5857alrimiv 1809 . . . . . . . . 9
5958adantr 271 . . . . . . . 8
60 eqeq2 2104 . . . . . . . . . . 11
6160imbi2d 229 . . . . . . . . . 10
6261albidv 1759 . . . . . . . . 9
6362spcegv 2721 . . . . . . . 8
6429, 59, 63sylc 62 . . . . . . 7
65 nfv 1473 . . . . . . . 8
6665mo2r 2007 . . . . . . 7
6764, 66syl 14 . . . . . 6
68 dmss 4666 . . . . . . . . . . 11
6918, 68syl 14 . . . . . . . . . 10
70 dmxpss 4895 . . . . . . . . . 10
7169, 70syl6ss 3051 . . . . . . . . 9
723adantr 271 . . . . . . . . . . . . . 14
735adantr 271 . . . . . . . . . . . . . 14
746adantlr 462 . . . . . . . . . . . . . 14
75 simpr 109 . . . . . . . . . . . . . 14
7672, 4, 73, 74, 7, 75frecuzrdglem 9967 . . . . . . . . . . . . 13
771eleq2d 2164 . . . . . . . . . . . . . 14
7877adantr 271 . . . . . . . . . . . . 13
7976, 78mpbird 166 . . . . . . . . . . . 12
80 opeldmg 4672 . . . . . . . . . . . . 13
8140, 80mpan 416 . . . . . . . . . . . 12
8229, 79, 81sylc 62 . . . . . . . . . . 11
8382ex 114 . . . . . . . . . 10
8483ssrdv 3045 . . . . . . . . 9
8571, 84eqssd 3056 . . . . . . . 8
8685eleq2d 2164 . . . . . . 7
8786pm5.32i 443 . . . . . 6
88 df-br 3868 . . . . . . 7
8988mobii 1992 . . . . . 6
9067, 87, 893imtr4i 200 . . . . 5
9190ralrimiva 2458 . . . 4
92 dffun7 5076 . . . 4
9322, 91, 92sylanbrc 409 . . 3
94 df-fn 5052 . . 3
9593, 85, 94sylanbrc 409 . 2
96 rnss 4697 . . . 4
9718, 96syl 14 . . 3
98 rnxpss 4896 . . 3
9997, 98syl6ss 3051 . 2
100 df-f 5053 . 2
10195, 99, 100sylanbrc 409 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104  wal 1294   wceq 1296  wex 1433   wcel 1445  wmo 1956  wral 2370  wrex 2371  cvv 2633   wss 3013  cop 3469   class class class wbr 3867   cmpt 3921  com 4433   cxp 4465  ccnv 4466   cdm 4467   crn 4468   wrel 4472   wfun 5043   wfn 5044  wf 5045  wf1o 5048  cfv 5049  (class class class)co 5690   cmpt2 5692  c2nd 5948  freccfrec 6193  c1 7448   caddc 7450  cz 8848  cuz 9118 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-coll 3975  ax-sep 3978  ax-nul 3986  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-iinf 4431  ax-cnex 7533  ax-resscn 7534  ax-1cn 7535  ax-1re 7536  ax-icn 7537  ax-addcl 7538  ax-addrcl 7539  ax-mulcl 7540  ax-addcom 7542  ax-addass 7544  ax-distr 7546  ax-i2m1 7547  ax-0lt1 7548  ax-0id 7550  ax-rnegex 7551  ax-cnre 7553  ax-pre-ltirr 7554  ax-pre-ltwlin 7555  ax-pre-lttrn 7556  ax-pre-ltadd 7558 This theorem depends on definitions:  df-bi 116  df-3or 928  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-nel 2358  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-csb 2948  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-iun 3754  df-br 3868  df-opab 3922  df-mpt 3923  df-tr 3959  df-id 4144  df-iord 4217  df-on 4219  df-ilim 4220  df-suc 4222  df-iom 4434  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-res 4479  df-ima 4480  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056  df-fv 5057  df-riota 5646  df-ov 5693  df-oprab 5694  df-mpt2 5695  df-1st 5949  df-2nd 5950  df-recs 6108  df-frec 6194  df-pnf 7621  df-mnf 7622  df-xr 7623  df-ltxr 7624  df-le 7625  df-sub 7752  df-neg 7753  df-inn 8521  df-n0 8772  df-z 8849  df-uz 9119 This theorem is referenced by:  frecuzrdg0  9969  frecuzrdgsuc  9970
 Copyright terms: Public domain W3C validator