# Metamath Proof Explorer

## Theorem r1fin

Description: The first _om levels of the cumulative hierarchy are all finite. (Contributed by Mario Carneiro, 15-May-2013)

Ref Expression
Assertion r1fin $⊢ A ∈ ω → R1 ⁡ A ∈ Fin$

### Proof

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