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	$⊢ φ \to (x \in A \to C \in B)$
		dom2d.2	$⊢ φ \to ((x \in A \land y \in A) \to (C = D \leftrightarrow x = y))$
		dom3d.3	$⊢ φ \to A \in V$
		dom3d.4	$⊢ φ \to B \in W$
	Assertion	dom3d	$⊢ φ \to A ≼ B$

Proof

Step	Hyp	Ref	Expression
1		dom2d.1	$⊢ φ \to (x \in A \to C \in B)$
2		dom2d.2	$⊢ φ \to ((x \in A \land y \in A) \to (C = D \leftrightarrow x = y))$
3		dom3d.3	$⊢ φ \to A \in V$
4		dom3d.4	$⊢ φ \to B \in W$
5	1 2	dom2lem	$⊢ φ \to (x \in A ⟼ C) : A \underset{1-1}{⟶} B$
6		f1f	$⊢ (x \in A ⟼ C) : A \underset{1-1}{⟶} B \to (x \in A ⟼ C) : A ⟶ B$
7	5 6	syl	$⊢ φ \to (x \in A ⟼ C) : A ⟶ B$
8		fex2	$⊢ ((x \in A ⟼ C) : A ⟶ B \land A \in V \land B \in W) \to (x \in A ⟼ C) \in V$
9	7 3 4 8	syl3anc	$⊢ φ \to (x \in A ⟼ C) \in V$
10		f1eq1	$⊢ z = (x \in A ⟼ C) \to (z : A \underset{1-1}{⟶} B \leftrightarrow (x \in A ⟼ C) : A \underset{1-1}{⟶} B)$
11	9 5 10	spcedv	$⊢ φ \to \exists z z : A \underset{1-1}{⟶} B$
12		brdomg	$⊢ B \in W \to (A ≼ B \leftrightarrow \exists z z : A \underset{1-1}{⟶} B)$
13	4 12	syl	$⊢ φ \to (A ≼ B \leftrightarrow \exists z z : A \underset{1-1}{⟶} B)$
14	11 13	mpbird	$⊢ φ \to A ≼ B$