Metamath Proof Explorer

Theorem fineqvr1ombregs

Description: All sets are finite iff all sets are hereditarily finite. (Contributed by BTernaryTau, 30-Dec-2025)

Ref Expression
Assertion fineqvr1ombregs 
|- ( Fin = _V <-> U. ( R1 " _om ) = _V )

Proof

Step Hyp Ref Expression
1 fineqvomon 
 |-  ( Fin = _V -> _om = On )
2 1 imaeq2d 
 |-  ( Fin = _V -> ( R1 " _om ) = ( R1 " On ) )
3 2 unieqd 
 |-  ( Fin = _V -> U. ( R1 " _om ) = U. ( R1 " On ) )
4 unir1regs 
 |-  U. ( R1 " On ) = _V
5 3 4 eqtrdi 
 |-  ( Fin = _V -> U. ( R1 " _om ) = _V )
6 r1omfi 
 |-  U. ( R1 " _om ) C_ Fin
7 sseq1 
 |-  ( U. ( R1 " _om ) = _V -> ( U. ( R1 " _om ) C_ Fin <-> _V C_ Fin ) )
8 6 7 mpbii 
 |-  ( U. ( R1 " _om ) = _V -> _V C_ Fin )
9 vss 
 |-  ( _V C_ Fin <-> Fin = _V )
10 8 9 sylib 
 |-  ( U. ( R1 " _om ) = _V -> Fin = _V )
11 5 10 impbii 
 |-  ( Fin = _V <-> U. ( R1 " _om ) = _V )