Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝑛 = ∅ → ( 𝑅1 ‘ 𝑛 ) = ( 𝑅1 ‘ ∅ ) ) |
2 |
1
|
eleq1d |
⊢ ( 𝑛 = ∅ → ( ( 𝑅1 ‘ 𝑛 ) ∈ Fin ↔ ( 𝑅1 ‘ ∅ ) ∈ Fin ) ) |
3 |
|
fveq2 |
⊢ ( 𝑛 = 𝑚 → ( 𝑅1 ‘ 𝑛 ) = ( 𝑅1 ‘ 𝑚 ) ) |
4 |
3
|
eleq1d |
⊢ ( 𝑛 = 𝑚 → ( ( 𝑅1 ‘ 𝑛 ) ∈ Fin ↔ ( 𝑅1 ‘ 𝑚 ) ∈ Fin ) ) |
5 |
|
fveq2 |
⊢ ( 𝑛 = suc 𝑚 → ( 𝑅1 ‘ 𝑛 ) = ( 𝑅1 ‘ suc 𝑚 ) ) |
6 |
5
|
eleq1d |
⊢ ( 𝑛 = suc 𝑚 → ( ( 𝑅1 ‘ 𝑛 ) ∈ Fin ↔ ( 𝑅1 ‘ suc 𝑚 ) ∈ Fin ) ) |
7 |
|
fveq2 |
⊢ ( 𝑛 = 𝐴 → ( 𝑅1 ‘ 𝑛 ) = ( 𝑅1 ‘ 𝐴 ) ) |
8 |
7
|
eleq1d |
⊢ ( 𝑛 = 𝐴 → ( ( 𝑅1 ‘ 𝑛 ) ∈ Fin ↔ ( 𝑅1 ‘ 𝐴 ) ∈ Fin ) ) |
9 |
|
r10 |
⊢ ( 𝑅1 ‘ ∅ ) = ∅ |
10 |
|
0fin |
⊢ ∅ ∈ Fin |
11 |
9 10
|
eqeltri |
⊢ ( 𝑅1 ‘ ∅ ) ∈ Fin |
12 |
|
pwfi |
⊢ ( ( 𝑅1 ‘ 𝑚 ) ∈ Fin ↔ 𝒫 ( 𝑅1 ‘ 𝑚 ) ∈ Fin ) |
13 |
|
r1funlim |
⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 ) |
14 |
13
|
simpri |
⊢ Lim dom 𝑅1 |
15 |
|
limomss |
⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 ) |
16 |
14 15
|
ax-mp |
⊢ ω ⊆ dom 𝑅1 |
17 |
16
|
sseli |
⊢ ( 𝑚 ∈ ω → 𝑚 ∈ dom 𝑅1 ) |
18 |
|
r1sucg |
⊢ ( 𝑚 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑚 ) = 𝒫 ( 𝑅1 ‘ 𝑚 ) ) |
19 |
17 18
|
syl |
⊢ ( 𝑚 ∈ ω → ( 𝑅1 ‘ suc 𝑚 ) = 𝒫 ( 𝑅1 ‘ 𝑚 ) ) |
20 |
19
|
eleq1d |
⊢ ( 𝑚 ∈ ω → ( ( 𝑅1 ‘ suc 𝑚 ) ∈ Fin ↔ 𝒫 ( 𝑅1 ‘ 𝑚 ) ∈ Fin ) ) |
21 |
12 20
|
bitr4id |
⊢ ( 𝑚 ∈ ω → ( ( 𝑅1 ‘ 𝑚 ) ∈ Fin ↔ ( 𝑅1 ‘ suc 𝑚 ) ∈ Fin ) ) |
22 |
21
|
biimpd |
⊢ ( 𝑚 ∈ ω → ( ( 𝑅1 ‘ 𝑚 ) ∈ Fin → ( 𝑅1 ‘ suc 𝑚 ) ∈ Fin ) ) |
23 |
2 4 6 8 11 22
|
finds |
⊢ ( 𝐴 ∈ ω → ( 𝑅1 ‘ 𝐴 ) ∈ Fin ) |