Theorem brdomi

Description: Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015)

	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	brrelex2i	$$⊢A\preccurlyeq B\to B\in \mathrm{V}$$
3		brdomg	$$⊢B\in \mathrm{V}\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$$