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 )