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 ) |
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 ) |