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

Theorem frecsuclem 6406
Description: Lemma for frecsuc 6407. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 29-Mar-2022.)
Hypothesis
Ref Expression
frecsuclem.g 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
Assertion
Ref Expression
frecsuclem ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
Distinct variable groups:   𝐴,𝑔,𝑚,𝑥   𝐵,𝑔,𝑚,𝑥   𝑔,𝐹,𝑚,𝑥   𝑧,𝐹,𝑚,𝑥   𝑔,𝐺,𝑚,𝑥   𝑆,𝑚,𝑥,𝑧
Allowed substitution hints:   𝐴(𝑧)   𝐵(𝑧)   𝑆(𝑔)   𝐺(𝑧)

Proof of Theorem frecsuclem
Dummy variables 𝑓 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-frec 6391 . . . . . . . . . . . . 13 frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
2 frecsuclem.g . . . . . . . . . . . . . . 15 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
3 recseq 6306 . . . . . . . . . . . . . . 15 (𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) → recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})))
42, 3ax-mp 5 . . . . . . . . . . . . . 14 recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
54reseq1i 4903 . . . . . . . . . . . . 13 (recs(𝐺) ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
61, 5eqtr4i 2201 . . . . . . . . . . . 12 frec(𝐹, 𝐴) = (recs(𝐺) ↾ ω)
76fveq1i 5516 . . . . . . . . . . 11 (frec(𝐹, 𝐴)‘suc 𝐵) = ((recs(𝐺) ↾ ω)‘suc 𝐵)
8 peano2 4594 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ∈ ω)
9 fvres 5539 . . . . . . . . . . . 12 (suc 𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
108, 9syl 14 . . . . . . . . . . 11 (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
117, 10eqtrid 2222 . . . . . . . . . 10 (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
12113ad2ant3 1020 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
13 eqid 2177 . . . . . . . . . . 11 recs(𝐺) = recs(𝐺)
142funmpt2 5255 . . . . . . . . . . . 12 Fun 𝐺
1514a1i 9 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Fun 𝐺)
16 ordom 4606 . . . . . . . . . . . 12 Ord ω
1716a1i 9 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Ord ω)
18 vex 2740 . . . . . . . . . . . . . 14 𝑓 ∈ V
1918a1i 9 . . . . . . . . . . . . 13 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓 ∈ V)
20 simp2 998 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑦 ∈ ω)
21 simp3 999 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓:𝑦𝑆)
22 simp11 1027 . . . . . . . . . . . . . . 15 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
23 fveq2 5515 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
2423eleq1d 2246 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → ((𝐹𝑧) ∈ 𝑆 ↔ (𝐹𝑤) ∈ 𝑆))
2524cbvralv 2703 . . . . . . . . . . . . . . 15 (∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆 ↔ ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
2622, 25sylib 122 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
27 simp12 1028 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝐴𝑆)
2820, 21, 26, 27frecabcl 6399 . . . . . . . . . . . . 13 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
29 dmeq 4827 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
3029eqeq1d 2186 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚))
31 fveq1 5514 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔𝑚) = (𝑓𝑚))
3231fveq2d 5519 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → (𝐹‘(𝑔𝑚)) = (𝐹‘(𝑓𝑚)))
3332eleq2d 2247 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝑓𝑚))))
3430, 33anbi12d 473 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑓 → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
3534rexbidv 2478 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑓 → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
3629eqeq1d 2186 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑓 → (dom 𝑔 = ∅ ↔ dom 𝑓 = ∅))
3736anbi1d 465 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑓 → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑥𝐴)))
3835, 37orbi12d 793 . . . . . . . . . . . . . . 15 (𝑔 = 𝑓 → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))))
3938abbidv 2295 . . . . . . . . . . . . . 14 (𝑔 = 𝑓 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4039, 2fvmptg 5592 . . . . . . . . . . . . 13 ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆) → (𝐺𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4119, 28, 40syl2anc 411 . . . . . . . . . . . 12 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → (𝐺𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4241, 28eqeltrd 2254 . . . . . . . . . . 11 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → (𝐺𝑓) ∈ 𝑆)
43 limom 4613 . . . . . . . . . . . . . . 15 Lim ω
44 limuni 4396 . . . . . . . . . . . . . . 15 (Lim ω → ω = ω)
4543, 44ax-mp 5 . . . . . . . . . . . . . 14 ω = ω
4645eleq2i 2244 . . . . . . . . . . . . 13 (𝑦 ∈ ω ↔ 𝑦 ω)
47 peano2 4594 . . . . . . . . . . . . 13 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
4846, 47sylbir 135 . . . . . . . . . . . 12 (𝑦 ω → suc 𝑦 ∈ ω)
4948adantl 277 . . . . . . . . . . 11 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ω) → suc 𝑦 ∈ ω)
5045eleq2i 2244 . . . . . . . . . . . . 13 (suc 𝐵 ∈ ω ↔ suc 𝐵 ω)
518, 50sylib 122 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ω)
52513ad2ant3 1020 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ω)
5313, 15, 17, 42, 49, 52tfrcldm 6363 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ∈ dom recs(𝐺))
5413tfr2a 6321 . . . . . . . . . 10 (suc 𝐵 ∈ dom recs(𝐺) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
5553, 54syl 14 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
5612, 55eqtrd 2210 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
57 tfrfun 6320 . . . . . . . . . . 11 Fun recs(𝐺)
5857a1i 9 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Fun recs(𝐺))
5983ad2ant3 1020 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ∈ ω)
60 resfunexg 5737 . . . . . . . . . 10 ((Fun recs(𝐺) ∧ suc 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
6158, 59, 60syl2anc 411 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
62 frecfcl 6405 . . . . . . . . . . . . 13 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → frec(𝐹, 𝐴):ω⟶𝑆)
636feq1i 5358 . . . . . . . . . . . . 13 (frec(𝐹, 𝐴):ω⟶𝑆 ↔ (recs(𝐺) ↾ ω):ω⟶𝑆)
6462, 63sylib 122 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → (recs(𝐺) ↾ ω):ω⟶𝑆)
65643adant3 1017 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ ω):ω⟶𝑆)
66 simp3 999 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → 𝐵 ∈ ω)
67 ordelsuc 4504 . . . . . . . . . . . . . 14 ((𝐵 ∈ ω ∧ Ord ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
6816, 67mpan2 425 . . . . . . . . . . . . 13 (𝐵 ∈ ω → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
69683ad2ant3 1020 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
7066, 69mpbid 147 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ⊆ ω)
71 fssres2 5393 . . . . . . . . . . 11 (((recs(𝐺) ↾ ω):ω⟶𝑆 ∧ suc 𝐵 ⊆ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆)
7265, 70, 71syl2anc 411 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆)
73 simp1 997 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
7473, 25sylib 122 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
75 simp2 998 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → 𝐴𝑆)
7659, 72, 74, 75frecabcl 6399 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
77 dmeq 4827 . . . . . . . . . . . . . . 15 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵))
7877eqeq1d 2186 . . . . . . . . . . . . . 14 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚))
79 fveq1 5514 . . . . . . . . . . . . . . . 16 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚))
8079fveq2d 5519 . . . . . . . . . . . . . . 15 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝐹‘(𝑔𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))
8180eleq2d 2247 . . . . . . . . . . . . . 14 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))
8278, 81anbi12d 473 . . . . . . . . . . . . 13 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
8382rexbidv 2478 . . . . . . . . . . . 12 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
8477eqeq1d 2186 . . . . . . . . . . . . 13 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = ∅ ↔ dom (recs(𝐺) ↾ suc 𝐵) = ∅))
8584anbi1d 465 . . . . . . . . . . . 12 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴)))
8683, 85orbi12d 793 . . . . . . . . . . 11 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
8786abbidv 2295 . . . . . . . . . 10 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
8887, 2fvmptg 5592 . . . . . . . . 9 (((recs(𝐺) ↾ suc 𝐵) ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ 𝑆) → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
8961, 76, 88syl2anc 411 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
9056, 89eqtrd 2210 . . . . . . 7 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
9190abeq2d 2290 . . . . . 6 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
92 fdm 5371 . . . . . . . . . . . 12 ((recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆 → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
9372, 92syl 14 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
94 peano3 4595 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ≠ ∅)
95943ad2ant3 1020 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ≠ ∅)
9693, 95eqnetrd 2371 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) ≠ ∅)
9796neneqd 2368 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ¬ dom (recs(𝐺) ↾ suc 𝐵) = ∅)
9897intnanrd 932 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))
99 biorf 744 . . . . . . . 8 (¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))))
10098, 99syl 14 . . . . . . 7 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))))
101 orcom 728 . . . . . . 7 (((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴)))
102100, 101bitrdi 196 . . . . . 6 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
10393eqeq1d 2186 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ suc 𝐵 = suc 𝑚))
104 vex 2740 . . . . . . . . . . . 12 𝑚 ∈ V
105 suc11g 4556 . . . . . . . . . . . 12 ((𝐵 ∈ ω ∧ 𝑚 ∈ V) → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
106104, 105mpan2 425 . . . . . . . . . . 11 (𝐵 ∈ ω → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
1071063ad2ant3 1020 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
108103, 107bitrd 188 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝐵 = 𝑚))
109 eqcom 2179 . . . . . . . . 9 (𝐵 = 𝑚𝑚 = 𝐵)
110108, 109bitrdi 196 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑚 = 𝐵))
111110anbi1d 465 . . . . . . 7 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ((dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
112111rexbidv 2478 . . . . . 6 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
11391, 102, 1123bitr2d 216 . . . . 5 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
114 fveq2 5515 . . . . . . . 8 (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵))
115114fveq2d 5519 . . . . . . 7 (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
116115eleq2d 2247 . . . . . 6 (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
117116ceqsrexbv 2868 . . . . 5 (∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
118113, 117bitrdi 196 . . . 4 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))))
1191183anibar 1165 . . 3 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
120119eqrdv 2175 . 2 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
121 sucidg 4416 . . . . . 6 (𝐵 ∈ ω → 𝐵 ∈ suc 𝐵)
122 fvres 5539 . . . . . 6 (𝐵 ∈ suc 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
123121, 122syl 14 . . . . 5 (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
1246fveq1i 5516 . . . . . 6 (frec(𝐹, 𝐴)‘𝐵) = ((recs(𝐺) ↾ ω)‘𝐵)
125 fvres 5539 . . . . . 6 (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘𝐵) = (recs(𝐺)‘𝐵))
126124, 125eqtrid 2222 . . . . 5 (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘𝐵) = (recs(𝐺)‘𝐵))
127123, 126eqtr4d 2213 . . . 4 (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
1281273ad2ant3 1020 . . 3 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
129128fveq2d 5519 . 2 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
130120, 129eqtrd 2210 1 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  w3a 978   = wceq 1353  wcel 2148  {cab 2163  wne 2347  wral 2455  wrex 2456  Vcvv 2737  wss 3129  c0 3422   cuni 3809  cmpt 4064  Ord word 4362  Lim wlim 4364  suc csuc 4365  ωcom 4589  dom cdm 4626  cres 4628  Fun wfun 5210  wf 5212  cfv 5216  recscrecs 6304  freccfrec 6390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-recs 6305  df-frec 6391
This theorem is referenced by:  frecsuc  6407
  Copyright terms: Public domain W3C validator