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 syl6bb ⊢ 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 syl6bb ⊢ 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