This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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