Metamath Proof Explorer

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 
|- ( A e. _om -> ( R1 ` A ) e. Fin )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( n = (/) -> ( R1 ` n ) = ( R1 ` (/) ) )
2 1 eleq1d 
 |-  ( n = (/) -> ( ( R1 ` n ) e. Fin <-> ( R1 ` (/) ) e. Fin ) )
3 fveq2 
 |-  ( n = m -> ( R1 ` n ) = ( R1 ` m ) )
4 3 eleq1d 
 |-  ( n = m -> ( ( R1 ` n ) e. Fin <-> ( R1 ` m ) e. Fin ) )
5 fveq2 
 |-  ( n = suc m -> ( R1 ` n ) = ( R1 ` suc m ) )
6 5 eleq1d 
 |-  ( n = suc m -> ( ( R1 ` n ) e. Fin <-> ( R1 ` suc m ) e. Fin ) )
7 fveq2 
 |-  ( n = A -> ( R1 ` n ) = ( R1 ` A ) )
8 7 eleq1d 
 |-  ( n = A -> ( ( R1 ` n ) e. Fin <-> ( R1 ` A ) e. Fin ) )
9 r10 
 |-  ( R1 ` (/) ) = (/)
10 0fi 
 |-  (/) e. Fin
11 9 10 eqeltri 
 |-  ( R1 ` (/) ) e. Fin
12 pwfi 
 |-  ( ( R1 ` m ) e. Fin <-> ~P ( R1 ` m ) e. Fin )
13 r1dmlim 
 |-  Lim dom R1
14 limomss 
 |-  ( Lim dom R1 -> _om C_ dom R1 )
15 13 14 ax-mp 
 |-  _om C_ dom R1
16 15 sseli 
 |-  ( m e. _om -> m e. dom R1 )
17 r1sucg 
 |-  ( m e. dom R1 -> ( R1 ` suc m ) = ~P ( R1 ` m ) )
18 16 17 syl 
 |-  ( m e. _om -> ( R1 ` suc m ) = ~P ( R1 ` m ) )
19 18 eleq1d 
 |-  ( m e. _om -> ( ( R1 ` suc m ) e. Fin <-> ~P ( R1 ` m ) e. Fin ) )
20 12 19 bitr4id 
 |-  ( m e. _om -> ( ( R1 ` m ) e. Fin <-> ( R1 ` suc m ) e. Fin ) )
21 20 biimpd 
 |-  ( m e. _om -> ( ( R1 ` m ) e. Fin -> ( R1 ` suc m ) e. Fin ) )
22 2 4 6 8 11 21 finds 
 |-  ( A e. _om -> ( R1 ` A ) e. Fin )