ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  frecuzrdgrrn Structured version   GIF version

Theorem frecuzrdgrrn 8835
Description: The function 𝑅 (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of 𝑆. (Contributed by Jim Kingdon, 27-May-2020.)
Hypotheses
Ref Expression
frec2uz.1 (φ𝐶 ℤ)
frec2uz.2 𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)
uzrdg.s (φ𝑆 𝑉)
uzrdg.a (φA 𝑆)
uzrdg.f ((φ (x (ℤ𝐶) y 𝑆)) → (x𝐹y) 𝑆)
uzrdg.2 𝑅 = frec((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)
Assertion
Ref Expression
frecuzrdgrrn ((φ 𝐷 𝜔) → (𝑅𝐷) ((ℤ𝐶) × 𝑆))
Distinct variable groups:   y,A   x,𝐶,y   y,𝐺   x,𝐹,y   x,𝑆,y   φ,x,y
Allowed substitution hints:   A(x)   𝐷(x,y)   𝑅(x,y)   𝐺(x)   𝑉(x,y)

Proof of Theorem frecuzrdgrrn
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 uzrdg.2 . . 3 𝑅 = frec((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)
21fveq1i 5122 . 2 (𝑅𝐷) = (frec((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)‘𝐷)
3 zex 7990 . . . . . . . 8 V
4 uzssz 8228 . . . . . . . 8 (ℤ𝐶) ⊆ ℤ
53, 4ssexi 3886 . . . . . . 7 (ℤ𝐶) V
65a1i 9 . . . . . 6 ((φ 𝐷 𝜔) → (ℤ𝐶) V)
7 uzrdg.s . . . . . . 7 (φ𝑆 𝑉)
87adantr 261 . . . . . 6 ((φ 𝐷 𝜔) → 𝑆 𝑉)
9 mpt2exga 5777 . . . . . 6 (((ℤ𝐶) V 𝑆 𝑉) → (x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩) V)
106, 8, 9syl2anc 391 . . . . 5 ((φ 𝐷 𝜔) → (x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩) V)
11 vex 2554 . . . . . 6 z V
1211a1i 9 . . . . 5 ((φ 𝐷 𝜔) → z V)
13 fvexg 5137 . . . . 5 (((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩) V z V) → ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘z) V)
1410, 12, 13syl2anc 391 . . . 4 ((φ 𝐷 𝜔) → ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘z) V)
1514alrimiv 1751 . . 3 ((φ 𝐷 𝜔) → z((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘z) V)
16 frec2uz.1 . . . . . 6 (φ𝐶 ℤ)
17 uzid 8223 . . . . . 6 (𝐶 ℤ → 𝐶 (ℤ𝐶))
1816, 17syl 14 . . . . 5 (φ𝐶 (ℤ𝐶))
19 uzrdg.a . . . . 5 (φA 𝑆)
20 opelxp 4317 . . . . 5 (⟨𝐶, A ((ℤ𝐶) × 𝑆) ↔ (𝐶 (ℤ𝐶) A 𝑆))
2118, 19, 20sylanbrc 394 . . . 4 (φ → ⟨𝐶, A ((ℤ𝐶) × 𝑆))
2221adantr 261 . . 3 ((φ 𝐷 𝜔) → ⟨𝐶, A ((ℤ𝐶) × 𝑆))
23 1st2nd2 5743 . . . . . . 7 (z ((ℤ𝐶) × 𝑆) → z = ⟨(1stz), (2ndz)⟩)
24 fveq2 5121 . . . . . . . 8 (z = ⟨(1stz), (2ndz)⟩ → ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘z) = ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘⟨(1stz), (2ndz)⟩))
25 df-ov 5458 . . . . . . . 8 ((1stz)(x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)(2ndz)) = ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘⟨(1stz), (2ndz)⟩)
2624, 25syl6eqr 2087 . . . . . . 7 (z = ⟨(1stz), (2ndz)⟩ → ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘z) = ((1stz)(x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)(2ndz)))
2723, 26syl 14 . . . . . 6 (z ((ℤ𝐶) × 𝑆) → ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘z) = ((1stz)(x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)(2ndz)))
2827adantl 262 . . . . 5 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘z) = ((1stz)(x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)(2ndz)))
29 xp1st 5734 . . . . . . 7 (z ((ℤ𝐶) × 𝑆) → (1stz) (ℤ𝐶))
3029adantl 262 . . . . . 6 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → (1stz) (ℤ𝐶))
31 xp2nd 5735 . . . . . . 7 (z ((ℤ𝐶) × 𝑆) → (2ndz) 𝑆)
3231adantl 262 . . . . . 6 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → (2ndz) 𝑆)
33 peano2uz 8262 . . . . . . . 8 ((1stz) (ℤ𝐶) → ((1stz) + 1) (ℤ𝐶))
3430, 33syl 14 . . . . . . 7 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → ((1stz) + 1) (ℤ𝐶))
35 uzrdg.f . . . . . . . . . 10 ((φ (x (ℤ𝐶) y 𝑆)) → (x𝐹y) 𝑆)
3635ralrimivva 2395 . . . . . . . . 9 (φx (ℤ𝐶)y 𝑆 (x𝐹y) 𝑆)
3736ad2antrr 457 . . . . . . . 8 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → x (ℤ𝐶)y 𝑆 (x𝐹y) 𝑆)
38 oveq1 5462 . . . . . . . . . . 11 (x = (1stz) → (x𝐹y) = ((1stz)𝐹y))
3938eleq1d 2103 . . . . . . . . . 10 (x = (1stz) → ((x𝐹y) 𝑆 ↔ ((1stz)𝐹y) 𝑆))
40 oveq2 5463 . . . . . . . . . . 11 (y = (2ndz) → ((1stz)𝐹y) = ((1stz)𝐹(2ndz)))
4140eleq1d 2103 . . . . . . . . . 10 (y = (2ndz) → (((1stz)𝐹y) 𝑆 ↔ ((1stz)𝐹(2ndz)) 𝑆))
4239, 41rspc2v 2656 . . . . . . . . 9 (((1stz) (ℤ𝐶) (2ndz) 𝑆) → (x (ℤ𝐶)y 𝑆 (x𝐹y) 𝑆 → ((1stz)𝐹(2ndz)) 𝑆))
4330, 32, 42syl2anc 391 . . . . . . . 8 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → (x (ℤ𝐶)y 𝑆 (x𝐹y) 𝑆 → ((1stz)𝐹(2ndz)) 𝑆))
4437, 43mpd 13 . . . . . . 7 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → ((1stz)𝐹(2ndz)) 𝑆)
45 opelxp 4317 . . . . . . 7 (⟨((1stz) + 1), ((1stz)𝐹(2ndz))⟩ ((ℤ𝐶) × 𝑆) ↔ (((1stz) + 1) (ℤ𝐶) ((1stz)𝐹(2ndz)) 𝑆))
4634, 44, 45sylanbrc 394 . . . . . 6 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → ⟨((1stz) + 1), ((1stz)𝐹(2ndz))⟩ ((ℤ𝐶) × 𝑆))
47 oveq1 5462 . . . . . . . 8 (x = (1stz) → (x + 1) = ((1stz) + 1))
4847, 38opeq12d 3548 . . . . . . 7 (x = (1stz) → ⟨(x + 1), (x𝐹y)⟩ = ⟨((1stz) + 1), ((1stz)𝐹y)⟩)
4940opeq2d 3547 . . . . . . 7 (y = (2ndz) → ⟨((1stz) + 1), ((1stz)𝐹y)⟩ = ⟨((1stz) + 1), ((1stz)𝐹(2ndz))⟩)
50 eqid 2037 . . . . . . 7 (x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩) = (x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)
5148, 49, 50ovmpt2g 5577 . . . . . 6 (((1stz) (ℤ𝐶) (2ndz) 𝑆 ⟨((1stz) + 1), ((1stz)𝐹(2ndz))⟩ ((ℤ𝐶) × 𝑆)) → ((1stz)(x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)(2ndz)) = ⟨((1stz) + 1), ((1stz)𝐹(2ndz))⟩)
5230, 32, 46, 51syl3anc 1134 . . . . 5 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → ((1stz)(x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)(2ndz)) = ⟨((1stz) + 1), ((1stz)𝐹(2ndz))⟩)
5328, 52eqtrd 2069 . . . 4 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘z) = ⟨((1stz) + 1), ((1stz)𝐹(2ndz))⟩)
5453, 46eqeltrd 2111 . . 3 (((φ 𝐷 𝜔) z ((ℤ𝐶) × 𝑆)) → ((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩)‘z) ((ℤ𝐶) × 𝑆))
55 simpr 103 . . 3 ((φ 𝐷 𝜔) → 𝐷 𝜔)
5615, 22, 54, 55freccl 5932 . 2 ((φ 𝐷 𝜔) → (frec((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)‘𝐷) ((ℤ𝐶) × 𝑆))
572, 56syl5eqel 2121 1 ((φ 𝐷 𝜔) → (𝑅𝐷) ((ℤ𝐶) × 𝑆))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1242   wcel 1390  wral 2300  Vcvv 2551  cop 3370  cmpt 3809  𝜔com 4256   × cxp 4286  cfv 4845  (class class class)co 5455  cmpt2 5457  1st c1st 5707  2nd c2nd 5708  freccfrec 5917  1c1 6672   + caddc 6674  cz 7981  cuz 8209
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254  ax-cnex 6734  ax-resscn 6735  ax-1cn 6736  ax-1re 6737  ax-icn 6738  ax-addcl 6739  ax-addrcl 6740  ax-mulcl 6741  ax-addcom 6743  ax-addass 6745  ax-distr 6747  ax-i2m1 6748  ax-0id 6751  ax-rnegex 6752  ax-cnre 6754  ax-pre-ltirr 6755  ax-pre-ltwlin 6756  ax-pre-lttrn 6757  ax-pre-ltadd 6759
This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-nel 2204  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-riota 5411  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-frec 5918  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337  df-enq0 6406  df-nq0 6407  df-0nq0 6408  df-plq0 6409  df-mq0 6410  df-inp 6448  df-i1p 6449  df-iplp 6450  df-iltp 6452  df-enr 6614  df-nr 6615  df-ltr 6618  df-0r 6619  df-1r 6620  df-0 6678  df-1 6679  df-r 6681  df-lt 6684  df-pnf 6819  df-mnf 6820  df-xr 6821  df-ltxr 6822  df-le 6823  df-sub 6941  df-neg 6942  df-inn 7656  df-n0 7918  df-z 7982  df-uz 8210
This theorem is referenced by:  frec2uzrdg  8836  frecuzrdgfn  8839  frecuzrdgcl  8840  frecuzrdgsuc  8842
  Copyright terms: Public domain W3C validator