domfin4

Description: A set dominated by a Dedekind finite set is Dedekind finite. (Contributed by Mario Carneiro, 16-May-2015)

		Ref	Expression
	Assertion	domfin4	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ Fin^IV )

Step	Hyp	Ref	Expression
1		domeng	⊢ ( 𝐴 ∈ Fin^IV → ( 𝐵 ≼ 𝐴 ↔ ∃ 𝑥 ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) )
2	1	biimpa	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ≼ 𝐴 ) → ∃ 𝑥 ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) )
3		ensym	⊢ ( 𝐵 ≈ 𝑥 → 𝑥 ≈ 𝐵 )
4	3	ad2antrl	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ≼ 𝐴 ) ∧ ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝑥 ≈ 𝐵 )
5		ssfin4	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ∈ Fin^IV )
6	5	ad2ant2rl	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ≼ 𝐴 ) ∧ ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝑥 ∈ Fin^IV )
7		fin4en1	⊢ ( 𝑥 ≈ 𝐵 → ( 𝑥 ∈ Fin^IV → 𝐵 ∈ Fin^IV ) )
8	4 6 7	sylc	⊢ ( ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ≼ 𝐴 ) ∧ ( 𝐵 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝐵 ∈ Fin^IV )
9	2 8	exlimddv	⊢ ( ( 𝐴 ∈ Fin^IV ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ Fin^IV )

Metamath Proof Explorer