Theorem brdomiOLD

Description: Obsolete version of brdomi as of 29-Nov-2024. (Contributed by Mario Carneiro, 26-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	brdomiOLD	$$⊢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$$