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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 ≼ 𝐵 )