Metamath Proof Explorer

Theorem funadj

Description: Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion funadj ⊢ Fun ⁡ adj h

Proof

Step Hyp Ref Expression
1 funopab ⊢ Fun ⁡ 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
2 adjmo ⊢ ∃* u u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
3 3simpc ⊢ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y → u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
4 3 moimi ⊢ ∃* u u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y → ∃* u t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
5 2 4 ax-mp ⊢ ∃* u t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
6 1 5 mpgbir ⊢ Fun ⁡ t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
7 dfadj2 ⊢ adj h = t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
8 7 funeqi ⊢ Fun ⁡ adj h ↔ Fun ⁡ t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
9 6 8 mpbir ⊢ Fun ⁡ adj h