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\preccurlyeq B\to \exists ff:A\underset{1-1}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
2	1	brrelex12i	$$⊢A\preccurlyeq B\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
3		brdom2g	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
4	2 3	syl	$$⊢A\preccurlyeq B\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
5	4	ibi	$$⊢A\preccurlyeq B\to \exists ff:A\underset{1-1}{⟶}B$$