Step |
Hyp |
Ref |
Expression |
1 |
|
tfr.1 |
⊢ 𝐹 = recs ( 𝐺 ) |
2 |
|
eqid |
⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } |
3 |
2
|
tfrlem7 |
⊢ Fun recs ( 𝐺 ) |
4 |
1
|
funeqi |
⊢ ( Fun 𝐹 ↔ Fun recs ( 𝐺 ) ) |
5 |
3 4
|
mpbir |
⊢ Fun 𝐹 |
6 |
2
|
tfrlem16 |
⊢ Lim dom recs ( 𝐺 ) |
7 |
1
|
dmeqi |
⊢ dom 𝐹 = dom recs ( 𝐺 ) |
8 |
|
limeq |
⊢ ( dom 𝐹 = dom recs ( 𝐺 ) → ( Lim dom 𝐹 ↔ Lim dom recs ( 𝐺 ) ) ) |
9 |
7 8
|
ax-mp |
⊢ ( Lim dom 𝐹 ↔ Lim dom recs ( 𝐺 ) ) |
10 |
6 9
|
mpbir |
⊢ Lim dom 𝐹 |
11 |
5 10
|
pm3.2i |
⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 ) |