Theorem enssdom

Description: Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998)

	Ref	Expression
Assertion	enssdom	⊢ ≈ ⊆ ≼

Proof

Step	Hyp	Ref	Expression
1		relen	⊢ Rel ≈
2		f1of1	⊢ ( 𝑓 : 𝑥 –1-1-onto→ 𝑦 → 𝑓 : 𝑥 –1-1→ 𝑦 )
3	2	eximi	⊢ ( ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 → ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 )
4		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 } ↔ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 )
5		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 } ↔ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 )
6	3 4 5	3imtr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 } → ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 } )
7		df-en	⊢ ≈ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 }
8	7	eleq2i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ≈ ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 } )
9		df-dom	⊢ ≼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 }
10	9	eleq2i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ≼ ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 } )
11	6 8 10	3imtr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ≈ → ⟨ 𝑥 , 𝑦 ⟩ ∈ ≼ )
12	1 11	relssi	⊢ ≈ ⊆ ≼