Theorem enssdom

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

	Ref	Expression
Assertion	enssdom	⊢ ≈ ⊆ ≼

Proof

Step	Hyp	Ref	Expression
1		f1of1	⊢ ( 𝑓 : 𝑥 –1-1-onto→ 𝑦 → 𝑓 : 𝑥 –1-1→ 𝑦 )
2	1	eximi	⊢ ( ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 → ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 )
3	2	ssopab2i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 }
4		df-en	⊢ ≈ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 }
5		df-dom	⊢ ≼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 }
6	3 4 5	3sstr4i	⊢ ≈ ⊆ ≼