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

Theorem frecsuclem 6315
 Description: Lemma for frecsuc 6316. 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 6300 . . . . . . . . . . . . 13 frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
2 frecsuclem.g . . . . . . . . . . . . . . 15 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
3 recseq 6215 . . . . . . . . . . . . . . 15 (𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) → recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})))
42, 3ax-mp 5 . . . . . . . . . . . . . 14 recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
54reseq1i 4827 . . . . . . . . . . . . 13 (recs(𝐺) ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
61, 5eqtr4i 2165 . . . . . . . . . . . 12 frec(𝐹, 𝐴) = (recs(𝐺) ↾ ω)
76fveq1i 5434 . . . . . . . . . . 11 (frec(𝐹, 𝐴)‘suc 𝐵) = ((recs(𝐺) ↾ ω)‘suc 𝐵)
8 peano2 4520 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ∈ ω)
9 fvres 5457 . . . . . . . . . . . 12 (suc 𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
108, 9syl 14 . . . . . . . . . . 11 (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
117, 10syl5eq 2186 . . . . . . . . . 10 (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
12113ad2ant3 1005 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
13 eqid 2141 . . . . . . . . . . 11 recs(𝐺) = recs(𝐺)
142funmpt2 5174 . . . . . . . . . . . 12 Fun 𝐺
1514a1i 9 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Fun 𝐺)
16 ordom 4532 . . . . . . . . . . . 12 Ord ω
1716a1i 9 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Ord ω)
18 vex 2694 . . . . . . . . . . . . . 14 𝑓 ∈ V
1918a1i 9 . . . . . . . . . . . . 13 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓 ∈ V)
20 simp2 983 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑦 ∈ ω)
21 simp3 984 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓:𝑦𝑆)
22 simp11 1012 . . . . . . . . . . . . . . 15 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
23 fveq2 5433 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
2423eleq1d 2210 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → ((𝐹𝑧) ∈ 𝑆 ↔ (𝐹𝑤) ∈ 𝑆))
2524cbvralv 2659 . . . . . . . . . . . . . . 15 (∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆 ↔ ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
2622, 25sylib 121 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
27 simp12 1013 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝐴𝑆)
2820, 21, 26, 27frecabcl 6308 . . . . . . . . . . . . 13 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
29 dmeq 4751 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
3029eqeq1d 2150 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚))
31 fveq1 5432 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔𝑚) = (𝑓𝑚))
3231fveq2d 5437 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → (𝐹‘(𝑔𝑚)) = (𝐹‘(𝑓𝑚)))
3332eleq2d 2211 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝑓𝑚))))
3430, 33anbi12d 465 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑓 → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
3534rexbidv 2441 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑓 → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
3629eqeq1d 2150 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑓 → (dom 𝑔 = ∅ ↔ dom 𝑓 = ∅))
3736anbi1d 461 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑓 → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑥𝐴)))
3835, 37orbi12d 783 . . . . . . . . . . . . . . 15 (𝑔 = 𝑓 → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))))
3938abbidv 2259 . . . . . . . . . . . . . 14 (𝑔 = 𝑓 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4039, 2fvmptg 5509 . . . . . . . . . . . . 13 ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆) → (𝐺𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4119, 28, 40syl2anc 409 . . . . . . . . . . . 12 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → (𝐺𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4241, 28eqeltrd 2218 . . . . . . . . . . 11 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → (𝐺𝑓) ∈ 𝑆)
43 limom 4539 . . . . . . . . . . . . . . 15 Lim ω
44 limuni 4329 . . . . . . . . . . . . . . 15 (Lim ω → ω = ω)
4543, 44ax-mp 5 . . . . . . . . . . . . . 14 ω = ω
4645eleq2i 2208 . . . . . . . . . . . . 13 (𝑦 ∈ ω ↔ 𝑦 ω)
47 peano2 4520 . . . . . . . . . . . . 13 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
4846, 47sylbir 134 . . . . . . . . . . . 12 (𝑦 ω → suc 𝑦 ∈ ω)
4948adantl 275 . . . . . . . . . . 11 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ω) → suc 𝑦 ∈ ω)
5045eleq2i 2208 . . . . . . . . . . . . 13 (suc 𝐵 ∈ ω ↔ suc 𝐵 ω)
518, 50sylib 121 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ω)
52513ad2ant3 1005 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ω)
5313, 15, 17, 42, 49, 52tfrcldm 6272 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ∈ dom recs(𝐺))
5413tfr2a 6230 . . . . . . . . . 10 (suc 𝐵 ∈ dom recs(𝐺) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
5553, 54syl 14 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
5612, 55eqtrd 2174 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
57 tfrfun 6229 . . . . . . . . . . 11 Fun recs(𝐺)
5857a1i 9 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Fun recs(𝐺))
5983ad2ant3 1005 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ∈ ω)
60 resfunexg 5653 . . . . . . . . . 10 ((Fun recs(𝐺) ∧ suc 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
6158, 59, 60syl2anc 409 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
62 frecfcl 6314 . . . . . . . . . . . . 13 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → frec(𝐹, 𝐴):ω⟶𝑆)
636feq1i 5277 . . . . . . . . . . . . 13 (frec(𝐹, 𝐴):ω⟶𝑆 ↔ (recs(𝐺) ↾ ω):ω⟶𝑆)
6462, 63sylib 121 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → (recs(𝐺) ↾ ω):ω⟶𝑆)
65643adant3 1002 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ ω):ω⟶𝑆)
66 simp3 984 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → 𝐵 ∈ ω)
67 ordelsuc 4432 . . . . . . . . . . . . . 14 ((𝐵 ∈ ω ∧ Ord ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
6816, 67mpan2 422 . . . . . . . . . . . . 13 (𝐵 ∈ ω → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
69683ad2ant3 1005 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
7066, 69mpbid 146 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ⊆ ω)
71 fssres2 5312 . . . . . . . . . . 11 (((recs(𝐺) ↾ ω):ω⟶𝑆 ∧ suc 𝐵 ⊆ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆)
7265, 70, 71syl2anc 409 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆)
73 simp1 982 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
7473, 25sylib 121 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
75 simp2 983 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → 𝐴𝑆)
7659, 72, 74, 75frecabcl 6308 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
77 dmeq 4751 . . . . . . . . . . . . . . 15 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵))
7877eqeq1d 2150 . . . . . . . . . . . . . 14 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚))
79 fveq1 5432 . . . . . . . . . . . . . . . 16 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚))
8079fveq2d 5437 . . . . . . . . . . . . . . 15 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝐹‘(𝑔𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))
8180eleq2d 2211 . . . . . . . . . . . . . 14 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))
8278, 81anbi12d 465 . . . . . . . . . . . . 13 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
8382rexbidv 2441 . . . . . . . . . . . 12 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
8477eqeq1d 2150 . . . . . . . . . . . . 13 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = ∅ ↔ dom (recs(𝐺) ↾ suc 𝐵) = ∅))
8584anbi1d 461 . . . . . . . . . . . 12 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴)))
8683, 85orbi12d 783 . . . . . . . . . . 11 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
8786abbidv 2259 . . . . . . . . . 10 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
8887, 2fvmptg 5509 . . . . . . . . 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 409 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
9056, 89eqtrd 2174 . . . . . . 7 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
9190abeq2d 2254 . . . . . 6 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
92 fdm 5290 . . . . . . . . . . . 12 ((recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆 → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
9372, 92syl 14 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
94 peano3 4521 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ≠ ∅)
95943ad2ant3 1005 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ≠ ∅)
9693, 95eqnetrd 2334 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) ≠ ∅)
9796neneqd 2331 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ¬ dom (recs(𝐺) ↾ suc 𝐵) = ∅)
9897intnanrd 918 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))
99 biorf 734 . . . . . . . 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 718 . . . . . . 7 (((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴)))
102100, 101syl6bb 195 . . . . . 6 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
10393eqeq1d 2150 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ suc 𝐵 = suc 𝑚))
104 vex 2694 . . . . . . . . . . . 12 𝑚 ∈ V
105 suc11g 4483 . . . . . . . . . . . 12 ((𝐵 ∈ ω ∧ 𝑚 ∈ V) → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
106104, 105mpan2 422 . . . . . . . . . . 11 (𝐵 ∈ ω → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
1071063ad2ant3 1005 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
108103, 107bitrd 187 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝐵 = 𝑚))
109 eqcom 2143 . . . . . . . . 9 (𝐵 = 𝑚𝑚 = 𝐵)
110108, 109syl6bb 195 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑚 = 𝐵))
111110anbi1d 461 . . . . . . 7 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ((dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
112111rexbidv 2441 . . . . . 6 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
11391, 102, 1123bitr2d 215 . . . . 5 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
114 fveq2 5433 . . . . . . . 8 (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵))
115114fveq2d 5437 . . . . . . 7 (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
116115eleq2d 2211 . . . . . 6 (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
117116ceqsrexbv 2822 . . . . 5 (∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
118113, 117syl6bb 195 . . . 4 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))))
1191183anibar 1150 . . 3 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
120119eqrdv 2139 . 2 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
121 sucidg 4349 . . . . . 6 (𝐵 ∈ ω → 𝐵 ∈ suc 𝐵)
122 fvres 5457 . . . . . 6 (𝐵 ∈ suc 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
123121, 122syl 14 . . . . 5 (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
1246fveq1i 5434 . . . . . 6 (frec(𝐹, 𝐴)‘𝐵) = ((recs(𝐺) ↾ ω)‘𝐵)
125 fvres 5457 . . . . . 6 (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘𝐵) = (recs(𝐺)‘𝐵))
126124, 125syl5eq 2186 . . . . 5 (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘𝐵) = (recs(𝐺)‘𝐵))
127123, 126eqtr4d 2177 . . . 4 (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
1281273ad2ant3 1005 . . 3 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
129128fveq2d 5437 . 2 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
130120, 129eqtrd 2174 1 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∧ w3a 963   = wceq 1332   ∈ wcel 2112  {cab 2127   ≠ wne 2310  ∀wral 2418  ∃wrex 2419  Vcvv 2691   ⊆ wss 3078  ∅c0 3370  ∪ cuni 3746   ↦ cmpt 3999  Ord word 4295  Lim wlim 4297  suc csuc 4298  ωcom 4515  dom cdm 4551   ↾ cres 4553  Fun wfun 5129  ⟶wf 5131  ‘cfv 5135  recscrecs 6213  freccfrec 6299 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2114  ax-14 2115  ax-ext 2123  ax-coll 4053  ax-sep 4056  ax-nul 4064  ax-pow 4108  ax-pr 4142  ax-un 4366  ax-setind 4463  ax-iinf 4513 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1732  df-eu 1993  df-mo 1994  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ne 2311  df-ral 2423  df-rex 2424  df-reu 2425  df-rab 2427  df-v 2693  df-sbc 2916  df-csb 3010  df-dif 3080  df-un 3082  df-in 3084  df-ss 3091  df-nul 3371  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-int 3782  df-iun 3825  df-br 3940  df-opab 4000  df-mpt 4001  df-tr 4037  df-id 4226  df-iord 4299  df-on 4301  df-ilim 4302  df-suc 4304  df-iom 4516  df-xp 4557  df-rel 4558  df-cnv 4559  df-co 4560  df-dm 4561  df-rn 4562  df-res 4563  df-ima 4564  df-iota 5100  df-fun 5137  df-fn 5138  df-f 5139  df-f1 5140  df-fo 5141  df-f1o 5142  df-fv 5143  df-recs 6214  df-frec 6300 This theorem is referenced by:  frecsuc  6316
 Copyright terms: Public domain W3C validator