# 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$