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

Metamath Proof Explorer

Theorem isofnALT

Description: The function value of the function returning the isomorphisms of a category is a function over the Cartesian square of the base set of the category. (Contributed by AV, 5-Apr-2020) (Proof shortened by Zhi Wang, 3-Nov-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion isofnALT ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 dmexg ⊢ ( 𝑥 ∈ V → dom 𝑥 ∈ V )
2 1 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ V ) → dom 𝑥 ∈ V )
3 2 ralrimiva ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ V dom 𝑥 ∈ V )
4 eqid ⊢ ( 𝑥 ∈ V ↦ dom 𝑥 ) = ( 𝑥 ∈ V ↦ dom 𝑥 )
5 4 fnmpt ⊢ ( ∀ 𝑥 ∈ V dom 𝑥 ∈ V → ( 𝑥 ∈ V ↦ dom 𝑥 ) Fn V )
6 3 5 syl ⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ V ↦ dom 𝑥 ) Fn V )
7 invfn ⊢ ( 𝐶 ∈ Cat → ( Inv ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
8 ssv ⊢ ran ( Inv ‘ 𝐶 ) ⊆ V
9 8 a1i ⊢ ( 𝐶 ∈ Cat → ran ( Inv ‘ 𝐶 ) ⊆ V )
10 fnco ⊢ ( ( ( 𝑥 ∈ V ↦ dom 𝑥 ) Fn V ∧ ( Inv ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ran ( Inv ‘ 𝐶 ) ⊆ V ) → ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
11 6 7 9 10 syl3anc ⊢ ( 𝐶 ∈ Cat → ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
12 isofval ⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) = ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) )
13 12 fneq1d ⊢ ( 𝐶 ∈ Cat → ( ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
14 11 13 mpbird ⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )