Theorem adjeu

Description: Elementhood in the domain of the adjoint function. (Contributed by Mario Carneiro, 11-Sep-2015) (Revised by Mario Carneiro, 24-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	adjeu	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(T\in \mathrm{dom}{adj}_h\leftrightarrow \exists !u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
2		fex2	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge \mathscr{H}\in \mathrm{V}\wedge \mathscr{H}\in \mathrm{V}\right)\to T\in \mathrm{V}$$
3	1 1 2	mp3an23	$$⊢T:\mathscr{H}⟶\mathscr{H}\to T\in \mathrm{V}$$
4		feq1	$$⊢t=T\to \left(t:\mathscr{H}⟶\mathscr{H}\leftrightarrow T:\mathscr{H}⟶\mathscr{H}\right)$$
5		fveq1	$$⊢t=T\to t\left(y\right)=T\left(y\right)$$
6	5	oveq2d	$$⊢t=T\to x{\cdot }_{\mathrm{ih}}t\left(y\right)=x{\cdot }_{\mathrm{ih}}T\left(y\right)$$
7	6	eqeq1d	$$⊢t=T\to \left(x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\leftrightarrow x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
8	7	2ralbidv	$$⊢t=T\to \left(\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\leftrightarrow \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
9	4 8	3anbi13d	$$⊢t=T\to \left(\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)$$
10		3anass	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)$$
11	9 10	bitrdi	$$⊢t=T\to \left(\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)\right)$$
12	11	exbidv	$$⊢t=T\to \left(\exists u\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\leftrightarrow \exists u\left(T:\mathscr{H}⟶\mathscr{H}\wedge \left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)\right)$$
13		19.42v	$$⊢\exists u\left(T:\mathscr{H}⟶\mathscr{H}\wedge \left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \exists u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)$$
14	12 13	bitrdi	$$⊢t=T\to \left(\exists u\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \exists u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)\right)$$
15		dfadj2	$$⊢{adj}_h=\left\{⟨t,u⟩|\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right\}$$
16	15	dmeqi	$$⊢\mathrm{dom}{adj}_h=\mathrm{dom}\left\{⟨t,u⟩|\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right\}$$
17		dmopab	$$⊢\mathrm{dom}\left\{⟨t,u⟩|\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right\}=\left\{t|\exists u\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right\}$$
18	16 17	eqtri	$$⊢\mathrm{dom}{adj}_h=\left\{t|\exists u\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right\}$$
19	14 18	elab2g	$$⊢T\in \mathrm{V}\to \left(T\in \mathrm{dom}{adj}_h\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \exists u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)\right)$$
20	19	baibd	$$⊢\left(T\in \mathrm{V}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(T\in \mathrm{dom}{adj}_h\leftrightarrow \exists u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)$$
21	3 20	mpancom	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(T\in \mathrm{dom}{adj}_h\leftrightarrow \exists u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)$$
22		df-reu	$$⊢\exists !u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\leftrightarrow \exists !u\left(u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
23	1 1	elmap	$$⊢u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\leftrightarrow u:\mathscr{H}⟶\mathscr{H}$$
24	23	anbi1i	$$⊢\left(u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\leftrightarrow \left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
25	24	eubii	$$⊢\exists !u\left(u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\leftrightarrow \exists !u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
26		adjmo	$$⊢{\exists }^{*}u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
27		df-eu	$$⊢\exists !u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\leftrightarrow \left(\exists u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\wedge {\exists }^{*}u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)$$
28	26 27	mpbiran2	$$⊢\exists !u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\leftrightarrow \exists u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
29	22 25 28	3bitri	$$⊢\exists !u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\leftrightarrow \exists u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
30	21 29	bitr4di	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(T\in \mathrm{dom}{adj}_h\leftrightarrow \exists !u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$