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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		domeng	⊢ ( 𝐴 ∈ Fin → ( 𝐵 ≼ 𝐴 ↔ ∃ 𝑥 ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) )
2		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ∈ Fin )
3	2	adantrl	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝑥 ∈ Fin )
4		enfii	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≈ 𝑥 ) → 𝐵 ∈ Fin )
5	4	adantrr	⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝐵 ∈ Fin )
6	3 5	sylancom	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝐵 ∈ Fin )
7	6	ex	⊢ ( 𝐴 ∈ Fin → ( ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝐵 ∈ Fin ) )
8	7	exlimdv	⊢ ( 𝐴 ∈ Fin → ( ∃ 𝑥 ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝐵 ∈ Fin ) )
9	1 8	sylbid	⊢ ( 𝐴 ∈ Fin → ( 𝐵 ≼ 𝐴 → 𝐵 ∈ Fin ) )
10	9	imp	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ Fin )