Theorem r1fin

Description: The first _om stages of the cumulative hierarchy of sets 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		r1dmlim	⊢ Lim dom 𝑅1
14		limomss	⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
15	13 14	ax-mp	⊢ ω ⊆ dom 𝑅1
16	15	sseli	⊢ ( 𝑚 ∈ ω → 𝑚 ∈ dom 𝑅1 )
17		r1sucg	⊢ ( 𝑚 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑚 ) = 𝒫 ( 𝑅1 ‘ 𝑚 ) )
18	16 17	syl	⊢ ( 𝑚 ∈ ω → ( 𝑅1 ‘ suc 𝑚 ) = 𝒫 ( 𝑅1 ‘ 𝑚 ) )
19	18	eleq1d	⊢ ( 𝑚 ∈ ω → ( ( 𝑅1 ‘ suc 𝑚 ) ∈ Fin ↔ 𝒫 ( 𝑅1 ‘ 𝑚 ) ∈ Fin ) )
20	12 19	bitr4id	⊢ ( 𝑚 ∈ ω → ( ( 𝑅1 ‘ 𝑚 ) ∈ Fin ↔ ( 𝑅1 ‘ suc 𝑚 ) ∈ Fin ) )
21	20	biimpd	⊢ ( 𝑚 ∈ ω → ( ( 𝑅1 ‘ 𝑚 ) ∈ Fin → ( 𝑅1 ‘ suc 𝑚 ) ∈ Fin ) )
22	2 4 6 8 11 21	finds	⊢ ( 𝐴 ∈ ω → ( 𝑅1 ‘ 𝐴 ) ∈ Fin )