Theorem brwdom

Description: Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	brwdom	$$⊢Y\in V\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢Y\in V\to Y\in \mathrm{V}$$
2		relwdom	$$⊢\mathrm{Rel}{\preccurlyeq }^{*}$$
3	2	brrelex1i	$$⊢X{\preccurlyeq }^{*}Y\to X\in \mathrm{V}$$
4	3	a1i	$$⊢Y\in \mathrm{V}\to \left(X{\preccurlyeq }^{*}Y\to X\in \mathrm{V}\right)$$
5		0ex	$$⊢\varnothing \in \mathrm{V}$$
6		eleq1a	$$⊢\varnothing \in \mathrm{V}\to \left(X=\varnothing \to X\in \mathrm{V}\right)$$
7	5 6	ax-mp	$$⊢X=\varnothing \to X\in \mathrm{V}$$
8		forn	$$⊢z:Y\underset{onto}{⟶}X\to \mathrm{ran}z=X$$
9		vex	$$⊢z\in \mathrm{V}$$
10	9	rnex	$$⊢\mathrm{ran}z\in \mathrm{V}$$
11	8 10	eqeltrrdi	$$⊢z:Y\underset{onto}{⟶}X\to X\in \mathrm{V}$$
12	11	exlimiv	$$⊢\exists zz:Y\underset{onto}{⟶}X\to X\in \mathrm{V}$$
13	7 12	jaoi	$$⊢\left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\to X\in \mathrm{V}$$
14	13	a1i	$$⊢Y\in \mathrm{V}\to \left(\left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\to X\in \mathrm{V}\right)$$
15		eqeq1	$$⊢x=X\to \left(x=\varnothing \leftrightarrow X=\varnothing \right)$$
16		foeq3	$$⊢x=X\to \left(z:y\underset{onto}{⟶}x\leftrightarrow z:y\underset{onto}{⟶}X\right)$$
17	16	exbidv	$$⊢x=X\to \left(\exists zz:y\underset{onto}{⟶}x\leftrightarrow \exists zz:y\underset{onto}{⟶}X\right)$$
18	15 17	orbi12d	$$⊢x=X\to \left(\left(x=\varnothing \vee \exists zz:y\underset{onto}{⟶}x\right)\leftrightarrow \left(X=\varnothing \vee \exists zz:y\underset{onto}{⟶}X\right)\right)$$
19		foeq2	$$⊢y=Y\to \left(z:y\underset{onto}{⟶}X\leftrightarrow z:Y\underset{onto}{⟶}X\right)$$
20	19	exbidv	$$⊢y=Y\to \left(\exists zz:y\underset{onto}{⟶}X\leftrightarrow \exists zz:Y\underset{onto}{⟶}X\right)$$
21	20	orbi2d	$$⊢y=Y\to \left(\left(X=\varnothing \vee \exists zz:y\underset{onto}{⟶}X\right)\leftrightarrow \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\right)$$
22		df-wdom	$$⊢{\preccurlyeq }^{*}=\left\{⟨x,y⟩|\left(x=\varnothing \vee \exists zz:y\underset{onto}{⟶}x\right)\right\}$$
23	18 21 22	brabg	$$⊢\left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\right)$$
24	23	expcom	$$⊢Y\in \mathrm{V}\to \left(X\in \mathrm{V}\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\right)\right)$$
25	4 14 24	pm5.21ndd	$$⊢Y\in \mathrm{V}\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\right)$$
26	1 25	syl	$$⊢Y\in V\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\right)$$