This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem domfin4

Description: A set dominated by a Dedekind finite set is Dedekind finite. (Contributed by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion domfin4 
|- ( ( A e. Fin4 /\ B ~<_ A ) -> B e. Fin4 )

Proof

Step Hyp Ref Expression
1 domeng 
 |-  ( A e. Fin4 -> ( B ~<_ A <-> E. x ( B ~~ x /\ x C_ A ) ) )
2 1 biimpa 
 |-  ( ( A e. Fin4 /\ B ~<_ A ) -> E. x ( B ~~ x /\ x C_ A ) )
3 ensym 
 |-  ( B ~~ x -> x ~~ B )
4 3 ad2antrl 
 |-  ( ( ( A e. Fin4 /\ B ~<_ A ) /\ ( B ~~ x /\ x C_ A ) ) -> x ~~ B )
5 ssfin4 
 |-  ( ( A e. Fin4 /\ x C_ A ) -> x e. Fin4 )
6 5 ad2ant2rl 
 |-  ( ( ( A e. Fin4 /\ B ~<_ A ) /\ ( B ~~ x /\ x C_ A ) ) -> x e. Fin4 )
7 fin4en1 
 |-  ( x ~~ B -> ( x e. Fin4 -> B e. Fin4 ) )
8 4 6 7 sylc 
 |-  ( ( ( A e. Fin4 /\ B ~<_ A ) /\ ( B ~~ x /\ x C_ A ) ) -> B e. Fin4 )
9 2 8 exlimddv 
 |-  ( ( A e. Fin4 /\ B ~<_ A ) -> B e. Fin4 )