Theorem brdom5

Description: An equivalence to a dominance relation. (Contributed by NM, 29-Mar-2007)

	Ref	Expression
Hypothesis	brdom3.2	$$⊢B\in \mathrm{V}$$
Assertion	brdom5	$$⊢A\preccurlyeq B\leftrightarrow \exists f\left(\forall x\in B{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)$$

Proof

Step	Hyp	Ref	Expression
1		brdom3.2	$$⊢B\in \mathrm{V}$$
2	1	brdom3	$$⊢A\preccurlyeq B\leftrightarrow \exists f\left(\forall x{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)$$
3		alral	$$⊢\forall x{\exists }^{*}yxfy\to \forall x\in B{\exists }^{*}yxfy$$
4	3	anim1i	$$⊢\left(\forall x{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)\to \left(\forall x\in B{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)$$
5	4	eximi	$$⊢\exists f\left(\forall x{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)\to \exists f\left(\forall x\in B{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)$$
6	2 5	sylbi	$$⊢A\preccurlyeq B\to \exists f\left(\forall x\in B{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)$$
7		inss2	$$⊢f\cap \left(B\times A\right)\subseteq B\times A$$
8		dmss	$$⊢f\cap \left(B\times A\right)\subseteq B\times A\to \mathrm{dom}\left(f\cap \left(B\times A\right)\right)\subseteq \mathrm{dom}\left(B\times A\right)$$
9	7 8	ax-mp	$$⊢\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\subseteq \mathrm{dom}\left(B\times A\right)$$
10		dmxpss	$$⊢\mathrm{dom}\left(B\times A\right)\subseteq B$$
11	9 10	sstri	$$⊢\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\subseteq B$$
12	11	sseli	$$⊢x\in \mathrm{dom}\left(f\cap \left(B\times A\right)\right)\to x\in B$$
13		inss1	$$⊢f\cap \left(B\times A\right)\subseteq f$$
14	13	ssbri	$$⊢x\left(f\cap \left(B\times A\right)\right)y\to xfy$$
15	14	moimi	$$⊢{\exists }^{*}yxfy\to {\exists }^{*}yx\left(f\cap \left(B\times A\right)\right)y$$
16	12 15	imim12i	$$⊢\left(x\in B\to {\exists }^{*}yxfy\right)\to \left(x\in \mathrm{dom}\left(f\cap \left(B\times A\right)\right)\to {\exists }^{*}yx\left(f\cap \left(B\times A\right)\right)y\right)$$
17	16	ralimi2	$$⊢\forall x\in B{\exists }^{*}yxfy\to \forall x\in \mathrm{dom}\left(f\cap \left(B\times A\right)\right){\exists }^{*}yx\left(f\cap \left(B\times A\right)\right)y$$
18		relinxp	$$⊢\mathrm{Rel}\left(f\cap \left(B\times A\right)\right)$$
19	17 18	jctil	$$⊢\forall x\in B{\exists }^{*}yxfy\to \left(\mathrm{Rel}\left(f\cap \left(B\times A\right)\right)\wedge \forall x\in \mathrm{dom}\left(f\cap \left(B\times A\right)\right){\exists }^{*}yx\left(f\cap \left(B\times A\right)\right)y\right)$$
20		dffun7	$$⊢\mathrm{Fun}\left(f\cap \left(B\times A\right)\right)\leftrightarrow \left(\mathrm{Rel}\left(f\cap \left(B\times A\right)\right)\wedge \forall x\in \mathrm{dom}\left(f\cap \left(B\times A\right)\right){\exists }^{*}yx\left(f\cap \left(B\times A\right)\right)y\right)$$
21	19 20	sylibr	$$⊢\forall x\in B{\exists }^{*}yxfy\to \mathrm{Fun}\left(f\cap \left(B\times A\right)\right)$$
22	21	funfnd	$$⊢\forall x\in B{\exists }^{*}yxfy\to \left(f\cap \left(B\times A\right)\right)Fn\mathrm{dom}\left(f\cap \left(B\times A\right)\right)$$
23		rninxp	$$⊢\mathrm{ran}\left(f\cap \left(B\times A\right)\right)=A\leftrightarrow \forall x\in A\exists y\in Byfx$$
24	23	biimpri	$$⊢\forall x\in A\exists y\in Byfx\to \mathrm{ran}\left(f\cap \left(B\times A\right)\right)=A$$
25	22 24	anim12i	$$⊢\left(\forall x\in B{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)\to \left(\left(f\cap \left(B\times A\right)\right)Fn\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\wedge \mathrm{ran}\left(f\cap \left(B\times A\right)\right)=A\right)$$
26		df-fo	$$⊢\left(f\cap \left(B\times A\right)\right):\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\underset{onto}{⟶}A\leftrightarrow \left(\left(f\cap \left(B\times A\right)\right)Fn\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\wedge \mathrm{ran}\left(f\cap \left(B\times A\right)\right)=A\right)$$
27	25 26	sylibr	$$⊢\left(\forall x\in B{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)\to \left(f\cap \left(B\times A\right)\right):\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\underset{onto}{⟶}A$$
28		vex	$$⊢f\in \mathrm{V}$$
29	28	inex1	$$⊢f\cap \left(B\times A\right)\in \mathrm{V}$$
30	29	dmex	$$⊢\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\in \mathrm{V}$$
31	30	fodom	$$⊢\left(f\cap \left(B\times A\right)\right):\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\underset{onto}{⟶}A\to A\preccurlyeq \mathrm{dom}\left(f\cap \left(B\times A\right)\right)$$
32		ssdomg	$$⊢B\in \mathrm{V}\to \left(\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\subseteq B\to \mathrm{dom}\left(f\cap \left(B\times A\right)\right)\preccurlyeq B\right)$$
33	1 11 32	mp2	$$⊢\mathrm{dom}\left(f\cap \left(B\times A\right)\right)\preccurlyeq B$$
34		domtr	$$⊢\left(A\preccurlyeq \mathrm{dom}\left(f\cap \left(B\times A\right)\right)\wedge \mathrm{dom}\left(f\cap \left(B\times A\right)\right)\preccurlyeq B\right)\to A\preccurlyeq B$$
35	33 34	mpan2	$$⊢A\preccurlyeq \mathrm{dom}\left(f\cap \left(B\times A\right)\right)\to A\preccurlyeq B$$
36	27 31 35	3syl	$$⊢\left(\forall x\in B{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)\to A\preccurlyeq B$$
37	36	exlimiv	$$⊢\exists f\left(\forall x\in B{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)\to A\preccurlyeq B$$
38	6 37	impbii	$$⊢A\preccurlyeq B\leftrightarrow \exists f\left(\forall x\in B{\exists }^{*}yxfy\wedge \forall x\in A\exists y\in Byfx\right)$$