Step | Hyp | Ref
| Expression |
1 | | tfrlem.1 |
. . . 4
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
2 | 1 | tfrlem8 8215 |
. . 3
⊢ Ord dom
recs(𝐹) |
3 | | ordzsl 7692 |
. . 3
⊢ (Ord dom
recs(𝐹) ↔ (dom
recs(𝐹) = ∅ ∨
∃𝑧 ∈ On dom
recs(𝐹) = suc 𝑧 ∨ Lim dom recs(𝐹))) |
4 | 2, 3 | mpbi 229 |
. 2
⊢ (dom
recs(𝐹) = ∅ ∨
∃𝑧 ∈ On dom
recs(𝐹) = suc 𝑧 ∨ Lim dom recs(𝐹)) |
5 | | res0 5895 |
. . . . . . 7
⊢
(recs(𝐹) ↾
∅) = ∅ |
6 | | 0ex 5231 |
. . . . . . 7
⊢ ∅
∈ V |
7 | 5, 6 | eqeltri 2835 |
. . . . . 6
⊢
(recs(𝐹) ↾
∅) ∈ V |
8 | | 0elon 6319 |
. . . . . . 7
⊢ ∅
∈ On |
9 | 1 | tfrlem15 8223 |
. . . . . . 7
⊢ (∅
∈ On → (∅ ∈ dom recs(𝐹) ↔ (recs(𝐹) ↾ ∅) ∈
V)) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ (∅
∈ dom recs(𝐹) ↔
(recs(𝐹) ↾ ∅)
∈ V) |
11 | 7, 10 | mpbir 230 |
. . . . 5
⊢ ∅
∈ dom recs(𝐹) |
12 | 11 | n0ii 4270 |
. . . 4
⊢ ¬
dom recs(𝐹) =
∅ |
13 | 12 | pm2.21i 119 |
. . 3
⊢ (dom
recs(𝐹) = ∅ →
Lim dom recs(𝐹)) |
14 | 1 | tfrlem13 8221 |
. . . . 5
⊢ ¬
recs(𝐹) ∈
V |
15 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → dom recs(𝐹) = suc 𝑧) |
16 | | df-suc 6272 |
. . . . . . . . . 10
⊢ suc 𝑧 = (𝑧 ∪ {𝑧}) |
17 | 15, 16 | eqtrdi 2794 |
. . . . . . . . 9
⊢ ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → dom recs(𝐹) = (𝑧 ∪ {𝑧})) |
18 | 17 | reseq2d 5891 |
. . . . . . . 8
⊢ ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → (recs(𝐹) ↾ dom recs(𝐹)) = (recs(𝐹) ↾ (𝑧 ∪ {𝑧}))) |
19 | 1 | tfrlem6 8213 |
. . . . . . . . 9
⊢ Rel
recs(𝐹) |
20 | | resdm 5936 |
. . . . . . . . 9
⊢ (Rel
recs(𝐹) → (recs(𝐹) ↾ dom recs(𝐹)) = recs(𝐹)) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . 8
⊢
(recs(𝐹) ↾ dom
recs(𝐹)) = recs(𝐹) |
22 | | resundi 5905 |
. . . . . . . 8
⊢
(recs(𝐹) ↾
(𝑧 ∪ {𝑧})) = ((recs(𝐹) ↾ 𝑧) ∪ (recs(𝐹) ↾ {𝑧})) |
23 | 18, 21, 22 | 3eqtr3g 2801 |
. . . . . . 7
⊢ ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → recs(𝐹) = ((recs(𝐹) ↾ 𝑧) ∪ (recs(𝐹) ↾ {𝑧}))) |
24 | | vex 3436 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
25 | 24 | sucid 6345 |
. . . . . . . . . 10
⊢ 𝑧 ∈ suc 𝑧 |
26 | 25, 15 | eleqtrrid 2846 |
. . . . . . . . 9
⊢ ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → 𝑧 ∈ dom recs(𝐹)) |
27 | 1 | tfrlem9a 8217 |
. . . . . . . . 9
⊢ (𝑧 ∈ dom recs(𝐹) → (recs(𝐹) ↾ 𝑧) ∈ V) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → (recs(𝐹) ↾ 𝑧) ∈ V) |
29 | | snex 5354 |
. . . . . . . . 9
⊢
{〈𝑧,
(recs(𝐹)‘𝑧)〉} ∈
V |
30 | 1 | tfrlem7 8214 |
. . . . . . . . . 10
⊢ Fun
recs(𝐹) |
31 | | funressn 7031 |
. . . . . . . . . 10
⊢ (Fun
recs(𝐹) → (recs(𝐹) ↾ {𝑧}) ⊆ {〈𝑧, (recs(𝐹)‘𝑧)〉}) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . 9
⊢
(recs(𝐹) ↾
{𝑧}) ⊆ {〈𝑧, (recs(𝐹)‘𝑧)〉} |
33 | 29, 32 | ssexi 5246 |
. . . . . . . 8
⊢
(recs(𝐹) ↾
{𝑧}) ∈
V |
34 | | unexg 7599 |
. . . . . . . 8
⊢
(((recs(𝐹) ↾
𝑧) ∈ V ∧
(recs(𝐹) ↾ {𝑧}) ∈ V) → ((recs(𝐹) ↾ 𝑧) ∪ (recs(𝐹) ↾ {𝑧})) ∈ V) |
35 | 28, 33, 34 | sylancl 586 |
. . . . . . 7
⊢ ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → ((recs(𝐹) ↾ 𝑧) ∪ (recs(𝐹) ↾ {𝑧})) ∈ V) |
36 | 23, 35 | eqeltrd 2839 |
. . . . . 6
⊢ ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → recs(𝐹) ∈ V) |
37 | 36 | rexlimiva 3210 |
. . . . 5
⊢
(∃𝑧 ∈ On
dom recs(𝐹) = suc 𝑧 → recs(𝐹) ∈ V) |
38 | 14, 37 | mto 196 |
. . . 4
⊢ ¬
∃𝑧 ∈ On dom
recs(𝐹) = suc 𝑧 |
39 | 38 | pm2.21i 119 |
. . 3
⊢
(∃𝑧 ∈ On
dom recs(𝐹) = suc 𝑧 → Lim dom recs(𝐹)) |
40 | | id 22 |
. . 3
⊢ (Lim dom
recs(𝐹) → Lim dom
recs(𝐹)) |
41 | 13, 39, 40 | 3jaoi 1426 |
. 2
⊢ ((dom
recs(𝐹) = ∅ ∨
∃𝑧 ∈ On dom
recs(𝐹) = suc 𝑧 ∨ Lim dom recs(𝐹)) → Lim dom recs(𝐹)) |
42 | 4, 41 | ax-mp 5 |
1
⊢ Lim dom
recs(𝐹) |