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 ⊢ φ → x ∈ A → C ∈ B
dom2d.2 ⊢ φ → x ∈ A ∧ y ∈ A → C = D ↔ x = y
dom3d.3 ⊢ φ → A ∈ V
dom3d.4 ⊢ φ → B ∈ W
Assertion dom3d ⊢ φ → A ≼ B

Proof

Step Hyp Ref Expression
1 dom2d.1 ⊢ φ → x ∈ A → C ∈ B
2 dom2d.2 ⊢ φ → x ∈ A ∧ y ∈ A → C = D ↔ x = y
3 dom3d.3 ⊢ φ → A ∈ V
4 dom3d.4 ⊢ φ → B ∈ W
5 1 2 dom2lem ⊢ φ → x ∈ A ⟼ C : A ⟶ 1-1 B
6 f1f ⊢ x ∈ A ⟼ C : A ⟶ 1-1 B → x ∈ A ⟼ C : A ⟶ B
7 5 6 syl ⊢ φ → x ∈ A ⟼ C : A ⟶ B
8 fex2 ⊢ x ∈ A ⟼ C : A ⟶ B ∧ A ∈ V ∧ B ∈ W → x ∈ A ⟼ C ∈ V
9 7 3 4 8 syl3anc ⊢ φ → x ∈ A ⟼ C ∈ V
10 f1eq1 ⊢ z = x ∈ A ⟼ C → z : A ⟶ 1-1 B ↔ x ∈ A ⟼ C : A ⟶ 1-1 B
11 9 5 10 spcedv ⊢ φ → ∃ z z : A ⟶ 1-1 B
12 brdomg ⊢ B ∈ W → A ≼ B ↔ ∃ z z : A ⟶ 1-1 B
13 4 12 syl ⊢ φ → A ≼ B ↔ ∃ z z : A ⟶ 1-1 B
14 11 13 mpbird ⊢ φ → A ≼ B