Step | Hyp | Ref
| Expression |
1 | | tfrlem.1 |
. . . . . . . . 9
⊢ A = {f ∣
∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))} |
2 | 1 | tfrlem3 5867 |
. . . . . . . 8
⊢ A = {g ∣
∃z ∈ On (g Fn
z ∧ ∀w ∈ z (g‘w) =
(𝐹‘(g ↾ w)))} |
3 | 2 | abeq2i 2145 |
. . . . . . 7
⊢ (g ∈ A ↔ ∃z ∈ On (g Fn
z ∧ ∀w ∈ z (g‘w) =
(𝐹‘(g ↾ w)))) |
4 | | fndm 4941 |
. . . . . . . . . . 11
⊢ (g Fn z →
dom g = z) |
5 | 4 | adantr 261 |
. . . . . . . . . 10
⊢
((g Fn z ∧ ∀w ∈ z (g‘w) =
(𝐹‘(g ↾ w)))
→ dom g = z) |
6 | 5 | eleq1d 2103 |
. . . . . . . . 9
⊢
((g Fn z ∧ ∀w ∈ z (g‘w) =
(𝐹‘(g ↾ w)))
→ (dom g ∈ On ↔ z
∈ On)) |
7 | 6 | biimprcd 149 |
. . . . . . . 8
⊢ (z ∈ On →
((g Fn z ∧ ∀w ∈ z (g‘w) =
(𝐹‘(g ↾ w)))
→ dom g ∈ On)) |
8 | 7 | rexlimiv 2421 |
. . . . . . 7
⊢ (∃z ∈ On (g Fn
z ∧ ∀w ∈ z (g‘w) =
(𝐹‘(g ↾ w)))
→ dom g ∈ On) |
9 | 3, 8 | sylbi 114 |
. . . . . 6
⊢ (g ∈ A → dom g
∈ On) |
10 | | eleq1a 2106 |
. . . . . 6
⊢ (dom
g ∈ On
→ (z = dom g → z ∈ On)) |
11 | 9, 10 | syl 14 |
. . . . 5
⊢ (g ∈ A → (z =
dom g → z ∈
On)) |
12 | 11 | rexlimiv 2421 |
. . . 4
⊢ (∃g ∈ A z = dom g →
z ∈
On) |
13 | 12 | abssi 3009 |
. . 3
⊢ {z ∣ ∃g ∈ A z = dom g}
⊆ On |
14 | | ssorduni 4179 |
. . 3
⊢
({z ∣ ∃g ∈ A z = dom g}
⊆ On → Ord ∪ {z ∣ ∃g ∈ A z = dom g}) |
15 | 13, 14 | ax-mp 7 |
. 2
⊢ Ord ∪ {z ∣ ∃g ∈ A z = dom g} |
16 | 1 | recsfval 5872 |
. . . . 5
⊢
recs(𝐹) = ∪ A |
17 | 16 | dmeqi 4479 |
. . . 4
⊢ dom
recs(𝐹) = dom ∪ A |
18 | | dmuni 4488 |
. . . 4
⊢ dom ∪ A = ∪ g ∈ A dom
g |
19 | | vex 2554 |
. . . . . 6
⊢ g ∈
V |
20 | 19 | dmex 4541 |
. . . . 5
⊢ dom
g ∈
V |
21 | 20 | dfiun2 3682 |
. . . 4
⊢ ∪ g ∈ A dom
g = ∪ {z ∣ ∃g ∈ A z = dom g} |
22 | 17, 18, 21 | 3eqtri 2061 |
. . 3
⊢ dom
recs(𝐹) = ∪ {z ∣ ∃g ∈ A z = dom g} |
23 | | ordeq 4075 |
. . 3
⊢ (dom
recs(𝐹) = ∪ {z ∣ ∃g ∈ A z = dom g}
→ (Ord dom recs(𝐹)
↔ Ord ∪ {z
∣ ∃g ∈ A z = dom
g})) |
24 | 22, 23 | ax-mp 7 |
. 2
⊢ (Ord dom
recs(𝐹) ↔ Ord ∪ {z ∣ ∃g ∈ A z = dom g}) |
25 | 15, 24 | mpbir 134 |
1
⊢ Ord dom
recs(𝐹) |