Theorem frecsuc 6186

Description: The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 31-Mar-2022.)

Assertion

Ref	Expression
frecsuc	⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))

Distinct variable groups:   𝑧,𝐹   𝑧,𝑆

Allowed substitution hints:   𝐴(𝑧)   𝐵(𝑧)

Proof of Theorem frecsuc

Dummy variables 𝑓 𝑔 𝑚 𝑥 𝑦 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmeq 4649	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔)
2	1	eqeq1d 2097	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → (dom 𝑓 = suc 𝑛 ↔ dom 𝑔 = suc 𝑛))
3		fveq1 5317	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑛) = (𝑔‘𝑛))
4	3	fveq2d 5322	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹‘(𝑓‘𝑛)) = (𝐹‘(𝑔‘𝑛)))
5	4	eleq2d 2158	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → (𝑦 ∈ (𝐹‘(𝑓‘𝑛)) ↔ 𝑦 ∈ (𝐹‘(𝑔‘𝑛))))
6	2, 5	anbi12d 458	. . . . . . 7 ⊢ (𝑓 = 𝑔 → ((dom 𝑓 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑛))) ↔ (dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛)))))
7	6	rexbidv 2382	. . . . . 6 ⊢ (𝑓 = 𝑔 → (∃𝑛 ∈ ω (dom 𝑓 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑛))) ↔ ∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛)))))
8	1	eqeq1d 2097	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (dom 𝑓 = ∅ ↔ dom 𝑔 = ∅))
9	8	anbi1d 454	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴) ↔ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴)))
10	7, 9	orbi12d 743	. . . . 5 ⊢ (𝑓 = 𝑔 → ((∃𝑛 ∈ ω (dom 𝑓 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑛))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴)) ↔ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴))))
11	10	abbidv 2206	. . . 4 ⊢ (𝑓 = 𝑔 → {𝑦 ∣ (∃𝑛 ∈ ω (dom 𝑓 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑛))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴))} = {𝑦 ∣ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴))})
12	11	cbvmptv 3940	. . 3 ⊢ (𝑓 ∈ V ↦ {𝑦 ∣ (∃𝑛 ∈ ω (dom 𝑓 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑛))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴))}) = (𝑔 ∈ V ↦ {𝑦 ∣ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴))})
13		eleq1 2151	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (𝐹‘(𝑔‘𝑛)) ↔ 𝑥 ∈ (𝐹‘(𝑔‘𝑛))))
14	13	anbi2d 453	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛))) ↔ (dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛)))))
15	14	rexbidv 2382	. . . . . 6 ⊢ (𝑦 = 𝑥 → (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛))) ↔ ∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛)))))
16		eleq1 2151	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
17	16	anbi2d 453	. . . . . 6 ⊢ (𝑦 = 𝑥 → ((dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴) ↔ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)))
18	15, 17	orbi12d 743	. . . . 5 ⊢ (𝑦 = 𝑥 → ((∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴)) ↔ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))))
19	18	cbvabv 2212	. . . 4 ⊢ {𝑦 ∣ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴))} = {𝑥 ∣ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}
20	19	mpteq2i 3931	. . 3 ⊢ (𝑔 ∈ V ↦ {𝑦 ∣ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴))}) = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})
21		suceq 4238	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → suc 𝑛 = suc 𝑚)
22	21	eqeq2d 2100	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (dom 𝑔 = suc 𝑛 ↔ dom 𝑔 = suc 𝑚))
23		fveq2 5318	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
24	23	fveq2d 5322	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝐹‘(𝑔‘𝑛)) = (𝐹‘(𝑔‘𝑚)))
25	24	eleq2d 2158	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑥 ∈ (𝐹‘(𝑔‘𝑛)) ↔ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))))
26	22, 25	anbi12d 458	. . . . . . 7 ⊢ (𝑛 = 𝑚 → ((dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛))) ↔ (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚)))))
27	26	cbvrexv 2592	. . . . . 6 ⊢ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛))) ↔ ∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))))
28	27	orbi1i 716	. . . . 5 ⊢ ((∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)))
29	28	abbii 2204	. . . 4 ⊢ {𝑥 ∣ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}
30	29	mpteq2i 3931	. . 3 ⊢ (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑛 ∈ ω (dom 𝑔 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑛))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})
31	12, 20, 30	3eqtri 2113	. 2 ⊢ (𝑓 ∈ V ↦ {𝑦 ∣ (∃𝑛 ∈ ω (dom 𝑓 = suc 𝑛 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑛))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴))}) = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})
32	31	frecsuclem 6185	1 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 665   ∧ w3a 925   = wceq 1290   ∈ wcel 1439  {cab 2075  ∀wral 2360  ∃wrex 2361  Vcvv 2620  ∅c0 3287   ↦ cmpt 3905  suc csuc 4201  ωcom 4418  dom cdm 4451  ‘cfv 5028  freccfrec 6169

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-coll 3960  ax-sep 3963  ax-nul 3971  ax-pow 4015  ax-pr 4045  ax-un 4269  ax-setind 4366  ax-iinf 4416

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2622  df-sbc 2842  df-csb 2935  df-dif 3002  df-un 3004  df-in 3006  df-ss 3013  df-nul 3288  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-int 3695  df-iun 3738  df-br 3852  df-opab 3906  df-mpt 3907  df-tr 3943  df-id 4129  df-iord 4202  df-on 4204  df-ilim 4205  df-suc 4207  df-iom 4419  df-xp 4457  df-rel 4458  df-cnv 4459  df-co 4460  df-dm 4461  df-rn 4462  df-res 4463  df-ima 4464  df-iota 4993  df-fun 5030  df-fn 5031  df-f 5032  df-f1 5033  df-fo 5034  df-f1o 5035  df-fv 5036  df-recs 6084  df-frec 6170

This theorem is referenced by:  frecrdg  6187  frec2uzsucd  9862  frec2uzrdg  9870  frecuzrdgsuc  9875  frecuzrdgg  9877  frecuzrdgsuctlem  9884  iseqvalt  9927  seq3val  9928