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

Metamath Proof Explorer

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 ‘ 𝐶 ) ) )