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 ⊢ C ∈ Cat → Iso ⁡ C Fn Base C × Base C

Proof

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