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

Theorem frecsuclem3 5990
 Description: Lemma for frecsuc 5991. (Contributed by Jim Kingdon, 15-Aug-2019.)
Hypothesis
Ref Expression
frecsuclem1.h 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
Assertion
Ref Expression
frecsuclem3 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
Distinct variable groups:   𝐴,𝑔,𝑚,𝑥,𝑧   𝐵,𝑔,𝑚,𝑥,𝑧   𝑔,𝐹,𝑚,𝑥,𝑧   𝑔,𝐺,𝑚,𝑥,𝑧   𝑔,𝑉,𝑚,𝑥
Allowed substitution hint:   𝑉(𝑧)

Proof of Theorem frecsuclem3
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eqid 2040 . . . . . . . . . . . . 13 recs(𝐺) = recs(𝐺)
2 frecsuclem1.h . . . . . . . . . . . . . 14 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
32frectfr 5985 . . . . . . . . . . . . 13 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉) → ∀𝑦(Fun 𝐺 ∧ (𝐺𝑦) ∈ V))
41, 3tfri1d 5949 . . . . . . . . . . . 12 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉) → recs(𝐺) Fn On)
5 fnfun 4996 . . . . . . . . . . . 12 (recs(𝐺) Fn On → Fun recs(𝐺))
64, 5syl 14 . . . . . . . . . . 11 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉) → Fun recs(𝐺))
763adant3 924 . . . . . . . . . 10 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → Fun recs(𝐺))
8 peano2 4318 . . . . . . . . . . 11 (𝐵 ∈ ω → suc 𝐵 ∈ ω)
983ad2ant3 927 . . . . . . . . . 10 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → suc 𝐵 ∈ ω)
10 resfunexg 5382 . . . . . . . . . 10 ((Fun recs(𝐺) ∧ suc 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
117, 9, 10syl2anc 391 . . . . . . . . 9 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
12 simp1 904 . . . . . . . . 9 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → ∀𝑧(𝐹𝑧) ∈ V)
13 simp2 905 . . . . . . . . 9 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → 𝐴𝑉)
1411, 12, 13frecabex 5984 . . . . . . . 8 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ V)
15 dmeq 4535 . . . . . . . . . . . . . . . . 17 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵))
1615eqeq1d 2048 . . . . . . . . . . . . . . . 16 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚))
17 fveq1 5177 . . . . . . . . . . . . . . . . . 18 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚))
1817fveq2d 5182 . . . . . . . . . . . . . . . . 17 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝐹‘(𝑔𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))
1918eleq2d 2107 . . . . . . . . . . . . . . . 16 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))
2016, 19anbi12d 442 . . . . . . . . . . . . . . 15 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
2120rexbidv 2327 . . . . . . . . . . . . . 14 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
2215eqeq1d 2048 . . . . . . . . . . . . . . 15 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = ∅ ↔ dom (recs(𝐺) ↾ suc 𝐵) = ∅))
2322anbi1d 438 . . . . . . . . . . . . . 14 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴)))
2421, 23orbi12d 707 . . . . . . . . . . . . 13 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
2524abbidv 2155 . . . . . . . . . . . 12 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
2625, 2fvmptg 5248 . . . . . . . . . . 11 (((recs(𝐺) ↾ suc 𝐵) ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ V) → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
2726ex 108 . . . . . . . . . 10 ((recs(𝐺) ↾ suc 𝐵) ∈ V → ({𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ V → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))}))
2811, 27syl 14 . . . . . . . . 9 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → ({𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ V → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))}))
292frecsuclem1 5987 . . . . . . . . . 10 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
3029eqeq1d 2048 . . . . . . . . 9 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → ((frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ↔ (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))}))
3128, 30sylibrd 158 . . . . . . . 8 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → ({𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ V → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))}))
3214, 31mpd 13 . . . . . . 7 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
3332abeq2d 2150 . . . . . 6 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
342frecsuclemdm 5988 . . . . . . . . . . 11 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
35 peano3 4319 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ≠ ∅)
36353ad2ant3 927 . . . . . . . . . . 11 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → suc 𝐵 ≠ ∅)
3734, 36eqnetrd 2229 . . . . . . . . . 10 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) ≠ ∅)
3837neneqd 2226 . . . . . . . . 9 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → ¬ dom (recs(𝐺) ↾ suc 𝐵) = ∅)
3938intnanrd 841 . . . . . . . 8 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → ¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))
40 biorf 663 . . . . . . . 8 (¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))))
4139, 40syl 14 . . . . . . 7 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))))
42 orcom 647 . . . . . . 7 (((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴)))
4341, 42syl6bb 185 . . . . . 6 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
4434eqeq1d 2048 . . . . . . . . . 10 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ suc 𝐵 = suc 𝑚))
45 vex 2560 . . . . . . . . . . . 12 𝑚 ∈ V
46 suc11g 4281 . . . . . . . . . . . 12 ((𝐵 ∈ ω ∧ 𝑚 ∈ V) → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
4745, 46mpan2 401 . . . . . . . . . . 11 (𝐵 ∈ ω → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
48473ad2ant3 927 . . . . . . . . . 10 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
4944, 48bitrd 177 . . . . . . . . 9 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝐵 = 𝑚))
50 eqcom 2042 . . . . . . . . 9 (𝐵 = 𝑚𝑚 = 𝐵)
5149, 50syl6bb 185 . . . . . . . 8 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑚 = 𝐵))
5251anbi1d 438 . . . . . . 7 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → ((dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
5352rexbidv 2327 . . . . . 6 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
5433, 43, 533bitr2d 205 . . . . 5 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
55 fveq2 5178 . . . . . . . 8 (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵))
5655fveq2d 5182 . . . . . . 7 (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
5756eleq2d 2107 . . . . . 6 (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
5857ceqsrexbv 2675 . . . . 5 (∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
5954, 58syl6bb 185 . . . 4 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))))
60593anibar 1072 . . 3 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
6160eqrdv 2038 . 2 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
622frecsuclem2 5989 . . 3 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
6362fveq2d 5182 . 2 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
6461, 63eqtrd 2072 1 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 629   ∧ w3a 885  ∀wal 1241   = wceq 1243   ∈ wcel 1393  {cab 2026   ≠ wne 2204  ∃wrex 2307  Vcvv 2557  ∅c0 3224   ↦ cmpt 3818  Oncon0 4100  suc csuc 4102  ωcom 4313  dom cdm 4345   ↾ cres 4347  Fun wfun 4896   Fn wfn 4897  ‘cfv 4902  recscrecs 5919  freccfrec 5977 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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311 This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-id 4030  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-recs 5920  df-frec 5978 This theorem is referenced by:  frecsuc  5991
 Copyright terms: Public domain W3C validator