Theorem funadj

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

	Ref	Expression
Assertion	funadj	⊢ Fun adjℎ

Proof

Step	Hyp	Ref	Expression
1		funopab	⊢ ( Fun { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) } ↔ ∀ 𝑡 ∃* 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) )
2		adjmo	⊢ ∃* 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) )
3		3simpc	⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) → ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) )
4	3	moimi	⊢ ( ∃* 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) → ∃* 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) )
5	2 4	ax-mp	⊢ ∃* 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) )
6	1 5	mpgbir	⊢ Fun { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) }
7		dfadj2	⊢ adjℎ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) }
8	7	funeqi	⊢ ( Fun adjℎ ↔ Fun { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) } )
9	6 8	mpbir	⊢ Fun adjℎ