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 )