Theorem dom3d

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

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

Proof

Step	Hyp	Ref	Expression
1		dom2d.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
2		dom2d.2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) ) )
3		dom3d.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		dom3d.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5	1 2	dom2lem	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1→ 𝐵 )
6		f1f	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1→ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 )
7	5 6	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 )
8		fex2	⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ V )
9	7 3 4 8	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ V )
10		f1eq1	⊢ ( 𝑧 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( 𝑧 : 𝐴 –1-1→ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1→ 𝐵 ) )
11	9 5 10	spcedv	⊢ ( 𝜑 → ∃ 𝑧 𝑧 : 𝐴 –1-1→ 𝐵 )
12		brdomg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑧 𝑧 : 𝐴 –1-1→ 𝐵 ) )
13	4 12	syl	⊢ ( 𝜑 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑧 𝑧 : 𝐴 –1-1→ 𝐵 ) )
14	11 13	mpbird	⊢ ( 𝜑 → 𝐴 ≼ 𝐵 )