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

Metamath Proof Explorer

Theorem brdomi

Description: Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015) Avoid ax-un . (Revised by BTernaryTau, 29-Nov-2024)

		Ref	Expression
	Assertion	brdomi	$⊢ A ≼ B \to \exists f f : A \underset{1-1}{⟶} B$

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2	1	brrelex12i	$⊢ A ≼ B \to (A \in V \land B \in V)$
3		brdom2g	$⊢ (A \in V \land B \in V) \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
4	2 3	syl	$⊢ A ≼ B \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
5	4	ibi	$⊢ A ≼ B \to \exists f f : A \underset{1-1}{⟶} B$