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 ( 𝐴 ∈ ω → ( 𝑅1𝐴 ) ∈ Fin )

Proof

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 )