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

Theorem frec2uzrdg 10206
 Description: A helper lemma for the value of a recursive definition generator on upper integers (typically either or ) with characteristic function and initial value . This lemma shows that evaluating at an element of gives an ordered pair whose first element is the index (translated from to ). See comment in frec2uz0d 10196 which describes and the index translation. (Contributed by Jim Kingdon, 24-May-2020.)
Hypotheses
Ref Expression
frec2uz.1
frec2uz.2 frec
frecuzrdgrrn.a
frecuzrdgrrn.f
frecuzrdgrrn.2 frec
frec2uzrdg.b
Assertion
Ref Expression
frec2uzrdg
Distinct variable groups:   ,   ,,   ,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)   (,)   ()

Proof of Theorem frec2uzrdg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frec2uzrdg.b . 2
2 fveq2 5424 . . . . 5
3 fveq2 5424 . . . . . 6
42fveq2d 5428 . . . . . 6
53, 4opeq12d 3716 . . . . 5
62, 5eqeq12d 2154 . . . 4
76imbi2d 229 . . 3
8 fveq2 5424 . . . . 5
9 fveq2 5424 . . . . . 6
108fveq2d 5428 . . . . . 6
119, 10opeq12d 3716 . . . . 5
128, 11eqeq12d 2154 . . . 4
13 fveq2 5424 . . . . 5
14 fveq2 5424 . . . . . 6
1513fveq2d 5428 . . . . . 6
1614, 15opeq12d 3716 . . . . 5
1713, 16eqeq12d 2154 . . . 4
18 fveq2 5424 . . . . 5
19 fveq2 5424 . . . . . 6
2018fveq2d 5428 . . . . . 6
2119, 20opeq12d 3716 . . . . 5
2218, 21eqeq12d 2154 . . . 4
23 frecuzrdgrrn.2 . . . . . . 7 frec
2423fveq1i 5425 . . . . . 6 frec
25 frec2uz.1 . . . . . . . 8
26 frecuzrdgrrn.a . . . . . . . 8
27 opexg 4153 . . . . . . . 8
2825, 26, 27syl2anc 408 . . . . . . 7
29 frec0g 6297 . . . . . . 7 frec
3028, 29syl 14 . . . . . 6 frec
3124, 30syl5eq 2184 . . . . 5
32 frec2uz.2 . . . . . . 7 frec
3325, 32frec2uz0d 10196 . . . . . 6
3431fveq2d 5428 . . . . . . 7
35 uzid 9359 . . . . . . . . 9
3625, 35syl 14 . . . . . . . 8
37 op2ndg 6052 . . . . . . . 8
3836, 26, 37syl2anc 408 . . . . . . 7
3934, 38eqtrd 2172 . . . . . 6
4033, 39opeq12d 3716 . . . . 5
4131, 40eqtr4d 2175 . . . 4
42 1st2nd2 6076 . . . . . . . . . . . . . . 15
4342adantl 275 . . . . . . . . . . . . . 14
4443fveq2d 5428 . . . . . . . . . . . . 13
45 df-ov 5780 . . . . . . . . . . . . . . 15
46 xp1st 6066 . . . . . . . . . . . . . . . . 17
4746adantl 275 . . . . . . . . . . . . . . . 16
48 xp2nd 6067 . . . . . . . . . . . . . . . . 17
4948adantl 275 . . . . . . . . . . . . . . . 16
50 peano2uz 9400 . . . . . . . . . . . . . . . . . 18
5147, 50syl 14 . . . . . . . . . . . . . . . . 17
52 frecuzrdgrrn.f . . . . . . . . . . . . . . . . . . . 20
5352ralrimivva 2514 . . . . . . . . . . . . . . . . . . 19
5453ad2antrr 479 . . . . . . . . . . . . . . . . . 18
55 oveq1 5784 . . . . . . . . . . . . . . . . . . . . 21
5655eleq1d 2208 . . . . . . . . . . . . . . . . . . . 20
57 oveq2 5785 . . . . . . . . . . . . . . . . . . . . 21
5857eleq1d 2208 . . . . . . . . . . . . . . . . . . . 20
5956, 58rspc2v 2802 . . . . . . . . . . . . . . . . . . 19
6047, 49, 59syl2anc 408 . . . . . . . . . . . . . . . . . 18
6154, 60mpd 13 . . . . . . . . . . . . . . . . 17
62 opelxp 4572 . . . . . . . . . . . . . . . . 17
6351, 61, 62sylanbrc 413 . . . . . . . . . . . . . . . 16
64 oveq1 5784 . . . . . . . . . . . . . . . . . 18
6564, 55opeq12d 3716 . . . . . . . . . . . . . . . . 17
6657opeq2d 3715 . . . . . . . . . . . . . . . . 17
67 eqid 2139 . . . . . . . . . . . . . . . . 17
6865, 66, 67ovmpog 5908 . . . . . . . . . . . . . . . 16
6947, 49, 63, 68syl3anc 1216 . . . . . . . . . . . . . . 15
7045, 69syl5eqr 2186 . . . . . . . . . . . . . 14
7170, 63eqeltrd 2216 . . . . . . . . . . . . 13
7244, 71eqeltrd 2216 . . . . . . . . . . . 12
7372ralrimiva 2505 . . . . . . . . . . 11
7436adantr 274 . . . . . . . . . . . 12
7526adantr 274 . . . . . . . . . . . 12
76 opelxp 4572 . . . . . . . . . . . 12
7774, 75, 76sylanbrc 413 . . . . . . . . . . 11
78 simpr 109 . . . . . . . . . . 11
79 frecsuc 6307 . . . . . . . . . . 11 frec frec
8073, 77, 78, 79syl3anc 1216 . . . . . . . . . 10 frec frec
8123fveq1i 5425 . . . . . . . . . 10 frec
8223fveq1i 5425 . . . . . . . . . . 11 frec
8382fveq2i 5427 . . . . . . . . . 10 frec
8480, 81, 833eqtr4g 2197 . . . . . . . . 9
8584adantr 274 . . . . . . . 8
86 fveq2 5424 . . . . . . . . 9
87 df-ov 5780 . . . . . . . . . 10
8825adantr 274 . . . . . . . . . . . 12
8988, 32, 78frec2uzuzd 10199 . . . . . . . . . . 11
9025, 32, 26, 52, 23frecuzrdgrrn 10205 . . . . . . . . . . . 12
91 xp2nd 6067 . . . . . . . . . . . 12
9290, 91syl 14 . . . . . . . . . . 11
93 peano2uz 9400 . . . . . . . . . . . . 13
9489, 93syl 14 . . . . . . . . . . . 12
9552caovclg 5926 . . . . . . . . . . . . . 14
9695adantlr 468 . . . . . . . . . . . . 13
9796, 89, 92caovcld 5927 . . . . . . . . . . . 12
98 opelxp 4572 . . . . . . . . . . . 12
9994, 97, 98sylanbrc 413 . . . . . . . . . . 11
100 oveq1 5784 . . . . . . . . . . . . 13
101 oveq1 5784 . . . . . . . . . . . . 13
102100, 101opeq12d 3716 . . . . . . . . . . . 12
103 oveq2 5785 . . . . . . . . . . . . 13
104103opeq2d 3715 . . . . . . . . . . . 12
105 oveq1 5784 . . . . . . . . . . . . . 14
106 oveq1 5784 . . . . . . . . . . . . . 14
107105, 106opeq12d 3716 . . . . . . . . . . . . 13
108 oveq2 5785 . . . . . . . . . . . . . 14
109108opeq2d 3715 . . . . . . . . . . . . 13
110107, 109cbvmpov 5854 . . . . . . . . . . . 12
111102, 104, 110ovmpog 5908 . . . . . . . . . . 11
11289, 92, 99, 111syl3anc 1216 . . . . . . . . . 10
11387, 112syl5eqr 2186 . . . . . . . . 9
11486, 113sylan9eqr 2194 . . . . . . . 8
11585, 114eqtrd 2172 . . . . . . 7
11688, 32, 78frec2uzsucd 10198 . . . . . . . . 9
117116adantr 274 . . . . . . . 8
118115fveq2d 5428 . . . . . . . . 9
11988, 32, 78frec2uzzd 10197 . . . . . . . . . . . 12
120119peano2zd 9195 . . . . . . . . . . 11
121120adantr 274 . . . . . . . . . 10
12297adantr 274 . . . . . . . . . 10
123 op2ndg 6052 . . . . . . . . . 10
124121, 122, 123syl2anc 408 . . . . . . . . 9
125118, 124eqtrd 2172 . . . . . . . 8
126117, 125opeq12d 3716 . . . . . . 7
127115, 126eqtr4d 2175 . . . . . 6
128127ex 114 . . . . 5
129128expcom 115 . . . 4
13012, 17, 22, 41, 129finds2 4518 . . 3
1317, 130vtoclga 2752 . 2
1321, 131mpcom 36 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wceq 1331   wcel 1480  wral 2416  cvv 2686  c0 3363  cop 3530   cmpt 3992   csuc 4290  com 4507   cxp 4540  cfv 5126  (class class class)co 5777   cmpo 5779  c1st 6039  c2nd 6040  freccfrec 6290  c1 7640   caddc 7642  cz 9073  cuz 9345 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4046  ax-sep 4049  ax-nul 4057  ax-pow 4101  ax-pr 4134  ax-un 4358  ax-setind 4455  ax-iinf 4505  ax-cnex 7730  ax-resscn 7731  ax-1cn 7732  ax-1re 7733  ax-icn 7734  ax-addcl 7735  ax-addrcl 7736  ax-mulcl 7737  ax-addcom 7739  ax-addass 7741  ax-distr 7743  ax-i2m1 7744  ax-0lt1 7745  ax-0id 7747  ax-rnegex 7748  ax-cnre 7750  ax-pre-ltirr 7751  ax-pre-ltwlin 7752  ax-pre-lttrn 7753  ax-pre-ltadd 7755 This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3740  df-int 3775  df-iun 3818  df-br 3933  df-opab 3993  df-mpt 3994  df-tr 4030  df-id 4218  df-iord 4291  df-on 4293  df-ilim 4294  df-suc 4296  df-iom 4508  df-xp 4548  df-rel 4549  df-cnv 4550  df-co 4551  df-dm 4552  df-rn 4553  df-res 4554  df-ima 4555  df-iota 5091  df-fun 5128  df-fn 5129  df-f 5130  df-f1 5131  df-fo 5132  df-f1o 5133  df-fv 5134  df-riota 5733  df-ov 5780  df-oprab 5781  df-mpo 5782  df-1st 6041  df-2nd 6042  df-recs 6205  df-frec 6291  df-pnf 7821  df-mnf 7822  df-xr 7823  df-ltxr 7824  df-le 7825  df-sub 7954  df-neg 7955  df-inn 8740  df-n0 8997  df-z 9074  df-uz 9346 This theorem is referenced by:  frecuzrdglem  10208  frecuzrdgtcl  10209  frecuzrdgsuc  10211
 Copyright terms: Public domain W3C validator