Metamath Proof Explorer

Theorem fin1a2lem8

Description: Lemma for fin1a2 . Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Assertion fin1a2lem8 
|- ( ( A e. V /\ A. x e. ~P A ( x e. Fin3 \/ ( A \ x ) e. Fin3 ) ) -> A e. Fin3 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( y e. _om |-> ( 2o .o y ) ) = ( y e. _om |-> ( 2o .o y ) )
2 eqid 
 |-  ( y e. On |-> suc y ) = ( y e. On |-> suc y )
3 1 2 fin1a2lem7 
 |-  ( ( A e. V /\ A. x e. ~P A ( x e. Fin3 \/ ( A \ x ) e. Fin3 ) ) -> A e. Fin3 )