Metamath Proof Explorer

Theorem domen

Description: Dominance in terms of equinumerosity. Example 1 of Enderton p. 146. (Contributed by NM, 15-Jun-1998)

		Ref	Expression
	Hypothesis	bren.1	$⊢ B \in V$
	Assertion	domen	$⊢ A ≼ B \leftrightarrow \exists x (A \approx x \land x \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		bren.1	$⊢ B \in V$
2	1	brdom	$⊢ A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B$
3		vex	$⊢ f \in V$
4	3	f11o	$⊢ f : A \underset{1-1}{⟶} B \leftrightarrow \exists x (f : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$
5	4	exbii	$⊢ \exists f f : A \underset{1-1}{⟶} B \leftrightarrow \exists f \exists x (f : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$
6		excom	$⊢ \exists f \exists x (f : A \underset{1-1 onto}{⟶} x \land x \subseteq B) \leftrightarrow \exists x \exists f (f : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$
7	5 6	bitri	$⊢ \exists f f : A \underset{1-1}{⟶} B \leftrightarrow \exists x \exists f (f : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$
8		bren	$⊢ A \approx x \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} x$
9	8	anbi1i	$⊢ (A \approx x \land x \subseteq B) \leftrightarrow (\exists f f : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$
10		19.41v	$⊢ \exists f (f : A \underset{1-1 onto}{⟶} x \land x \subseteq B) \leftrightarrow (\exists f f : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$
11	9 10	bitr4i	$⊢ (A \approx x \land x \subseteq B) \leftrightarrow \exists f (f : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$
12	11	exbii	$⊢ \exists x (A \approx x \land x \subseteq B) \leftrightarrow \exists x \exists f (f : A \underset{1-1 onto}{⟶} x \land x \subseteq B)$
13	7 12	bitr4i	$⊢ \exists f f : A \underset{1-1}{⟶} B \leftrightarrow \exists x (A \approx x \land x \subseteq B)$
14	2 13	bitri	$⊢ A ≼ B \leftrightarrow \exists x (A \approx x \land x \subseteq B)$