Step | Hyp | Ref
| Expression |
1 | | eqid 2081 |
. . . . . . . . . . . . 13
⊢
recs(𝐺) = recs(𝐺) |
2 | | frecsuclem1.h |
. . . . . . . . . . . . . 14
⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) |
3 | 2 | frectfr 6008 |
. . . . . . . . . . . . 13
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → ∀𝑦(Fun 𝐺 ∧ (𝐺‘𝑦) ∈ V)) |
4 | 1, 3 | tfri1d 5972 |
. . . . . . . . . . . 12
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → recs(𝐺) Fn On) |
5 | | fnfun 5016 |
. . . . . . . . . . . 12
⊢
(recs(𝐺) Fn On
→ Fun recs(𝐺)) |
6 | 4, 5 | syl 14 |
. . . . . . . . . . 11
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → Fun recs(𝐺)) |
7 | 6 | 3adant3 958 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → Fun recs(𝐺)) |
8 | | peano2 4336 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ω → suc 𝐵 ∈
ω) |
9 | 8 | 3ad2ant3 961 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈
ω) |
10 | | resfunexg 5403 |
. . . . . . . . . 10
⊢ ((Fun
recs(𝐺) ∧ suc 𝐵 ∈ ω) →
(recs(𝐺) ↾ suc 𝐵) ∈ V) |
11 | 7, 9, 10 | syl2anc 403 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V) |
12 | | simp1 938 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ∀𝑧(𝐹‘𝑧) ∈ V) |
13 | | simp2 939 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → 𝐴 ∈ 𝑉) |
14 | 11, 12, 13 | frecabex 6007 |
. . . . . . . 8
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ V) |
15 | | dmeq 4553 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵)) |
16 | 15 | eqeq1d 2089 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚)) |
17 | | fveq1 5197 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚)) |
18 | 17 | fveq2d 5202 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝐹‘(𝑔‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) |
19 | 18 | eleq2d 2148 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑥 ∈ (𝐹‘(𝑔‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))) |
20 | 16, 19 | anbi12d 456 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
21 | 20 | rexbidv 2369 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
22 | 15 | eqeq1d 2089 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = ∅ ↔ dom (recs(𝐺) ↾ suc 𝐵) = ∅)) |
23 | 22 | anbi1d 452 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))) |
24 | 21, 23 | orbi12d 739 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))) |
25 | 24 | abbidv 2196 |
. . . . . . . . . . . 12
⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))}) |
26 | 25, 2 | fvmptg 5269 |
. . . . . . . . . . 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 113 |
. . . . . . . . . 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 6010 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵))) |
30 | 29 | eqeq1d 2089 |
. . . . . . . . 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 167 |
. . . . . . . 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 2191 |
. . . . . 6
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))) |
34 | 2 | frecsuclemdm 6011 |
. . . . . . . . . . 11
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵) |
35 | | peano3 4337 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ω → suc 𝐵 ≠ ∅) |
36 | 35 | 3ad2ant3 961 |
. . . . . . . . . . 11
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → suc 𝐵 ≠ ∅) |
37 | 34, 36 | eqnetrd 2269 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) ≠ ∅) |
38 | 37 | neneqd 2266 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ¬ dom
(recs(𝐺) ↾ suc 𝐵) = ∅) |
39 | 38 | intnanrd 874 |
. . . . . . . 8
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ¬ (dom
(recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)) |
40 | | biorf 695 |
. . . . . . . 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 679 |
. . . . . . 7
⊢ (((dom
(recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))) |
43 | 41, 42 | syl6bb 194 |
. . . . . 6
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))) |
44 | 34 | eqeq1d 2089 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ suc 𝐵 = suc 𝑚)) |
45 | | vex 2604 |
. . . . . . . . . . . 12
⊢ 𝑚 ∈ V |
46 | | suc11g 4300 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ω ∧ 𝑚 ∈ V) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚)) |
47 | 45, 46 | mpan2 415 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ω → (suc
𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚)) |
48 | 47 | 3ad2ant3 961 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚)) |
49 | 44, 48 | bitrd 186 |
. . . . . . . . 9
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ 𝐵 = 𝑚)) |
50 | | eqcom 2083 |
. . . . . . . . 9
⊢ (𝐵 = 𝑚 ↔ 𝑚 = 𝐵) |
51 | 49, 50 | syl6bb 194 |
. . . . . . . 8
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ 𝑚 = 𝐵)) |
52 | 51 | anbi1d 452 |
. . . . . . 7
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ((dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
53 | 52 | rexbidv 2369 |
. . . . . 6
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
54 | 33, 43, 53 | 3bitr2d 214 |
. . . . 5
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))) |
55 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵)) |
56 | 55 | fveq2d 5202 |
. . . . . . 7
⊢ (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))) |
57 | 56 | eleq2d 2148 |
. . . . . 6
⊢ (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))) |
58 | 57 | ceqsrexbv 2726 |
. . . . 5
⊢
(∃𝑚 ∈
ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))) |
59 | 54, 58 | syl6bb 194 |
. . . 4
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))) |
60 | 59 | 3anibar 1106 |
. . 3
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))) |
61 | 60 | eqrdv 2079 |
. 2
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))) |
62 | 2 | frecsuclem2 6012 |
. . 3
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵)) |
63 | 62 | fveq2d 5202 |
. 2
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) |
64 | 61, 63 | eqtrd 2113 |
1
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) |