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 )