Metamath Proof Explorer


Theorem adjadj

Description: Double adjoint. Theorem 3.11(iv) of Beran p. 106. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjadj TdomadjhadjhadjhT=T

Proof

Step Hyp Ref Expression
1 adj2 TdomadjhxyTxihy=xihadjhTy
2 dmadjrn TdomadjhadjhTdomadjh
3 adj1 adjhTdomadjhxyxihadjhTy=adjhadjhTxihy
4 2 3 syl3an1 TdomadjhxyxihadjhTy=adjhadjhTxihy
5 1 4 eqtr2d TdomadjhxyadjhadjhTxihy=Txihy
6 5 3expib TdomadjhxyadjhadjhTxihy=Txihy
7 6 ralrimivv TdomadjhxyadjhadjhTxihy=Txihy
8 dmadjrn adjhTdomadjhadjhadjhTdomadjh
9 dmadjop adjhadjhTdomadjhadjhadjhT:
10 2 8 9 3syl TdomadjhadjhadjhT:
11 dmadjop TdomadjhT:
12 hoeq1 adjhadjhT:T:xyadjhadjhTxihy=TxihyadjhadjhT=T
13 10 11 12 syl2anc TdomadjhxyadjhadjhTxihy=TxihyadjhadjhT=T
14 7 13 mpbid TdomadjhadjhadjhT=T