This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dom2

Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. C and D can be read C ( x ) and D ( y ) , as can be inferred from their distinct variable conditions. (Contributed by NM, 26-Oct-2003)

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

Proof

Step	Hyp	Ref	Expression
1		dom2.1	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 )
2		dom2.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) )
3		eqid	⊢ 𝐴 = 𝐴
4	1	a1i	⊢ ( 𝐴 = 𝐴 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
5	2	a1i	⊢ ( 𝐴 = 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) ) )
6	4 5	dom2d	⊢ ( 𝐴 = 𝐴 → ( 𝐵 ∈ 𝑉 → 𝐴 ≼ 𝐵 ) )
7	3 6	ax-mp	⊢ ( 𝐵 ∈ 𝑉 → 𝐴 ≼ 𝐵 )