Step |
Hyp |
Ref |
Expression |
1 |
|
tfrlem.1 |
⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } |
2 |
1
|
tfrlem8 |
⊢ Ord dom recs ( 𝐹 ) |
3 |
|
ordzsl |
⊢ ( Ord dom recs ( 𝐹 ) ↔ ( dom recs ( 𝐹 ) = ∅ ∨ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 ∨ Lim dom recs ( 𝐹 ) ) ) |
4 |
2 3
|
mpbi |
⊢ ( dom recs ( 𝐹 ) = ∅ ∨ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 ∨ Lim dom recs ( 𝐹 ) ) |
5 |
|
res0 |
⊢ ( recs ( 𝐹 ) ↾ ∅ ) = ∅ |
6 |
|
0ex |
⊢ ∅ ∈ V |
7 |
5 6
|
eqeltri |
⊢ ( recs ( 𝐹 ) ↾ ∅ ) ∈ V |
8 |
|
0elon |
⊢ ∅ ∈ On |
9 |
1
|
tfrlem15 |
⊢ ( ∅ ∈ On → ( ∅ ∈ dom recs ( 𝐹 ) ↔ ( recs ( 𝐹 ) ↾ ∅ ) ∈ V ) ) |
10 |
8 9
|
ax-mp |
⊢ ( ∅ ∈ dom recs ( 𝐹 ) ↔ ( recs ( 𝐹 ) ↾ ∅ ) ∈ V ) |
11 |
7 10
|
mpbir |
⊢ ∅ ∈ dom recs ( 𝐹 ) |
12 |
11
|
n0ii |
⊢ ¬ dom recs ( 𝐹 ) = ∅ |
13 |
12
|
pm2.21i |
⊢ ( dom recs ( 𝐹 ) = ∅ → Lim dom recs ( 𝐹 ) ) |
14 |
1
|
tfrlem13 |
⊢ ¬ recs ( 𝐹 ) ∈ V |
15 |
|
simpr |
⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → dom recs ( 𝐹 ) = suc 𝑧 ) |
16 |
|
df-suc |
⊢ suc 𝑧 = ( 𝑧 ∪ { 𝑧 } ) |
17 |
15 16
|
eqtrdi |
⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → dom recs ( 𝐹 ) = ( 𝑧 ∪ { 𝑧 } ) ) |
18 |
17
|
reseq2d |
⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = ( recs ( 𝐹 ) ↾ ( 𝑧 ∪ { 𝑧 } ) ) ) |
19 |
1
|
tfrlem6 |
⊢ Rel recs ( 𝐹 ) |
20 |
|
resdm |
⊢ ( Rel recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 ) ) |
21 |
19 20
|
ax-mp |
⊢ ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 ) |
22 |
|
resundi |
⊢ ( recs ( 𝐹 ) ↾ ( 𝑧 ∪ { 𝑧 } ) ) = ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) |
23 |
18 21 22
|
3eqtr3g |
⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → recs ( 𝐹 ) = ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) ) |
24 |
|
vex |
⊢ 𝑧 ∈ V |
25 |
24
|
sucid |
⊢ 𝑧 ∈ suc 𝑧 |
26 |
25 15
|
eleqtrrid |
⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → 𝑧 ∈ dom recs ( 𝐹 ) ) |
27 |
1
|
tfrlem9a |
⊢ ( 𝑧 ∈ dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ 𝑧 ) ∈ V ) |
28 |
26 27
|
syl |
⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → ( recs ( 𝐹 ) ↾ 𝑧 ) ∈ V ) |
29 |
|
snex |
⊢ { 〈 𝑧 , ( recs ( 𝐹 ) ‘ 𝑧 ) 〉 } ∈ V |
30 |
1
|
tfrlem7 |
⊢ Fun recs ( 𝐹 ) |
31 |
|
funressn |
⊢ ( Fun recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ { 𝑧 } ) ⊆ { 〈 𝑧 , ( recs ( 𝐹 ) ‘ 𝑧 ) 〉 } ) |
32 |
30 31
|
ax-mp |
⊢ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ⊆ { 〈 𝑧 , ( recs ( 𝐹 ) ‘ 𝑧 ) 〉 } |
33 |
29 32
|
ssexi |
⊢ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ∈ V |
34 |
|
unexg |
⊢ ( ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∈ V ∧ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ∈ V ) → ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) ∈ V ) |
35 |
28 33 34
|
sylancl |
⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) ∈ V ) |
36 |
23 35
|
eqeltrd |
⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → recs ( 𝐹 ) ∈ V ) |
37 |
36
|
rexlimiva |
⊢ ( ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 → recs ( 𝐹 ) ∈ V ) |
38 |
14 37
|
mto |
⊢ ¬ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 |
39 |
38
|
pm2.21i |
⊢ ( ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 → Lim dom recs ( 𝐹 ) ) |
40 |
|
id |
⊢ ( Lim dom recs ( 𝐹 ) → Lim dom recs ( 𝐹 ) ) |
41 |
13 39 40
|
3jaoi |
⊢ ( ( dom recs ( 𝐹 ) = ∅ ∨ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 ∨ Lim dom recs ( 𝐹 ) ) → Lim dom recs ( 𝐹 ) ) |
42 |
4 41
|
ax-mp |
⊢ Lim dom recs ( 𝐹 ) |