Metamath Proof Explorer


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 : T dom adj h ∃! u x y x ih T y = u x ih y

Proof

Step Hyp Ref Expression
1 ax-hilex V
2 fex2 T : V V T V
3 1 1 2 mp3an23 T : T V
4 feq1 t = T t : T :
5 fveq1 t = T t y = T y
6 5 oveq2d t = T x ih t y = x ih T y
7 6 eqeq1d t = T x ih t y = u x ih y x ih T y = u x ih y
8 7 2ralbidv t = T x y x ih t y = u x ih y x y x ih T y = u x ih y
9 4 8 3anbi13d t = T t : u : x y x ih t y = u x ih y T : u : x y x ih T y = u x ih y
10 3anass T : u : x y x ih T y = u x ih y T : u : x y x ih T y = u x ih y
11 9 10 bitrdi t = T t : u : x y x ih t y = u x ih y T : u : x y x ih T y = u x ih y
12 11 exbidv t = T u t : u : x y x ih t y = u x ih y u T : u : x y x ih T y = u x ih y
13 19.42v u T : u : x y x ih T y = u x ih y T : u u : x y x ih T y = u x ih y
14 12 13 bitrdi t = T u t : u : x y x ih t y = u x ih y T : u u : x y x ih T y = u x ih y
15 dfadj2 adj h = t u | t : u : x y x ih t y = u x ih y
16 15 dmeqi dom adj h = dom t u | t : u : x y x ih t y = u x ih y
17 dmopab dom t u | t : u : x y x ih t y = u x ih y = t | u t : u : x y x ih t y = u x ih y
18 16 17 eqtri dom adj h = t | u t : u : x y x ih t y = u x ih y
19 14 18 elab2g T V T dom adj h T : u u : x y x ih T y = u x ih y
20 19 baibd T V T : T dom adj h u u : x y x ih T y = u x ih y
21 3 20 mpancom T : T dom adj h u u : x y x ih T y = u x ih y
22 df-reu ∃! u x y x ih T y = u x ih y ∃! u u x y x ih T y = u x ih y
23 1 1 elmap u u :
24 23 anbi1i u x y x ih T y = u x ih y u : x y x ih T y = u x ih y
25 24 eubii ∃! u u x y x ih T y = u x ih y ∃! u u : x y x ih T y = u x ih y
26 adjmo * u u : x y x ih T y = u x ih y
27 df-eu ∃! u u : x y x ih T y = u x ih y u u : x y x ih T y = u x ih y * u u : x y x ih T y = u x ih y
28 26 27 mpbiran2 ∃! u u : x y x ih T y = u x ih y u u : x y x ih T y = u x ih y
29 22 25 28 3bitri ∃! u x y x ih T y = u x ih y u u : x y x ih T y = u x ih y
30 21 29 bitr4di T : T dom adj h ∃! u x y x ih T y = u x ih y