Theorem isofval

Description: Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017)

	Ref	Expression
Assertion	isofval	⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) = ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-iso	⊢ Iso = ( 𝑐 ∈ Cat ↦ ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝑐 ) ) )
2		fveq2	⊢ ( 𝑐 = 𝐶 → ( Inv ‘ 𝑐 ) = ( Inv ‘ 𝐶 ) )
3	2	coeq2d	⊢ ( 𝑐 = 𝐶 → ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝑐 ) ) = ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) )
4		id	⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
5		funmpt	⊢ Fun ( 𝑥 ∈ V ↦ dom 𝑥 )
6		fvexd	⊢ ( 𝐶 ∈ Cat → ( Inv ‘ 𝐶 ) ∈ V )
7		cofunexg	⊢ ( ( Fun ( 𝑥 ∈ V ↦ dom 𝑥 ) ∧ ( Inv ‘ 𝐶 ) ∈ V ) → ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) ∈ V )
8	5 6 7	sylancr	⊢ ( 𝐶 ∈ Cat → ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) ∈ V )
9	1 3 4 8	fvmptd3	⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) = ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) )