Metamath Proof Explorer

Theorem ssdomfi

Description: A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg ). (Contributed by BTernaryTau, 12-Nov-2024)

		Ref	Expression
	Assertion	ssdomfi	$⊢ B \in Fin \to (A \subseteq B \to A ≼ B)$

Proof

Step	Hyp	Ref	Expression
1		f1oi	$⊢ ({I ↾}_{A}) : A \underset{1-1 onto}{⟶} A$
2		f1of1	$⊢ ({I ↾}_{A}) : A \underset{1-1 onto}{⟶} A \to ({I ↾}_{A}) : A \underset{1-1}{⟶} A$
3	1 2	ax-mp	$⊢ ({I ↾}_{A}) : A \underset{1-1}{⟶} A$
4		f1ss	$⊢ (({I ↾}_{A}) : A \underset{1-1}{⟶} A \land A \subseteq B) \to ({I ↾}_{A}) : A \underset{1-1}{⟶} B$
5	3 4	mpan	$⊢ A \subseteq B \to ({I ↾}_{A}) : A \underset{1-1}{⟶} B$
6		f1domfi	$⊢ (B \in Fin \land ({I ↾}_{A}) : A \underset{1-1}{⟶} B) \to A ≼ B$
7	5 6	sylan2	$⊢ (B \in Fin \land A \subseteq B) \to A ≼ B$
8	7	ex	$⊢ B \in Fin \to (A \subseteq B \to A ≼ B)$