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

Theorem frecsuclem 6407
Description: Lemma for frecsuc 6408. 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 6392 . . . . . . . . . . . . 13 frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
2 frecsuclem.g . . . . . . . . . . . . . . 15 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
3 recseq 6307 . . . . . . . . . . . . . . 15 (𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) → recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})))
42, 3ax-mp 5 . . . . . . . . . . . . . 14 recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
54reseq1i 4904 . . . . . . . . . . . . 13 (recs(𝐺) ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
61, 5eqtr4i 2201 . . . . . . . . . . . 12 frec(𝐹, 𝐴) = (recs(𝐺) ↾ ω)
76fveq1i 5517 . . . . . . . . . . 11 (frec(𝐹, 𝐴)‘suc 𝐵) = ((recs(𝐺) ↾ ω)‘suc 𝐵)
8 peano2 4595 . . . . . . . . . . . 12 (𝐵 ∈ ω → suc 𝐵 ∈ ω)
9 fvres 5540 . . . . . . . . . . . 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 5256 . . . . . . . . . . . 12 Fun 𝐺
1514a1i 9 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Fun 𝐺)
16 ordom 4607 . . . . . . . . . . . 12 Ord ω
1716a1i 9 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Ord ω)
18 vex 2741 . . . . . . . . . . . . . 14 𝑓 ∈ V
1918a1i 9 . . . . . . . . . . . . 13 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓 ∈ V)
20 simp2 998 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑦 ∈ ω)
21 simp3 999 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓:𝑦𝑆)
22 simp11 1027 . . . . . . . . . . . . . . 15 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
23 fveq2 5516 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
2423eleq1d 2246 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → ((𝐹𝑧) ∈ 𝑆 ↔ (𝐹𝑤) ∈ 𝑆))
2524cbvralv 2704 . . . . . . . . . . . . . . 15 (∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆 ↔ ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
2622, 25sylib 122 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
27 simp12 1028 . . . . . . . . . . . . . 14 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝐴𝑆)
2820, 21, 26, 27frecabcl 6400 . . . . . . . . . . . . 13 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
29 dmeq 4828 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
3029eqeq1d 2186 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚))
31 fveq1 5515 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔𝑚) = (𝑓𝑚))
3231fveq2d 5520 . . . . . . . . . . . . . . . . . . 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 5593 . . . . . . . . . . . . 13 ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆) → (𝐺𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4119, 28, 40syl2anc 411 . . . . . . . . . . . 12 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → (𝐺𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
4241, 28eqeltrd 2254 . . . . . . . . . . 11 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → (𝐺𝑓) ∈ 𝑆)
43 limom 4614 . . . . . . . . . . . . . . 15 Lim ω
44 limuni 4397 . . . . . . . . . . . . . . 15 (Lim ω → ω = ω)
4543, 44ax-mp 5 . . . . . . . . . . . . . 14 ω = ω
4645eleq2i 2244 . . . . . . . . . . . . 13 (𝑦 ∈ ω ↔ 𝑦 ω)
47 peano2 4595 . . . . . . . . . . . . 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 6364 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ∈ dom recs(𝐺))
5413tfr2a 6322 . . . . . . . . . 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 6321 . . . . . . . . . . 11 Fun recs(𝐺)
5857a1i 9 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → Fun recs(𝐺))
5983ad2ant3 1020 . . . . . . . . . 10 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ∈ ω)
60 resfunexg 5738 . . . . . . . . . 10 ((Fun recs(𝐺) ∧ suc 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
6158, 59, 60syl2anc 411 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
62 frecfcl 6406 . . . . . . . . . . . . 13 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → frec(𝐹, 𝐴):ω⟶𝑆)
636feq1i 5359 . . . . . . . . . . . . 13 (frec(𝐹, 𝐴):ω⟶𝑆 ↔ (recs(𝐺) ↾ ω):ω⟶𝑆)
6462, 63sylib 122 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → (recs(𝐺) ↾ ω):ω⟶𝑆)
65643adant3 1017 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (recs(𝐺) ↾ ω):ω⟶𝑆)
66 simp3 999 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → 𝐵 ∈ ω)
67 ordelsuc 4505 . . . . . . . . . . . . . 14 ((𝐵 ∈ ω ∧ Ord ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
6816, 67mpan2 425 . . . . . . . . . . . . 13 (𝐵 ∈ ω → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
69683ad2ant3 1020 . . . . . . . . . . . 12 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
7066, 69mpbid 147 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → suc 𝐵 ⊆ ω)
71 fssres2 5394 . . . . . . . . . . 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 6400 . . . . . . . . 9 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
77 dmeq 4828 . . . . . . . . . . . . . . 15 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵))
7877eqeq1d 2186 . . . . . . . . . . . . . 14 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚))
79 fveq1 5515 . . . . . . . . . . . . . . . 16 (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚))
8079fveq2d 5520 . . . . . . . . . . . . . . 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 5593 . . . . . . . . 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 5372 . . . . . . . . . . . 12 ((recs(𝐺) ↾ suc 𝐵):suc 𝐵𝑆 → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
9372, 92syl 14 . . . . . . . . . . 11 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
94 peano3 4596 . . . . . . . . . . . 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 2741 . . . . . . . . . . . 12 𝑚 ∈ V
105 suc11g 4557 . . . . . . . . . . . 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 5516 . . . . . . . 8 (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵))
115114fveq2d 5520 . . . . . . 7 (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
116115eleq2d 2247 . . . . . 6 (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
117116ceqsrexbv 2869 . . . . 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 4417 . . . . . 6 (𝐵 ∈ ω → 𝐵 ∈ suc 𝐵)
122 fvres 5540 . . . . . 6 (𝐵 ∈ suc 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
123121, 122syl 14 . . . . 5 (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
1246fveq1i 5517 . . . . . 6 (frec(𝐹, 𝐴)‘𝐵) = ((recs(𝐺) ↾ ω)‘𝐵)
125 fvres 5540 . . . . . 6 (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘𝐵) = (recs(𝐺)‘𝐵))
126124, 125eqtrid 2222 . . . . 5 (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘𝐵) = (recs(𝐺)‘𝐵))
127123, 126eqtr4d 2213 . . . 4 (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
1281273ad2ant3 1020 . . 3 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
129128fveq2d 5520 . 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 2738  wss 3130  c0 3423   cuni 3810  cmpt 4065  Ord word 4363  Lim wlim 4365  suc csuc 4366  ωcom 4590  dom cdm 4627  cres 4629  Fun wfun 5211  wf 5213  cfv 5217  recscrecs 6305  freccfrec 6391
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 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588
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 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-iord 4367  df-on 4369  df-ilim 4370  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-recs 6306  df-frec 6392
This theorem is referenced by:  frecsuc  6408
  Copyright terms: Public domain W3C validator