This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 0fi ⊢ ∅ ∈ 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 )