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

Metamath Proof Explorer

Theorem domfi

Description: A set dominated by a finite set is finite. (Contributed by NM, 23-Mar-2006) (Revised by Mario Carneiro, 12-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 domeng 
 |-  ( A e. Fin -> ( B ~<_ A <-> E. x ( B ~~ x /\ x C_ A ) ) )
2 ssfi 
 |-  ( ( A e. Fin /\ x C_ A ) -> x e. Fin )
3 2 adantrl 
 |-  ( ( A e. Fin /\ ( B ~~ x /\ x C_ A ) ) -> x e. Fin )
4 enfii 
 |-  ( ( x e. Fin /\ B ~~ x ) -> B e. Fin )
5 4 adantrr 
 |-  ( ( x e. Fin /\ ( B ~~ x /\ x C_ A ) ) -> B e. Fin )
6 3 5 sylancom 
 |-  ( ( A e. Fin /\ ( B ~~ x /\ x C_ A ) ) -> B e. Fin )
7 6 ex 
 |-  ( A e. Fin -> ( ( B ~~ x /\ x C_ A ) -> B e. Fin ) )
8 7 exlimdv 
 |-  ( A e. Fin -> ( E. x ( B ~~ x /\ x C_ A ) -> B e. Fin ) )
9 1 8 sylbid 
 |-  ( A e. Fin -> ( B ~<_ A -> B e. Fin ) )
10 9 imp 
 |-  ( ( A e. Fin /\ B ~<_ A ) -> B e. Fin )