Metamath Proof Explorer

Theorem r1omfi

Description: Hereditarily finite sets are finite sets. (Contributed by BTernaryTau, 30-Dec-2025)

Ref Expression
Assertion r1omfi 
|- U. ( R1 " _om ) C_ Fin

Proof

Step Hyp Ref Expression
1 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
2 1 simpli 
 |-  Fun R1
3 eluniima 
 |-  ( Fun R1 -> ( x e. U. ( R1 " _om ) <-> E. y e. _om x e. ( R1 ` y ) ) )
4 2 3 ax-mp 
 |-  ( x e. U. ( R1 " _om ) <-> E. y e. _om x e. ( R1 ` y ) )
5 r1fin 
 |-  ( y e. _om -> ( R1 ` y ) e. Fin )
6 r1pwss 
 |-  ( x e. ( R1 ` y ) -> ~P x C_ ( R1 ` y ) )
7 ssfi 
 |-  ( ( ( R1 ` y ) e. Fin /\ ~P x C_ ( R1 ` y ) ) -> ~P x e. Fin )
8 5 6 7 syl2an 
 |-  ( ( y e. _om /\ x e. ( R1 ` y ) ) -> ~P x e. Fin )
9 8 rexlimiva 
 |-  ( E. y e. _om x e. ( R1 ` y ) -> ~P x e. Fin )
10 pwfir 
 |-  ( ~P x e. Fin -> x e. Fin )
11 9 10 syl 
 |-  ( E. y e. _om x e. ( R1 ` y ) -> x e. Fin )
12 4 11 sylbi 
 |-  ( x e. U. ( R1 " _om ) -> x e. Fin )
13 12 ssriv 
 |-  U. ( R1 " _om ) C_ Fin