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

Theorem finxpreclem4 34812
 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 8253 . . . . . . . 8 2o ∈ ω
2 nnon 7570 . . . . . . . . . . 11 (𝑁 ∈ ω → 𝑁 ∈ On)
3 2on 8098 . . . . . . . . . . . . . 14 2o ∈ On
4 oawordeu 8168 . . . . . . . . . . . . . 14 (((2o ∈ On ∧ 𝑁 ∈ On) ∧ 2o𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
53, 4mpanl1 699 . . . . . . . . . . . . 13 ((𝑁 ∈ On ∧ 2o𝑁) → ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁)
6 riotasbc 7115 . . . . . . . . . . . . 13 (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁[(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
75, 6syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ On ∧ 2o𝑁) → [(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁)
8 riotaex 7101 . . . . . . . . . . . . . 14 (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ V
9 sbceq1g 4325 . . . . . . . . . . . . . 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 7185 . . . . . . . . . . . . . . . 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 4343 . . . . . . . . . . . . . . . 16 (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜𝑜 = (𝑜 ∈ On (2o +o 𝑜) = 𝑁)
1413oveq2i 7150 . . . . . . . . . . . . . . 15 (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜𝑜) = (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))
1512, 14eqtri 2824 . . . . . . . . . . . . . 14 (𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜(2o +o 𝑜) = (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))
1615eqeq1i 2806 . . . . . . . . . . . . 13 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜(2o +o 𝑜) = 𝑁 ↔ (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
1710, 16bitri 278 . . . . . . . . . . . 12 ([(𝑜 ∈ On (2o +o 𝑜) = 𝑁) / 𝑜](2o +o 𝑜) = 𝑁 ↔ (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
187, 17sylib 221 . . . . . . . . . . 11 ((𝑁 ∈ On ∧ 2o𝑁) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
192, 18sylan 583 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 2o𝑁) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = 𝑁)
20 simpl 486 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 ∈ ω)
2119, 20eqeltrd 2893 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 2o𝑁) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
22 riotacl 7114 . . . . . . . . . . 11 (∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
23 riotaund 7136 . . . . . . . . . . . 12 (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) = ∅)
24 0elon 6216 . . . . . . . . . . . 12 ∅ ∈ On
2523, 24eqeltrdi 2901 . . . . . . . . . . 11 (¬ ∃!𝑜 ∈ On (2o +o 𝑜) = 𝑁 → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On)
2622, 25pm2.61i 185 . . . . . . . . . 10 (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On
27 nnarcl 8229 . . . . . . . . . . . 12 ((2o ∈ On ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On) → ((2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
283, 27mpan 689 . . . . . . . . . . 11 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ On → ((2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω ↔ (2o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)))
291biantrur 534 . . . . . . . . . . 11 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ↔ (2o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω))
3028, 29syl6bbr 292 . . . . . . . . . 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 221 . . . . . . . 8 ((𝑁 ∈ ω ∧ 2o𝑁) → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
33 nnacom 8230 . . . . . . . 8 ((2o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
341, 32, 33sylancr 590 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → (2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) = ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o))
35 df-2o 8090 . . . . . . . . 9 2o = suc 1o
3635oveq2i 7150 . . . . . . . 8 ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o)
37 1onn 8252 . . . . . . . . 9 1o ∈ ω
38 nnasuc 8219 . . . . . . . . 9 (((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
3932, 37, 38sylancl 589 . . . . . . . 8 ((𝑁 ∈ ω ∧ 2o𝑁) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o suc 1o) = suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
4036, 39syl5eq 2848 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 2o) = suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
4134, 19, 403eqtr3d 2844 . . . . . 6 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 = suc ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o))
422adantr 484 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 ∈ On)
43 sucidg 6241 . . . . . . . . . . . 12 (1o ∈ ω → 1o ∈ suc 1o)
4437, 43ax-mp 5 . . . . . . . . . . 11 1o ∈ suc 1o
4544, 35eleqtrri 2892 . . . . . . . . . 10 1o ∈ 2o
46 ssel 3911 . . . . . . . . . 10 (2o𝑁 → (1o ∈ 2o → 1o𝑁))
4745, 46mpi 20 . . . . . . . . 9 (2o𝑁 → 1o𝑁)
4847ne0d 4254 . . . . . . . 8 (2o𝑁𝑁 ≠ ∅)
4948adantl 485 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 ≠ ∅)
50 nnlim 7577 . . . . . . . 8 (𝑁 ∈ ω → ¬ Lim 𝑁)
5150adantr 484 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → ¬ Lim 𝑁)
52 onsucuni3 34785 . . . . . . 7 ((𝑁 ∈ On ∧ 𝑁 ≠ ∅ ∧ ¬ Lim 𝑁) → 𝑁 = suc 𝑁)
5342, 49, 51, 52syl3anc 1368 . . . . . 6 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 = suc 𝑁)
54 nnacom 8230 . . . . . . . 8 (((𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω ∧ 1o ∈ ω) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
5532, 37, 54sylancl 589 . . . . . . 7 ((𝑁 ∈ ω ∧ 2o𝑁) → ((𝑜 ∈ On (2o +o 𝑜) = 𝑁) +o 1o) = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
56 suceq 6228 . . . . . . 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 2844 . . . . 5 ((𝑁 ∈ ω ∧ 2o𝑁) → suc 𝑁 = suc (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
59 ordom 7573 . . . . . . . . 9 Ord ω
60 ordelss 6179 . . . . . . . . 9 ((Ord ω ∧ 𝑁 ∈ ω) → 𝑁 ⊆ ω)
6159, 60mpan 689 . . . . . . . 8 (𝑁 ∈ ω → 𝑁 ⊆ ω)
62 nnfi 8700 . . . . . . . 8 (𝑁 ∈ ω → 𝑁 ∈ Fin)
63 nnunifi 8757 . . . . . . . 8 ((𝑁 ⊆ ω ∧ 𝑁 ∈ Fin) → 𝑁 ∈ ω)
6461, 62, 63syl2anc 587 . . . . . . 7 (𝑁 ∈ ω → 𝑁 ∈ ω)
6564adantr 484 . . . . . 6 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 ∈ ω)
66 nnacl 8224 . . . . . . 7 ((1o ∈ ω ∧ (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω) → (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
6737, 32, 66sylancr 590 . . . . . 6 ((𝑁 ∈ ω ∧ 2o𝑁) → (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω)
68 peano4 7588 . . . . . 6 (( 𝑁 ∈ ω ∧ (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ∈ ω) → (suc 𝑁 = suc (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ 𝑁 = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
6965, 67, 68syl2anc 587 . . . . 5 ((𝑁 ∈ ω ∧ 2o𝑁) → (suc 𝑁 = suc (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)) ↔ 𝑁 = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
7058, 69mpbid 235 . . . 4 ((𝑁 ∈ ω ∧ 2o𝑁) → 𝑁 = (1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁)))
7170fveq2d 6653 . . 3 ((𝑁 ∈ ω ∧ 2o𝑁) → (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘ 𝑁) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘(1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
7271adantr 484 . 2 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘ 𝑁) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘(1o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))))
7332adantr 484 . . 3 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝑜 ∈ On (2o +o 𝑜) = 𝑁) ∈ ω)
74 df-1o 8089 . . . . . . . 8 1o = suc ∅
7574fveq2i 6652 . . . . . . 7 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅)
76 rdgsuc 8047 . . . . . . . 8 (∅ ∈ On → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)))
7724, 76ax-mp 5 . . . . . . 7 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅))
78 opex 5324 . . . . . . . . 9 𝑁, 𝑦⟩ ∈ V
7978rdg0 8044 . . . . . . . 8 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅) = ⟨𝑁, 𝑦
8079fveq2i 6652 . . . . . . 7 (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘∅)) = (𝐹‘⟨𝑁, 𝑦⟩)
8175, 77, 803eqtri 2828 . . . . . 6 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (𝐹‘⟨𝑁, 𝑦⟩)
82 finxpreclem4.1 . . . . . . 7 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
8382finxpreclem3 34811 . . . . . 6 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → ⟨ 𝑁, (1st𝑦)⟩ = (𝐹‘⟨𝑁, 𝑦⟩))
8481, 83eqtr4id 2855 . . . . 5 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = ⟨ 𝑁, (1st𝑦)⟩)
8584fveq2d 6653 . . . 4 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘⟨ 𝑁, (1st𝑦)⟩))
86 2on0 8100 . . . . . 6 2o ≠ ∅
87 nnlim 7577 . . . . . . 7 (2o ∈ ω → ¬ Lim 2o)
881, 87ax-mp 5 . . . . . 6 ¬ Lim 2o
89 rdgsucuni 34787 . . . . . 6 ((2o ∈ On ∧ 2o ≠ ∅ ∧ ¬ Lim 2o) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘ 2o)))
903, 86, 88, 89mp3an 1458 . . . . 5 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘ 2o))
91 1oequni2o 34786 . . . . . . 7 1o = 2o
9291fveq2i 6652 . . . . . 6 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘ 2o)
9392fveq2i 6652 . . . . 5 (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o)) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘ 2o))
9490, 93eqtr4i 2827 . . . 4 (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (𝐹‘(rec(𝐹, ⟨𝑁, 𝑦⟩)‘1o))
9574fveq2i 6652 . . . . 5 (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘1o) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘suc ∅)
96 rdgsuc 8047 . . . . . 6 (∅ ∈ On → (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘∅)))
9724, 96ax-mp 5 . . . . 5 (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘suc ∅) = (𝐹‘(rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘∅))
98 opex 5324 . . . . . . 7 𝑁, (1st𝑦)⟩ ∈ V
9998rdg0 8044 . . . . . 6 (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘∅) = ⟨ 𝑁, (1st𝑦)⟩
10099fveq2i 6652 . . . . 5 (𝐹‘(rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘∅)) = (𝐹‘⟨ 𝑁, (1st𝑦)⟩)
10195, 97, 1003eqtri 2828 . . . 4 (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘1o) = (𝐹‘⟨ 𝑁, (1st𝑦)⟩)
10285, 94, 1013eqtr4g 2861 . . 3 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘2o) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘1o))
103 1on 8096 . . . 4 1o ∈ On
104 rdgeqoa 34788 . . . 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 1448 . . 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 6653 . . 3 ((𝑁 ∈ ω ∧ 2o𝑁) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
108107adantr 484 . 2 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘(2o +o (𝑜 ∈ On (2o +o 𝑜) = 𝑁))) = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))
10972, 106, 1083eqtr2rd 2843 1 (((𝑁 ∈ ω ∧ 2o𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨ 𝑁, (1st𝑦)⟩)‘ 𝑁))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2112   ≠ wne 2990  ∃!wreu 3111  Vcvv 3444  [wsbc 3723  ⦋csb 3831   ⊆ wss 3884  ∅c0 4246  ifcif 4428  ⟨cop 4534  ∪ cuni 4803   × cxp 5521  Ord word 6162  Oncon0 6163  Lim wlim 6164  suc csuc 6165  ‘cfv 6328  ℩crio 7096  (class class class)co 7139   ∈ cmpo 7141  ωcom 7564  1st c1st 7673  reccrdg 8032  1oc1o 8082  2oc2o 8083   +o coa 8086  Fincfn 8496 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500 This theorem is referenced by:  finxpsuclem  34815
 Copyright terms: Public domain W3C validator