Theorem dom2d

Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004) (Revised by Mario Carneiro, 20-May-2013)

	Ref	Expression
Hypotheses	dom2d.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
	dom2d.2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) ) )
Assertion	dom2d	⊢ ( 𝜑 → ( 𝐵 ∈ 𝑅 → 𝐴 ≼ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dom2d.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
2		dom2d.2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) ) )
3	1 2	dom2lem	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1→ 𝐵 )
4		f1domg	⊢ ( 𝐵 ∈ 𝑅 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1→ 𝐵 → 𝐴 ≼ 𝐵 ) )
5	3 4	syl5com	⊢ ( 𝜑 → ( 𝐵 ∈ 𝑅 → 𝐴 ≼ 𝐵 ) )