Theorem brdomg

Description: Dominance relation. (Contributed by NM, 15-Jun-1998) (Proof shortened by BTernaryTau, 29-Nov-2024)

	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		brdom2g	$$⊢\left(A\in \mathrm{V}\wedge B\in C\right)\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
2	1	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)$$
3		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
4	3	brrelex1i	$$⊢A\preccurlyeq B\to A\in \mathrm{V}$$
5		f1f	$$⊢f:A\underset{1-1}{⟶}B\to f:A⟶B$$
6		fdm	$$⊢f:A⟶B\to \mathrm{dom}f=A$$
7		vex	$$⊢f\in \mathrm{V}$$
8	7	dmex	$$⊢\mathrm{dom}f\in \mathrm{V}$$
9	6 8	eqeltrrdi	$$⊢f:A⟶B\to A\in \mathrm{V}$$
10	5 9	syl	$$⊢f:A\underset{1-1}{⟶}B\to A\in \mathrm{V}$$
11	10	exlimiv	$$⊢\exists ff:A\underset{1-1}{⟶}B\to A\in \mathrm{V}$$
12	4 11	pm5.21ni	$$⊢\neg A\in \mathrm{V}\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
13	12	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)$$
14	2 13	pm2.61i	$$⊢B\in C\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$