Step | Hyp | Ref
| Expression |
1 | | tfrlem.1 |
. . . . . . . . 9
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
2 | 1 | tfrlem3 6258 |
. . . . . . . 8
⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))} |
3 | 2 | abeq2i 2268 |
. . . . . . 7
⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) |
4 | | fndm 5269 |
. . . . . . . . . . 11
⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧) |
5 | 4 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → dom 𝑔 = 𝑧) |
6 | 5 | eleq1d 2226 |
. . . . . . . . 9
⊢ ((𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (dom 𝑔 ∈ On ↔ 𝑧 ∈ On)) |
7 | 6 | biimprcd 159 |
. . . . . . . 8
⊢ (𝑧 ∈ On → ((𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → dom 𝑔 ∈ On)) |
8 | 7 | rexlimiv 2568 |
. . . . . . 7
⊢
(∃𝑧 ∈ On
(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → dom 𝑔 ∈ On) |
9 | 3, 8 | sylbi 120 |
. . . . . 6
⊢ (𝑔 ∈ 𝐴 → dom 𝑔 ∈ On) |
10 | | eleq1a 2229 |
. . . . . 6
⊢ (dom
𝑔 ∈ On → (𝑧 = dom 𝑔 → 𝑧 ∈ On)) |
11 | 9, 10 | syl 14 |
. . . . 5
⊢ (𝑔 ∈ 𝐴 → (𝑧 = dom 𝑔 → 𝑧 ∈ On)) |
12 | 11 | rexlimiv 2568 |
. . . 4
⊢
(∃𝑔 ∈
𝐴 𝑧 = dom 𝑔 → 𝑧 ∈ On) |
13 | 12 | abssi 3203 |
. . 3
⊢ {𝑧 ∣ ∃𝑔 ∈ 𝐴 𝑧 = dom 𝑔} ⊆ On |
14 | | ssorduni 4446 |
. . 3
⊢ ({𝑧 ∣ ∃𝑔 ∈ 𝐴 𝑧 = dom 𝑔} ⊆ On → Ord ∪ {𝑧
∣ ∃𝑔 ∈
𝐴 𝑧 = dom 𝑔}) |
15 | 13, 14 | ax-mp 5 |
. 2
⊢ Ord ∪ {𝑧
∣ ∃𝑔 ∈
𝐴 𝑧 = dom 𝑔} |
16 | 1 | recsfval 6262 |
. . . . 5
⊢
recs(𝐹) = ∪ 𝐴 |
17 | 16 | dmeqi 4787 |
. . . 4
⊢ dom
recs(𝐹) = dom ∪ 𝐴 |
18 | | dmuni 4796 |
. . . 4
⊢ dom ∪ 𝐴 =
∪ 𝑔 ∈ 𝐴 dom 𝑔 |
19 | | vex 2715 |
. . . . . 6
⊢ 𝑔 ∈ V |
20 | 19 | dmex 4852 |
. . . . 5
⊢ dom 𝑔 ∈ V |
21 | 20 | dfiun2 3883 |
. . . 4
⊢ ∪ 𝑔 ∈ 𝐴 dom 𝑔 = ∪ {𝑧 ∣ ∃𝑔 ∈ 𝐴 𝑧 = dom 𝑔} |
22 | 17, 18, 21 | 3eqtri 2182 |
. . 3
⊢ dom
recs(𝐹) = ∪ {𝑧
∣ ∃𝑔 ∈
𝐴 𝑧 = dom 𝑔} |
23 | | ordeq 4332 |
. . 3
⊢ (dom
recs(𝐹) = ∪ {𝑧
∣ ∃𝑔 ∈
𝐴 𝑧 = dom 𝑔} → (Ord dom recs(𝐹) ↔ Ord ∪
{𝑧 ∣ ∃𝑔 ∈ 𝐴 𝑧 = dom 𝑔})) |
24 | 22, 23 | ax-mp 5 |
. 2
⊢ (Ord dom
recs(𝐹) ↔ Ord ∪ {𝑧
∣ ∃𝑔 ∈
𝐴 𝑧 = dom 𝑔}) |
25 | 15, 24 | mpbir 145 |
1
⊢ Ord dom
recs(𝐹) |