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ℎ ⊆ ( ℋ ↑m ℋ )

Proof

Step	Hyp	Ref	Expression
1		dfadj2	⊢ adjℎ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) }
2		3anass	⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
3		ax-hilex	⊢ ℋ ∈ V
4	3 3	elmap	⊢ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↔ 𝑡 : ℋ ⟶ ℋ )
5	4	anbi1i	⊢ ( ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
6	2 5	bitr4i	⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
7	6	opabbii	⊢ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) } = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ) }
8	1 7	eqtri	⊢ adjℎ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ) }
9	8	dmeqi	⊢ dom adjℎ = dom { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ) }
10		dmopabss	⊢ dom { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ) } ⊆ ( ℋ ↑m ℋ )
11	9 10	eqsstri	⊢ dom adjℎ ⊆ ( ℋ ↑m ℋ )