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 
|- ( 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 0fin 
 |-  (/) e. Fin
11 9 10 eqeltri 
 |-  ( R1 ` (/) ) e. Fin
12 pwfi 
 |-  ( ( R1 ` m ) e. Fin <-> ~P ( R1 ` m ) e. Fin )
13 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
14 13 simpri 
 |-  Lim dom R1
15 limomss 
 |-  ( Lim dom R1 -> _om C_ dom R1 )
16 14 15 ax-mp 
 |-  _om C_ dom R1
17 16 sseli 
 |-  ( m e. _om -> m e. dom R1 )
18 r1sucg 
 |-  ( m e. dom R1 -> ( R1 ` suc m ) = ~P ( R1 ` m ) )
19 17 18 syl 
 |-  ( m e. _om -> ( R1 ` suc m ) = ~P ( R1 ` m ) )
20 19 eleq1d 
 |-  ( m e. _om -> ( ( R1 ` suc m ) e. Fin <-> ~P ( R1 ` m ) e. Fin ) )
21 12 20 bitr4id 
 |-  ( m e. _om -> ( ( R1 ` m ) e. Fin <-> ( R1 ` suc m ) e. Fin ) )
22 21 biimpd 
 |-  ( m e. _om -> ( ( R1 ` m ) e. Fin -> ( R1 ` suc m ) e. Fin ) )
23 2 4 6 8 11 22 finds 
 |-  ( A e. _om -> ( R1 ` A ) e. Fin )