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

Theorem frecsuclem 6153
Description: Lemma for frecsuc 6154. 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 6138 . . . . . . . . . . . . 13 frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
2 frecsuclem.g . . . . . . . . . . . . . . 15 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
3 recseq 6053 . . . . . . . . . . . . . . 15 (𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) → recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})))
42, 3ax-mp 7 . . . . . . . . . . . . . 14 recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
54reseq1i 4697 . . . . . . . . . . . . 13 (recs(𝐺) ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
61, 5eqtr4i 2111 . . . . . . . . . . . 12 frec(𝐹, 𝐴) = (recs(𝐺) ↾ ω)
76fveq1i 5290 . . . . . . . . . . 11 (frec(𝐹, 𝐴)‘suc 𝐵) = ((recs(𝐺) ↾ ω)‘suc 𝐵)
8 peano2 4400 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ∈ ω)
9 fvres 5313 . . . . . . . . . . . 12 (suc 𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
108, 9syl 14 . . . . . . . . . . 11 (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
117, 10syl5eq 2132 . . . . . . . . . 10 (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
12113ad2ant3 966 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
13 eqid 2088 . . . . . . . . . . 11 recs(𝐺) = recs(𝐺)
142funmpt2 5039 . . . . . . . . . . . 12 Fun 𝐺
1514a1i 9 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Fun 𝐺)
16 ordom 4411 . . . . . . . . . . . 12 Ord ω
1716a1i 9 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Ord ω)
18 vex 2622 . . . . . . . . . . . . . 14 𝑓 ∈ V
1918a1i 9 . . . . . . . . . . . . 13 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓 ∈ V)
20 simp2 944 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑦 ∈ ω)
21 simp3 945 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓:𝑦𝑆)
22 simp11 973 . . . . . . . . . . . . . . 15 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
23 fveq2 5289 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
2423eleq1d 2156 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → ((𝐹𝑧) ∈ 𝑆 ↔ (𝐹𝑤) ∈ 𝑆))
2524cbvralv 2590 . . . . . . . . . . . . . . 15 (∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆 ↔ ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
2622, 25sylib 120 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
27 simp12 974 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝐴𝑆)
2820, 21, 26, 27frecabcl 6146 . . . . . . . . . . . . 13 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
29 dmeq 4624 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
3029eqeq1d 2096 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚))
31 fveq1 5288 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔𝑚) = (𝑓𝑚))
3231fveq2d 5293 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → (𝐹‘(𝑔𝑚)) = (𝐹‘(𝑓𝑚)))
3332eleq2d 2157 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝑓𝑚))))
3430, 33anbi12d 457 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑓 → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
3534rexbidv 2381 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑓 → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
3629eqeq1d 2096 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑓 → (dom 𝑔 = ∅ ↔ dom 𝑓 = ∅))
3736anbi1d 453 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑓 → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑥𝐴)))
3835, 37orbi12d 742 . . . . . . . . . . . . . . 15 (𝑔 = 𝑓 → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))))
3938abbidv 2205 . . . . . . . . . . . . . 14 (𝑔 = 𝑓 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4039, 2fvmptg 5364 . . . . . . . . . . . . 13 ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆) → (𝐺𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4119, 28, 40syl2anc 403 . . . . . . . . . . . 12 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → (𝐺𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4241, 28eqeltrd 2164 . . . . . . . . . . 11 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → (𝐺𝑓) ∈ 𝑆)
43 limom 4418 . . . . . . . . . . . . . . 15 Lim ω
44 limuni 4214 . . . . . . . . . . . . . . 15 (Lim ω → ω = ω)
4543, 44ax-mp 7 . . . . . . . . . . . . . 14 ω = ω
4645eleq2i 2154 . . . . . . . . . . . . 13 (𝑦 ∈ ω ↔ 𝑦 ω)
47 peano2 4400 . . . . . . . . . . . . 13 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
4846, 47sylbir 133 . . . . . . . . . . . 12 (𝑦 ω → suc 𝑦 ∈ ω)
4948adantl 271 . . . . . . . . . . 11 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ω) → suc 𝑦 ∈ ω)
5045eleq2i 2154 . . . . . . . . . . . . 13 (suc 𝐵 ∈ ω ↔ suc 𝐵 ω)
518, 50sylib 120 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ω)
52513ad2ant3 966 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ω)
5313, 15, 17, 42, 49, 52tfrcldm 6110 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ∈ dom recs(𝐺))
5413tfr2a 6068 . . . . . . . . . 10 (suc 𝐵 ∈ dom recs(𝐺) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
5553, 54syl 14 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
5612, 55eqtrd 2120 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
57 tfrfun 6067 . . . . . . . . . . 11 Fun recs(𝐺)
5857a1i 9 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Fun recs(𝐺))
5983ad2ant3 966 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ∈ ω)
60 resfunexg 5500 . . . . . . . . . 10 ((Fun recs(𝐺) ∧ suc 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
6158, 59, 60syl2anc 403 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
62 frecfcl 6152 . . . . . . . . . . . . 13 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → frec(𝐹, 𝐴):ω⟶𝑆)
636feq1i 5140 . . . . . . . . . . . . 13 (frec(𝐹, 𝐴):ω⟶𝑆 ↔ (recs(𝐺) ↾ ω):ω⟶𝑆)
6462, 63sylib 120 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → (recs(𝐺) ↾ ω):ω⟶𝑆)
65643adant3 963 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ ω):ω⟶𝑆)
66 simp3 945 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → 𝐵 ∈ ω)
67 ordelsuc 4312 . . . . . . . . . . . . . 14 ((𝐵 ∈ ω ∧ Ord ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
6816, 67mpan2 416 . . . . . . . . . . . . 13 (𝐵 ∈ ω → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
69683ad2ant3 966 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
7066, 69mpbid 145 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ⊆ ω)
71 fssres2 5172 . . . . . . . . . . 11 (((recs(𝐺) ↾ ω):ω⟶𝑆 ∧ suc 𝐵 ⊆ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆)
7265, 70, 71syl2anc 403 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆)
73 simp1 943 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
7473, 25sylib 120 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
75 simp2 944 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → 𝐴𝑆)
7659, 72, 74, 75frecabcl 6146 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
77 dmeq 4624 . . . . . . . . . . . . . . 15 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵))
7877eqeq1d 2096 . . . . . . . . . . . . . 14 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚))
79 fveq1 5288 . . . . . . . . . . . . . . . 16 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚))
8079fveq2d 5293 . . . . . . . . . . . . . . 15 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝐹‘(𝑔𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))
8180eleq2d 2157 . . . . . . . . . . . . . 14 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))
8278, 81anbi12d 457 . . . . . . . . . . . . 13 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
8382rexbidv 2381 . . . . . . . . . . . 12 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
8477eqeq1d 2096 . . . . . . . . . . . . 13 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = ∅ ↔ dom (recs(𝐺) ↾ suc 𝐵) = ∅))
8584anbi1d 453 . . . . . . . . . . . 12 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴)))
8683, 85orbi12d 742 . . . . . . . . . . 11 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
8786abbidv 2205 . . . . . . . . . 10 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
8887, 2fvmptg 5364 . . . . . . . . 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 403 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
9056, 89eqtrd 2120 . . . . . . 7 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))})
9190abeq2d 2200 . . . . . 6 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
92 fdm 5152 . . . . . . . . . . . 12 ((recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆 → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
9372, 92syl 14 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
94 peano3 4401 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ≠ ∅)
95943ad2ant3 966 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ≠ ∅)
9693, 95eqnetrd 2279 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) ≠ ∅)
9796neneqd 2276 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ¬ dom (recs(𝐺) ↾ suc 𝐵) = ∅)
9897intnanrd 879 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))
99 biorf 698 . . . . . . . 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 682 . . . . . . 7 (((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴)))
102100, 101syl6bb 194 . . . . . 6 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))))
10393eqeq1d 2096 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ suc 𝐵 = suc 𝑚))
104 vex 2622 . . . . . . . . . . . 12 𝑚 ∈ V
105 suc11g 4363 . . . . . . . . . . . 12 ((𝐵 ∈ ω ∧ 𝑚 ∈ V) → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
106104, 105mpan2 416 . . . . . . . . . . 11 (𝐵 ∈ ω → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
1071063ad2ant3 966 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (suc 𝐵 = suc 𝑚𝐵 = 𝑚))
108103, 107bitrd 186 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝐵 = 𝑚))
109 eqcom 2090 . . . . . . . . 9 (𝐵 = 𝑚𝑚 = 𝐵)
110108, 109syl6bb 194 . . . . . . . 8 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑚 = 𝐵))
111110anbi1d 453 . . . . . . 7 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ((dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
112111rexbidv 2381 . . . . . 6 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
11391, 102, 1123bitr2d 214 . . . . 5 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
114 fveq2 5289 . . . . . . . 8 (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵))
115114fveq2d 5293 . . . . . . 7 (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
116115eleq2d 2157 . . . . . 6 (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
117116ceqsrexbv 2746 . . . . 5 (∃𝑚 ∈ ω (𝑚 = 𝐵𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
118113, 117syl6bb 194 . . . 4 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))))
1191183anibar 1111 . . 3 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
120119eqrdv 2086 . 2 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
121 sucidg 4234 . . . . . 6 (𝐵 ∈ ω → 𝐵 ∈ suc 𝐵)
122 fvres 5313 . . . . . 6 (𝐵 ∈ suc 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
123121, 122syl 14 . . . . 5 (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
1246fveq1i 5290 . . . . . 6 (frec(𝐹, 𝐴)‘𝐵) = ((recs(𝐺) ↾ ω)‘𝐵)
125 fvres 5313 . . . . . 6 (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘𝐵) = (recs(𝐺)‘𝐵))
126124, 125syl5eq 2132 . . . . 5 (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘𝐵) = (recs(𝐺)‘𝐵))
127123, 126eqtr4d 2123 . . . 4 (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
1281273ad2ant3 966 . . 3 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
129128fveq2d 5293 . 2 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
130120, 129eqtrd 2120 1 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 664  w3a 924   = wceq 1289  wcel 1438  {cab 2074  wne 2255  wral 2359  wrex 2360  Vcvv 2619  wss 2997  c0 3284   cuni 3648  cmpt 3891  Ord word 4180  Lim wlim 4182  suc csuc 4183  ωcom 4395  dom cdm 4428  cres 4430  Fun wfun 4996  wf 4998  cfv 5002  recscrecs 6051  freccfrec 6137
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3946  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027  ax-un 4251  ax-setind 4343  ax-iinf 4393
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-iun 3727  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-id 4111  df-iord 4184  df-on 4186  df-ilim 4187  df-suc 4189  df-iom 4396  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-fv 5010  df-recs 6052  df-frec 6138
This theorem is referenced by:  frecsuc  6154
  Copyright terms: Public domain W3C validator