enssdom

Description: Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998) (Proof shortened by TM, 10-Feb-2026)

		Ref	Expression
	Assertion	enssdom	$⊢ \approx \subseteq ≼$

Step	Hyp	Ref	Expression
1		f1of1	$⊢ f : x \underset{1-1 onto}{⟶} y \to f : x \underset{1-1}{⟶} y$
2	1	eximi	$⊢ \exists f f : x \underset{1-1 onto}{⟶} y \to \exists f f : x \underset{1-1}{⟶} y$
3	2	ssopab2i	$⊢ \{⟨x, y⟩ \| \exists f f : x \underset{1-1 onto}{⟶} y\} \subseteq \{⟨x, y⟩ \| \exists f f : x \underset{1-1}{⟶} y\}$
4		df-en	$⊢ \approx = \{⟨x, y⟩ \| \exists f f : x \underset{1-1 onto}{⟶} y\}$
5		df-dom	$⊢ ≼ = \{⟨x, y⟩ \| \exists f f : x \underset{1-1}{⟶} y\}$
6	3 4 5	3sstr4i	$⊢ \approx \subseteq ≼$

Metamath Proof Explorer