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