Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  finxpreclem4 Structured version   Visualization version   GIF version

Theorem finxpreclem4 35721
Description: Lemma for ↑↑ recursion theorems. (Contributed by ML, 23-Oct-2020.)
Hypothesis
Ref Expression
finxpreclem4.1 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
Assertion
Ref Expression
finxpreclem4 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘ 𝑁))
Distinct variable groups:   𝑛,𝑁,𝑥   𝑈,𝑛,𝑥   𝑦,𝑛,𝑥
Allowed substitution hints:   𝑈(𝑦)   𝐹(𝑥,𝑦,𝑛)   𝑁(𝑦)

Proof of Theorem finxpreclem4
Dummy variable 𝑜 is distinct from all other variables.
StepHypRef Expression
1 2onn 8544 . . . . . . . 8 2o ∈ ω
2 nnon 7787 . . . . . . . . . . 11 (𝑁 ∈ ω → 𝑁 ∈ On)
3 2on 8382 . . . . . . . . . . . . . 14 2o ∈ On
4 oawordeu 8458 . . . . . . . . . . . . . 14 (((2o ∈ On ∧ 𝑁 ∈ On) ∧ 2o𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
53, 4mpanl1 697 . . . . . . . . . . . . 13 ((𝑁 ∈ On ∧ 2o𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
6 riotasbc 7313 . . . . . . . . . . . . 13 (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁[(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
75, 6syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ On ∧ 2o𝑁) → [(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
8 riotaex 7298 . . . . . . . . . . . . . 14 (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V
9 sbceq1g 4362 . . . . . . . . . . . . . 14 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V → ([(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜(2o +o 𝑜) = 𝑁))
108, 9ax-mp 5 . . . . . . . . . . . . 13 ([(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜(2o +o 𝑜) = 𝑁)
11 csbov2g 7384 . . . . . . . . . . . . . . . 16 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜(2o +o 𝑜) = (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜𝑜))
128, 11ax-mp 5 . . . . . . . . . . . . . . 15 (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜(2o +o 𝑜) = (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜𝑜)
138csbvargi 4380 . . . . . . . . . . . . . . . 16 (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜𝑜 = (𝑜 ∈ On (2o +o 𝑜) = 𝑁)
1413oveq2i 7349 . . . . . . . . . . . . . . 15 (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜𝑜) = (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))
1512, 14eqtri 2764 . . . . . . . . . . . . . 14 (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜(2o +o 𝑜) = (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))
1615eqeq1i 2741 . . . . . . . . . . . . 13 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜(2o +o 𝑜) = 𝑁 ↔ (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
1710, 16bitri 274 . . . . . . . . . . . 12 ([(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁 ↔ (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
187, 17sylib 217 . . . . . . . . . . 11 ((𝑁 ∈ On ∧ 2o𝑁) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
192, 18sylan 580 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 2o𝑁) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
20 simpl 483 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 ∈ ω)
2119, 20eqeltrd 2837 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 2o𝑁) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
22 riotacl 7312 . . . . . . . . . . 11 (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
23 riotaund 7334 . . . . . . . . . . . 12 (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) = ∅)
24 0elon 6356 . . . . . . . . . . . 12 ∅ ∈ On
2523, 24eqeltrdi 2845 . . . . . . . . . . 11 (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
2622, 25pm2.61i 182 . . . . . . . . . 10 (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On
27 nnarcl 8519 . . . . . . . . . . . 12 ((2o ∈ On ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On) → ((2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
283, 27mpan 687 . . . . . . . . . . 11 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On → ((2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
291biantrur 531 . . . . . . . . . . 11 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ↔ (2o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω))
3028, 29bitr4di 288 . . . . . . . . . 10 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On → ((2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω))
3126, 30ax-mp 5 . . . . . . . . 9 ((2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
3221, 31sylib 217 . . . . . . . 8 ((𝑁 ∈ ω ∧ 2o𝑁) → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
33 nnacom 8520 . . . . . . . 8 ((2o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
341, 32, 33sylancr 587 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
35 df-2o 8369 . . . . . . . . 9 2o = suc 1o
3635oveq2i 7349 . . . . . . . 8 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o)
37 1onn 8542 . . . . . . . . 9 1o ∈ ω
38 nnasuc 8509 . . . . . . . . 9 (((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
3932, 37, 38sylancl 586 . . . . . . . 8 ((𝑁 ∈ ω ∧ 2o𝑁) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
4036, 39eqtrid 2788 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
4134, 19, 403eqtr3d 2784 . . . . . 6 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 = suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
422adantr 481 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 ∈ On)
43 sucidg 6383 . . . . . . . . . . . 12 (1o ∈ ω → 1o ∈ suc 1o)
4437, 43ax-mp 5 . . . . . . . . . . 11 1o ∈ suc 1o
4544, 35eleqtrri 2836 . . . . . . . . . 10 1o ∈ 2o
46 ssel 3925 . . . . . . . . . 10 (2o𝑁 → (1o ∈ 2o → 1o𝑁))
4745, 46mpi 20 . . . . . . . . 9 (2o𝑁 → 1o𝑁)
4847ne0d 4283 . . . . . . . 8 (2o𝑁𝑁 ≠ ∅)
4948adantl 482 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 ≠ ∅)
50 nnlim 7795 . . . . . . . 8 (𝑁 ∈ ω → ¬ Lim 𝑁)
5150adantr 481 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → ¬ Lim 𝑁)
52 onsucuni3 35694 . . . . . . 7 ((𝑁 ∈ On ∧ 𝑁 ≠ ∅ ∧ ¬ Lim 𝑁) → 𝑁 = suc 𝑁)
5342, 49, 51, 52syl3anc 1370 . . . . . 6 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 = suc 𝑁)
54 nnacom 8520 . . . . . . . 8 (((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
5532, 37, 54sylancl 586 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
56 suceq 6368 . . . . . . 7 (((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) → suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = suc (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
5755, 56syl 17 . . . . . 6 ((𝑁 ∈ ω ∧ 2o𝑁) → suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = suc (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
5841, 53, 573eqtr3d 2784 . . . . 5 ((𝑁 ∈ ω ∧ 2o𝑁) → suc 𝑁 = suc (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
59 ordom 7791 . . . . . . . . 9 Ord ω
60 ordelss 6319 . . . . . . . . 9 ((Ord ω ∧ 𝑁 ∈ ω) → 𝑁 ⊆ ω)
6159, 60mpan 687 . . . . . . . 8 (𝑁 ∈ ω → 𝑁 ⊆ ω)
62 nnfi 9033 . . . . . . . 8 (𝑁 ∈ ω → 𝑁 ∈ Fin)
63 nnunifi 9160 . . . . . . . 8 ((𝑁 ⊆ ω ∧ 𝑁 ∈ Fin) → 𝑁 ∈ ω)
6461, 62, 63syl2anc 584 . . . . . . 7 (𝑁 ∈ ω → 𝑁 ∈ ω)
6564adantr 481 . . . . . 6 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 ∈ ω)
66 nnacl 8514 . . . . . . 7 ((1o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
6737, 32, 66sylancr 587 . . . . . 6 ((𝑁 ∈ ω ∧ 2o𝑁) → (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
68 peano4 7808 . . . . . 6 (( 𝑁 ∈ ω ∧ (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω) → (suc 𝑁 = suc (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ 𝑁 = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
6965, 67, 68syl2anc 584 . . . . 5 ((𝑁 ∈ ω ∧ 2o𝑁) → (suc 𝑁 = suc (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ 𝑁 = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
7058, 69mpbid 231 . . . 4 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
7170fveq2d 6830 . . 3 ((𝑁 ∈ ω ∧ 2o𝑁) → (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘ 𝑁) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘(1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
7271adantr 481 . 2 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘ 𝑁) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘(1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
7332adantr 481 . . 3 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
74 df-1o 8368 . . . . . . . 8 1o = suc ∅
7574fveq2i 6829 . . . . . . 7 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅)
76 rdgsuc 8326 . . . . . . . 8 (∅ ∈ On → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)))
7724, 76ax-mp 5 . . . . . . 7 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅))
78 opex 5410 . . . . . . . . 9 𝑁, 𝑦⟩ ∈ V
7978rdg0 8323 . . . . . . . 8 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅) = ⟨𝑁, 𝑦
8079fveq2i 6829 . . . . . . 7 (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)) = (𝐹‘⟨𝑁, 𝑦⟩)
8175, 77, 803eqtri 2768 . . . . . 6 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (𝐹‘⟨𝑁, 𝑦⟩)
82 finxpreclem4.1 . . . . . . 7 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
8382finxpreclem3 35720 . . . . . 6 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → ⟨ 𝑁, (1st𝑦)⟩ = (𝐹‘⟨𝑁, 𝑦⟩))
8481, 83eqtr4id 2795 . . . . 5 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = ⟨ 𝑁, (1st𝑦)⟩)
8584fveq2d 6830 . . . 4 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘⟨ 𝑁, (1st𝑦)⟩))
86 2on0 8384 . . . . . 6 2o ≠ ∅
87 nnlim 7795 . . . . . . 7 (2o ∈ ω → ¬ Lim 2o)
881, 87ax-mp 5 . . . . . 6 ¬ Lim 2o
89 rdgsucuni 35696 . . . . . 6 ((2o ∈ On ∧ 2o ≠ ∅ ∧ ¬ Lim 2o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘ 2o)))
903, 86, 88, 89mp3an 1460 . . . . 5 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘ 2o))
91 1oequni2o 35695 . . . . . . 7 1o = 2o
9291fveq2i 6829 . . . . . 6 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘ 2o)
9392fveq2i 6829 . . . . 5 (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘ 2o))
9490, 93eqtr4i 2767 . . . 4 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o))
9574fveq2i 6829 . . . . 5 (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘1o) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘suc ∅)
96 rdgsuc 8326 . . . . . 6 (∅ ∈ On → (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘∅)))
9724, 96ax-mp 5 . . . . 5 (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘∅))
98 opex 5410 . . . . . . 7 𝑁, (1st𝑦)⟩ ∈ V
9998rdg0 8323 . . . . . 6 (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘∅) = ⟨ 𝑁, (1st𝑦)⟩
10099fveq2i 6829 . . . . 5 (𝐹‘(rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘∅)) = (𝐹‘⟨ 𝑁, (1st𝑦)⟩)
10195, 97, 1003eqtri 2768 . . . 4 (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘1o) = (𝐹‘⟨ 𝑁, (1st𝑦)⟩)
10285, 94, 1013eqtr4g 2801 . . 3 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘1o))
103 1on 8380 . . . 4 1o ∈ On
104 rdgeqoa 35697 . . . 4 ((2o ∈ On ∧ 1o ∈ On ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → ((rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘1o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘(1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))))
1053, 103, 104mp3an12 1450 . . 3 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω → ((rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘1o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘(1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))))
10673, 102, 105sylc 65 . 2 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘(1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
10719fveq2d 6830 . . 3 ((𝑁 ∈ ω ∧ 2o𝑁) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
108107adantr 481 . 2 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
10972, 106, 1083eqtr2rd 2783 1 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘ 𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wne 2940  ∃!wreu 3347  Vcvv 3441  [wsbc 3727  csb 3843  wss 3898  c0 4270  ifcif 4474  cop 4580   cuni 4853   × cxp 5619  Ord word 6302  Oncon0 6303  Lim wlim 6304  suc csuc 6305  cfv 6480  crio 7293  (class class class)co 7338  cmpo 7340  ωcom 7781  1st c1st 7898  reccrdg 8311  1oc1o 8361  2oc2o 8362   +o coa 8365  Fincfn 8805
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pr 5373  ax-un 7651
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-om 7782  df-2nd 7901  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-2o 8369  df-oadd 8372  df-en 8806  df-fin 8809
This theorem is referenced by:  finxpsuclem  35724
  Copyright terms: Public domain W3C validator