Metamath Proof Explorer

Theorem dmadjss

Description: The domain of the adjoint function is a subset of the maps from ~H to ~H . (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion dmadjss ⊢ dom ⁡ adj h ⊆ ℋ ℋ

Proof

Step Hyp Ref Expression
1 dfadj2 ⊢ adj h = t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
2 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
3 ax-hilex ⊢ ℋ ∈ V
4 3 3 elmap ⊢ t ∈ ℋ ℋ ↔ t : ℋ ⟶ ℋ
5 4 anbi1i ⊢ t ∈ ℋ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y ↔ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
6 2 5 bitr4i ⊢ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y ↔ t ∈ ℋ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
7 6 opabbii ⊢ 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
8 1 7 eqtri ⊢ adj h = t u | t ∈ ℋ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
9 8 dmeqi ⊢ dom ⁡ adj h = dom ⁡ t u | t ∈ ℋ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
10 dmopabss ⊢ dom ⁡ t u | t ∈ ℋ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y ⊆ ℋ ℋ
11 9 10 eqsstri ⊢ dom ⁡ adj h ⊆ ℋ ℋ