Theorem ajmoi

Description: Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip2eqi.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	ip2eqi.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
	ip2eqi.u	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
Assertion	ajmoi	$$⊢{\exists }^{*}s\left(s:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ip2eqi.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		ip2eqi.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
3		ip2eqi.u	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
4		r19.26-2	$$⊢\forall x\in X\forall y\in Y\left(T\left(x\right)Qy=xPs\left(y\right)\wedge T\left(x\right)Qy=xPt\left(y\right)\right)\leftrightarrow \left(\forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPt\left(y\right)\right)$$
5		eqtr2	$$⊢\left(T\left(x\right)Qy=xPs\left(y\right)\wedge T\left(x\right)Qy=xPt\left(y\right)\right)\to xPs\left(y\right)=xPt\left(y\right)$$
6	5	2ralimi	$$⊢\forall x\in X\forall y\in Y\left(T\left(x\right)Qy=xPs\left(y\right)\wedge T\left(x\right)Qy=xPt\left(y\right)\right)\to \forall x\in X\forall y\in YxPs\left(y\right)=xPt\left(y\right)$$
7	4 6	sylbir	$$⊢\left(\forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPt\left(y\right)\right)\to \forall x\in X\forall y\in YxPs\left(y\right)=xPt\left(y\right)$$
8	1 2 3	phoeqi	$$⊢\left(s:Y⟶X\wedge t:Y⟶X\right)\to \left(\forall x\in X\forall y\in YxPs\left(y\right)=xPt\left(y\right)\leftrightarrow s=t\right)$$
9	8	biimpa	$$⊢\left(\left(s:Y⟶X\wedge t:Y⟶X\right)\wedge \forall x\in X\forall y\in YxPs\left(y\right)=xPt\left(y\right)\right)\to s=t$$
10	7 9	sylan2	$$⊢\left(\left(s:Y⟶X\wedge t:Y⟶X\right)\wedge \left(\forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPt\left(y\right)\right)\right)\to s=t$$
11	10	an4s	$$⊢\left(\left(s:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\right)\wedge \left(t:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPt\left(y\right)\right)\right)\to s=t$$
12	11	gen2	$$⊢\forall s\forall t\left(\left(\left(s:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\right)\wedge \left(t:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPt\left(y\right)\right)\right)\to s=t\right)$$
13		feq1	$$⊢s=t\to \left(s:Y⟶X\leftrightarrow t:Y⟶X\right)$$
14		fveq1	$$⊢s=t\to s\left(y\right)=t\left(y\right)$$
15	14	oveq2d	$$⊢s=t\to xPs\left(y\right)=xPt\left(y\right)$$
16	15	eqeq2d	$$⊢s=t\to \left(T\left(x\right)Qy=xPs\left(y\right)\leftrightarrow T\left(x\right)Qy=xPt\left(y\right)\right)$$
17	16	2ralbidv	$$⊢s=t\to \left(\forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\leftrightarrow \forall x\in X\forall y\in YT\left(x\right)Qy=xPt\left(y\right)\right)$$
18	13 17	anbi12d	$$⊢s=t\to \left(\left(s:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\right)\leftrightarrow \left(t:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPt\left(y\right)\right)\right)$$
19	18	mo4	$$⊢{\exists }^{*}s\left(s:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\right)\leftrightarrow \forall s\forall t\left(\left(\left(s:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\right)\wedge \left(t:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPt\left(y\right)\right)\right)\to s=t\right)$$
20	12 19	mpbir	$$⊢{\exists }^{*}s\left(s:Y⟶X\wedge \forall x\in X\forall y\in YT\left(x\right)Qy=xPs\left(y\right)\right)$$