MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  om2uzrdg Structured version   Visualization version   GIF version

Theorem om2uzrdg 13308
Description: A helper lemma for the value of a recursive definition generator on upper integers (typically either or 0) with characteristic function 𝐹(𝑥, 𝑦) and initial value 𝐴. Normally 𝐹 is a function on the partition, and 𝐴 is a member of the partition. See also comment in om2uz0i 13299. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)
Hypotheses
Ref Expression
om2uz.1 𝐶 ∈ ℤ
om2uz.2 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)
uzrdg.1 𝐴 ∈ V
uzrdg.2 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)
Assertion
Ref Expression
om2uzrdg (𝐵 ∈ ω → (𝑅𝐵) = ⟨(𝐺𝐵), (2nd ‘(𝑅𝐵))⟩)
Distinct variable groups:   𝑦,𝐴   𝑥,𝑦,𝐶   𝑦,𝐺   𝑥,𝐹,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝐺(𝑥)

Proof of Theorem om2uzrdg
Dummy variables 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6646 . . 3 (𝑧 = ∅ → (𝑅𝑧) = (𝑅‘∅))
2 fveq2 6646 . . . 4 (𝑧 = ∅ → (𝐺𝑧) = (𝐺‘∅))
3 2fveq3 6651 . . . 4 (𝑧 = ∅ → (2nd ‘(𝑅𝑧)) = (2nd ‘(𝑅‘∅)))
42, 3opeq12d 4787 . . 3 (𝑧 = ∅ → ⟨(𝐺𝑧), (2nd ‘(𝑅𝑧))⟩ = ⟨(𝐺‘∅), (2nd ‘(𝑅‘∅))⟩)
51, 4eqeq12d 2836 . 2 (𝑧 = ∅ → ((𝑅𝑧) = ⟨(𝐺𝑧), (2nd ‘(𝑅𝑧))⟩ ↔ (𝑅‘∅) = ⟨(𝐺‘∅), (2nd ‘(𝑅‘∅))⟩))
6 fveq2 6646 . . 3 (𝑧 = 𝑣 → (𝑅𝑧) = (𝑅𝑣))
7 fveq2 6646 . . . 4 (𝑧 = 𝑣 → (𝐺𝑧) = (𝐺𝑣))
8 2fveq3 6651 . . . 4 (𝑧 = 𝑣 → (2nd ‘(𝑅𝑧)) = (2nd ‘(𝑅𝑣)))
97, 8opeq12d 4787 . . 3 (𝑧 = 𝑣 → ⟨(𝐺𝑧), (2nd ‘(𝑅𝑧))⟩ = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩)
106, 9eqeq12d 2836 . 2 (𝑧 = 𝑣 → ((𝑅𝑧) = ⟨(𝐺𝑧), (2nd ‘(𝑅𝑧))⟩ ↔ (𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩))
11 fveq2 6646 . . 3 (𝑧 = suc 𝑣 → (𝑅𝑧) = (𝑅‘suc 𝑣))
12 fveq2 6646 . . . 4 (𝑧 = suc 𝑣 → (𝐺𝑧) = (𝐺‘suc 𝑣))
13 2fveq3 6651 . . . 4 (𝑧 = suc 𝑣 → (2nd ‘(𝑅𝑧)) = (2nd ‘(𝑅‘suc 𝑣)))
1412, 13opeq12d 4787 . . 3 (𝑧 = suc 𝑣 → ⟨(𝐺𝑧), (2nd ‘(𝑅𝑧))⟩ = ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩)
1511, 14eqeq12d 2836 . 2 (𝑧 = suc 𝑣 → ((𝑅𝑧) = ⟨(𝐺𝑧), (2nd ‘(𝑅𝑧))⟩ ↔ (𝑅‘suc 𝑣) = ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩))
16 fveq2 6646 . . 3 (𝑧 = 𝐵 → (𝑅𝑧) = (𝑅𝐵))
17 fveq2 6646 . . . 4 (𝑧 = 𝐵 → (𝐺𝑧) = (𝐺𝐵))
18 2fveq3 6651 . . . 4 (𝑧 = 𝐵 → (2nd ‘(𝑅𝑧)) = (2nd ‘(𝑅𝐵)))
1917, 18opeq12d 4787 . . 3 (𝑧 = 𝐵 → ⟨(𝐺𝑧), (2nd ‘(𝑅𝑧))⟩ = ⟨(𝐺𝐵), (2nd ‘(𝑅𝐵))⟩)
2016, 19eqeq12d 2836 . 2 (𝑧 = 𝐵 → ((𝑅𝑧) = ⟨(𝐺𝑧), (2nd ‘(𝑅𝑧))⟩ ↔ (𝑅𝐵) = ⟨(𝐺𝐵), (2nd ‘(𝑅𝐵))⟩))
21 uzrdg.2 . . . . 5 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)
2221fveq1i 6647 . . . 4 (𝑅‘∅) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘∅)
23 opex 5332 . . . . 5 𝐶, 𝐴⟩ ∈ V
24 fr0g 8049 . . . . 5 (⟨𝐶, 𝐴⟩ ∈ V → ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘∅) = ⟨𝐶, 𝐴⟩)
2523, 24ax-mp 5 . . . 4 ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘∅) = ⟨𝐶, 𝐴
2622, 25eqtri 2843 . . 3 (𝑅‘∅) = ⟨𝐶, 𝐴
27 om2uz.1 . . . . 5 𝐶 ∈ ℤ
28 om2uz.2 . . . . 5 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)
2927, 28om2uz0i 13299 . . . 4 (𝐺‘∅) = 𝐶
3026fveq2i 6649 . . . . 5 (2nd ‘(𝑅‘∅)) = (2nd ‘⟨𝐶, 𝐴⟩)
3127elexi 3492 . . . . . 6 𝐶 ∈ V
32 uzrdg.1 . . . . . 6 𝐴 ∈ V
3331, 32op2nd 7676 . . . . 5 (2nd ‘⟨𝐶, 𝐴⟩) = 𝐴
3430, 33eqtri 2843 . . . 4 (2nd ‘(𝑅‘∅)) = 𝐴
3529, 34opeq12i 4784 . . 3 ⟨(𝐺‘∅), (2nd ‘(𝑅‘∅))⟩ = ⟨𝐶, 𝐴
3626, 35eqtr4i 2846 . 2 (𝑅‘∅) = ⟨(𝐺‘∅), (2nd ‘(𝑅‘∅))⟩
37 frsuc 8050 . . . . . 6 (𝑣 ∈ ω → ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘𝑣)))
3821fveq1i 6647 . . . . . 6 (𝑅‘suc 𝑣) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘suc 𝑣)
3921fveq1i 6647 . . . . . . 7 (𝑅𝑣) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘𝑣)
4039fveq2i 6649 . . . . . 6 ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘(𝑅𝑣)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘𝑣))
4137, 38, 403eqtr4g 2880 . . . . 5 (𝑣 ∈ ω → (𝑅‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘(𝑅𝑣)))
42 fveq2 6646 . . . . . 6 ((𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩ → ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘(𝑅𝑣)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩))
43 df-ov 7136 . . . . . . 7 ((𝐺𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘(𝑅𝑣))) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩)
44 fvex 6659 . . . . . . . 8 (𝐺𝑣) ∈ V
45 fvex 6659 . . . . . . . 8 (2nd ‘(𝑅𝑣)) ∈ V
46 oveq1 7140 . . . . . . . . . 10 (𝑤 = (𝐺𝑣) → (𝑤 + 1) = ((𝐺𝑣) + 1))
47 oveq1 7140 . . . . . . . . . 10 (𝑤 = (𝐺𝑣) → (𝑤𝐹𝑧) = ((𝐺𝑣)𝐹𝑧))
4846, 47opeq12d 4787 . . . . . . . . 9 (𝑤 = (𝐺𝑣) → ⟨(𝑤 + 1), (𝑤𝐹𝑧)⟩ = ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹𝑧)⟩)
49 oveq2 7141 . . . . . . . . . 10 (𝑧 = (2nd ‘(𝑅𝑣)) → ((𝐺𝑣)𝐹𝑧) = ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣))))
5049opeq2d 4786 . . . . . . . . 9 (𝑧 = (2nd ‘(𝑅𝑣)) → ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹𝑧)⟩ = ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩)
51 oveq1 7140 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑥 + 1) = (𝑤 + 1))
52 oveq1 7140 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑥𝐹𝑦) = (𝑤𝐹𝑦))
5351, 52opeq12d 4787 . . . . . . . . . 10 (𝑥 = 𝑤 → ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩ = ⟨(𝑤 + 1), (𝑤𝐹𝑦)⟩)
54 oveq2 7141 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑤𝐹𝑦) = (𝑤𝐹𝑧))
5554opeq2d 4786 . . . . . . . . . 10 (𝑦 = 𝑧 → ⟨(𝑤 + 1), (𝑤𝐹𝑦)⟩ = ⟨(𝑤 + 1), (𝑤𝐹𝑧)⟩)
5653, 55cbvmpov 7226 . . . . . . . . 9 (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩) = (𝑤 ∈ V, 𝑧 ∈ V ↦ ⟨(𝑤 + 1), (𝑤𝐹𝑧)⟩)
57 opex 5332 . . . . . . . . 9 ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩ ∈ V
5848, 50, 56, 57ovmpo 7287 . . . . . . . 8 (((𝐺𝑣) ∈ V ∧ (2nd ‘(𝑅𝑣)) ∈ V) → ((𝐺𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘(𝑅𝑣))) = ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩)
5944, 45, 58mp2an 690 . . . . . . 7 ((𝐺𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘(𝑅𝑣))) = ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩
6043, 59eqtr3i 2845 . . . . . 6 ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩) = ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩
6142, 60syl6eq 2871 . . . . 5 ((𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩ → ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘(𝑅𝑣)) = ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩)
6241, 61sylan9eq 2875 . . . 4 ((𝑣 ∈ ω ∧ (𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩) → (𝑅‘suc 𝑣) = ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩)
6327, 28om2uzsuci 13300 . . . . . 6 (𝑣 ∈ ω → (𝐺‘suc 𝑣) = ((𝐺𝑣) + 1))
6463adantr 483 . . . . 5 ((𝑣 ∈ ω ∧ (𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩) → (𝐺‘suc 𝑣) = ((𝐺𝑣) + 1))
6562fveq2d 6650 . . . . . 6 ((𝑣 ∈ ω ∧ (𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩) → (2nd ‘(𝑅‘suc 𝑣)) = (2nd ‘⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩))
66 ovex 7166 . . . . . . 7 ((𝐺𝑣) + 1) ∈ V
67 ovex 7166 . . . . . . 7 ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣))) ∈ V
6866, 67op2nd 7676 . . . . . 6 (2nd ‘⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩) = ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))
6965, 68syl6eq 2871 . . . . 5 ((𝑣 ∈ ω ∧ (𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩) → (2nd ‘(𝑅‘suc 𝑣)) = ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣))))
7064, 69opeq12d 4787 . . . 4 ((𝑣 ∈ ω ∧ (𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩) → ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩ = ⟨((𝐺𝑣) + 1), ((𝐺𝑣)𝐹(2nd ‘(𝑅𝑣)))⟩)
7162, 70eqtr4d 2858 . . 3 ((𝑣 ∈ ω ∧ (𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩) → (𝑅‘suc 𝑣) = ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩)
7271ex 415 . 2 (𝑣 ∈ ω → ((𝑅𝑣) = ⟨(𝐺𝑣), (2nd ‘(𝑅𝑣))⟩ → (𝑅‘suc 𝑣) = ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩))
735, 10, 15, 20, 36, 72finds 7586 1 (𝐵 ∈ ω → (𝑅𝐵) = ⟨(𝐺𝐵), (2nd ‘(𝑅𝐵))⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1537  wcel 2114  Vcvv 3473  c0 4269  cop 4549  cmpt 5122  cres 5533  suc csuc 6169  cfv 6331  (class class class)co 7133  cmpo 7135  ωcom 7558  2nd c2nd 7666  reccrdg 8023  1c1 10516   + caddc 10518  cz 11960
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-2nd 7668  df-wrecs 7925  df-recs 7986  df-rdg 8024
This theorem is referenced by:  uzrdglem  13309  uzrdgfni  13310  uzrdgsuci  13312
  Copyright terms: Public domain W3C validator