Step | Hyp | Ref
| Expression |
1 | | eqid 2040 |
. . . . . . . . . . . . 13
⊢
recs(𝐺) = recs(𝐺) |
2 | | frecsuclem1.h |
. . . . . . . . . . . . . 14
⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) |
3 | 2 | frectfr 5985 |
. . . . . . . . . . . . 13
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → ∀𝑦(Fun 𝐺 ∧ (𝐺‘𝑦) ∈ V)) |
4 | 1, 3 | tfri1d 5949 |
. . . . . . . . . . . 12
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → recs(𝐺) Fn On) |
5 | | fnfun 4996 |
. . . . . . . . . . . 12
⊢
(recs(𝐺) Fn On
→ Fun recs(𝐺)) |
6 | 4, 5 | syl 14 |
. . . . . . . . . . 11
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → Fun recs(𝐺)) |
7 | 6 | 3adant3 924 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → Fun recs(𝐺)) |
8 | | peano2 4318 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ω → suc 𝐵 ∈
ω) |
9 | 8 | 3ad2ant3 927 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈
ω) |
10 | | resfunexg 5382 |
. . . . . . . . . 10
⊢ ((Fun
recs(𝐺) ∧ suc 𝐵 ∈ ω) →
(recs(𝐺) ↾ suc 𝐵) ∈ V) |
11 | 7, 9, 10 | syl2anc 391 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V) |
12 | | simp1 904 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ∀𝑧(𝐹‘𝑧) ∈ V) |
13 | | simp2 905 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → 𝐴 ∈ 𝑉) |
14 | 11, 12, 13 | frecabex 5984 |
. . . . . . . 8
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ V) |
15 | | dmeq 4535 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵)) |
16 | 15 | eqeq1d 2048 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚)) |
17 | | fveq1 5177 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚)) |
18 | 17 | fveq2d 5182 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝐹‘(𝑔‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) |
19 | 18 | eleq2d 2107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑥 ∈ (𝐹‘(𝑔‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))) |
20 | 16, 19 | anbi12d 442 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
21 | 20 | rexbidv 2327 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
22 | 15 | eqeq1d 2048 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = ∅ ↔ dom (recs(𝐺) ↾ suc 𝐵) = ∅)) |
23 | 22 | anbi1d 438 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))) |
24 | 21, 23 | orbi12d 707 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))) |
25 | 24 | abbidv 2155 |
. . . . . . . . . . . 12
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))}) |
26 | 25, 2 | fvmptg 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 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))}) |
27 | 26 | ex 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 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})) |
28 | 11, 27 | syl 14 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ({𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ V → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})) |
29 | 2 | frecsuclem1 5987 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵))) |
30 | 29 | eqeq1d 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 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})) |
31 | 28, 30 | sylibrd 158 |
. . . . . . . 8
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ({𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ V → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})) |
32 | 14, 31 | mpd 13 |
. . . . . . 7
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))}) |
33 | 32 | abeq2d 2150 |
. . . . . 6
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))) |
34 | 2 | frecsuclemdm 5988 |
. . . . . . . . . . 11
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵) |
35 | | peano3 4319 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ω → suc 𝐵 ≠ ∅) |
36 | 35 | 3ad2ant3 927 |
. . . . . . . . . . 11
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → suc 𝐵 ≠ ∅) |
37 | 34, 36 | eqnetrd 2229 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) ≠ ∅) |
38 | 37 | neneqd 2226 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ¬ dom
(recs(𝐺) ↾ suc 𝐵) = ∅) |
39 | 38 | intnanrd 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 𝐵)‘𝑚)))))) |
41 | 39, 40 | syl 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 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))) |
43 | 41, 42 | syl6bb 185 |
. . . . . 6
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))) |
44 | 34 | eqeq1d 2048 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ suc 𝐵 = suc 𝑚)) |
45 | | vex 2560 |
. . . . . . . . . . . 12
⊢ 𝑚 ∈ V |
46 | | suc11g 4281 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ω ∧ 𝑚 ∈ V) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚)) |
47 | 45, 46 | mpan2 401 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ω → (suc
𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚)) |
48 | 47 | 3ad2ant3 927 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚)) |
49 | 44, 48 | bitrd 177 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ 𝐵 = 𝑚)) |
50 | | eqcom 2042 |
. . . . . . . . 9
⊢ (𝐵 = 𝑚 ↔ 𝑚 = 𝐵) |
51 | 49, 50 | syl6bb 185 |
. . . . . . . 8
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ 𝑚 = 𝐵)) |
52 | 51 | anbi1d 438 |
. . . . . . 7
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ((dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
53 | 52 | rexbidv 2327 |
. . . . . 6
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
54 | 33, 43, 53 | 3bitr2d 205 |
. . . . 5
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
55 | | fveq2 5178 |
. . . . . . . 8
⊢ (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵)) |
56 | 55 | fveq2d 5182 |
. . . . . . 7
⊢ (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))) |
57 | 56 | eleq2d 2107 |
. . . . . 6
⊢ (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))) |
58 | 57 | ceqsrexbv 2675 |
. . . . 5
⊢
(∃𝑚 ∈
ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))) |
59 | 54, 58 | syl6bb 185 |
. . . 4
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))) |
60 | 59 | 3anibar 1072 |
. . 3
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))) |
61 | 60 | eqrdv 2038 |
. 2
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))) |
62 | 2 | frecsuclem2 5989 |
. . 3
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵)) |
63 | 62 | fveq2d 5182 |
. 2
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) |
64 | 61, 63 | eqtrd 2072 |
1
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) |