| Step | Hyp | Ref
| Expression |
| 1 | | tfrlem.1 |
. . . . . 6
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
| 2 | 1 | tfrlem8 8424 |
. . . . 5
⊢ Ord dom
recs(𝐹) |
| 3 | 2 | a1i 11 |
. . . 4
⊢
(recs(𝐹) ∈ V
→ Ord dom recs(𝐹)) |
| 4 | | dmexg 7923 |
. . . 4
⊢
(recs(𝐹) ∈ V
→ dom recs(𝐹) ∈
V) |
| 5 | | elon2 6395 |
. . . 4
⊢ (dom
recs(𝐹) ∈ On ↔
(Ord dom recs(𝐹) ∧ dom
recs(𝐹) ∈
V)) |
| 6 | 3, 4, 5 | sylanbrc 583 |
. . 3
⊢
(recs(𝐹) ∈ V
→ dom recs(𝐹) ∈
On) |
| 7 | | onsuc 7831 |
. . . 4
⊢ (dom
recs(𝐹) ∈ On →
suc dom recs(𝐹) ∈
On) |
| 8 | | tfrlem.3 |
. . . . 5
⊢ 𝐶 = (recs(𝐹) ∪ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
| 9 | 1, 8 | tfrlem10 8427 |
. . . 4
⊢ (dom
recs(𝐹) ∈ On →
𝐶 Fn suc dom recs(𝐹)) |
| 10 | 1, 8 | tfrlem11 8428 |
. . . . . 6
⊢ (dom
recs(𝐹) ∈ On →
(𝑧 ∈ suc dom
recs(𝐹) → (𝐶‘𝑧) = (𝐹‘(𝐶 ↾ 𝑧)))) |
| 11 | 10 | ralrimiv 3145 |
. . . . 5
⊢ (dom
recs(𝐹) ∈ On →
∀𝑧 ∈ suc dom
recs(𝐹)(𝐶‘𝑧) = (𝐹‘(𝐶 ↾ 𝑧))) |
| 12 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝐶‘𝑧) = (𝐶‘𝑦)) |
| 13 | | reseq2 5992 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝐶 ↾ 𝑧) = (𝐶 ↾ 𝑦)) |
| 14 | 13 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝐹‘(𝐶 ↾ 𝑧)) = (𝐹‘(𝐶 ↾ 𝑦))) |
| 15 | 12, 14 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ((𝐶‘𝑧) = (𝐹‘(𝐶 ↾ 𝑧)) ↔ (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦)))) |
| 16 | 15 | cbvralvw 3237 |
. . . . 5
⊢
(∀𝑧 ∈
suc dom recs(𝐹)(𝐶‘𝑧) = (𝐹‘(𝐶 ↾ 𝑧)) ↔ ∀𝑦 ∈ suc dom recs(𝐹)(𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦))) |
| 17 | 11, 16 | sylib 218 |
. . . 4
⊢ (dom
recs(𝐹) ∈ On →
∀𝑦 ∈ suc dom
recs(𝐹)(𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦))) |
| 18 | | fneq2 6660 |
. . . . . 6
⊢ (𝑥 = suc dom recs(𝐹) → (𝐶 Fn 𝑥 ↔ 𝐶 Fn suc dom recs(𝐹))) |
| 19 | | raleq 3323 |
. . . . . 6
⊢ (𝑥 = suc dom recs(𝐹) → (∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦)) ↔ ∀𝑦 ∈ suc dom recs(𝐹)(𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦)))) |
| 20 | 18, 19 | anbi12d 632 |
. . . . 5
⊢ (𝑥 = suc dom recs(𝐹) → ((𝐶 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦))) ↔ (𝐶 Fn suc dom recs(𝐹) ∧ ∀𝑦 ∈ suc dom recs(𝐹)(𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦))))) |
| 21 | 20 | rspcev 3622 |
. . . 4
⊢ ((suc dom
recs(𝐹) ∈ On ∧
(𝐶 Fn suc dom recs(𝐹) ∧ ∀𝑦 ∈ suc dom recs(𝐹)(𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦)))) → ∃𝑥 ∈ On (𝐶 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦)))) |
| 22 | 7, 9, 17, 21 | syl12anc 837 |
. . 3
⊢ (dom
recs(𝐹) ∈ On →
∃𝑥 ∈ On (𝐶 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦)))) |
| 23 | 6, 22 | syl 17 |
. 2
⊢
(recs(𝐹) ∈ V
→ ∃𝑥 ∈ On
(𝐶 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦)))) |
| 24 | | snex 5436 |
. . . . 5
⊢
{〈dom recs(𝐹),
(𝐹‘recs(𝐹))〉} ∈
V |
| 25 | | unexg 7763 |
. . . . 5
⊢
((recs(𝐹) ∈ V
∧ {〈dom recs(𝐹),
(𝐹‘recs(𝐹))〉} ∈ V) →
(recs(𝐹) ∪ {〈dom
recs(𝐹), (𝐹‘recs(𝐹))〉}) ∈ V) |
| 26 | 24, 25 | mpan2 691 |
. . . 4
⊢
(recs(𝐹) ∈ V
→ (recs(𝐹) ∪
{〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) ∈ V) |
| 27 | 8, 26 | eqeltrid 2845 |
. . 3
⊢
(recs(𝐹) ∈ V
→ 𝐶 ∈
V) |
| 28 | | fneq1 6659 |
. . . . . 6
⊢ (𝑓 = 𝐶 → (𝑓 Fn 𝑥 ↔ 𝐶 Fn 𝑥)) |
| 29 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑓 = 𝐶 → (𝑓‘𝑦) = (𝐶‘𝑦)) |
| 30 | | reseq1 5991 |
. . . . . . . . 9
⊢ (𝑓 = 𝐶 → (𝑓 ↾ 𝑦) = (𝐶 ↾ 𝑦)) |
| 31 | 30 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑓 = 𝐶 → (𝐹‘(𝑓 ↾ 𝑦)) = (𝐹‘(𝐶 ↾ 𝑦))) |
| 32 | 29, 31 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑓 = 𝐶 → ((𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦)))) |
| 33 | 32 | ralbidv 3178 |
. . . . . 6
⊢ (𝑓 = 𝐶 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦)))) |
| 34 | 28, 33 | anbi12d 632 |
. . . . 5
⊢ (𝑓 = 𝐶 → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ (𝐶 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦))))) |
| 35 | 34 | rexbidv 3179 |
. . . 4
⊢ (𝑓 = 𝐶 → (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ On (𝐶 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦))))) |
| 36 | 35, 1 | elab2g 3680 |
. . 3
⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐴 ↔ ∃𝑥 ∈ On (𝐶 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦))))) |
| 37 | 27, 36 | syl 17 |
. 2
⊢
(recs(𝐹) ∈ V
→ (𝐶 ∈ 𝐴 ↔ ∃𝑥 ∈ On (𝐶 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐶‘𝑦) = (𝐹‘(𝐶 ↾ 𝑦))))) |
| 38 | 23, 37 | mpbird 257 |
1
⊢
(recs(𝐹) ∈ V
→ 𝐶 ∈ 𝐴) |