Theorem brdomg

Description: Dominance relation. (Contributed by NM, 15-Jun-1998)

	Ref	Expression
Assertion	brdomg	$$⊢B\in C\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1eq2	$$⊢x=A\to \left(f:x\underset{1-1}{⟶}y\leftrightarrow f:A\underset{1-1}{⟶}y\right)$$
2	1	exbidv	$$⊢x=A\to \left(\exists ff:x\underset{1-1}{⟶}y\leftrightarrow \exists ff:A\underset{1-1}{⟶}y\right)$$
3		f1eq3	$$⊢y=B\to \left(f:A\underset{1-1}{⟶}y\leftrightarrow f:A\underset{1-1}{⟶}B\right)$$
4	3	exbidv	$$⊢y=B\to \left(\exists ff:A\underset{1-1}{⟶}y\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
5		df-dom	$$⊢\preccurlyeq =\left\{⟨x,y⟩|\exists ff:x\underset{1-1}{⟶}y\right\}$$
6	2 4 5	brabg	$$⊢\left(A\in \mathrm{V}\wedge B\in C\right)\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
7	6	ex	$$⊢A\in \mathrm{V}\to \left(B\in C\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)\right)$$
8		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
9	8	brrelex1i	$$⊢A\preccurlyeq B\to A\in \mathrm{V}$$
10		f1f	$$⊢f:A\underset{1-1}{⟶}B\to f:A⟶B$$
11		fdm	$$⊢f:A⟶B\to \mathrm{dom}f=A$$
12		vex	$$⊢f\in \mathrm{V}$$
13	12	dmex	$$⊢\mathrm{dom}f\in \mathrm{V}$$
14	11 13	eqeltrrdi	$$⊢f:A⟶B\to A\in \mathrm{V}$$
15	10 14	syl	$$⊢f:A\underset{1-1}{⟶}B\to A\in \mathrm{V}$$
16	15	exlimiv	$$⊢\exists ff:A\underset{1-1}{⟶}B\to A\in \mathrm{V}$$
17	9 16	pm5.21ni	$$⊢\neg A\in \mathrm{V}\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
18	17	a1d	$$⊢\neg A\in \mathrm{V}\to \left(B\in C\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)\right)$$
19	7 18	pm2.61i	$$⊢B\in C\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$