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 ( ( 𝐴 ∈ 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 )