Metamath Proof Explorer

Theorem isofval2

Description: Function value of the function returning the isomorphisms of a category. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Hypotheses isofval2.b ⊢ B = Base C
isofval2.n ⊢ N = Inv ⁡ C
isofval2.c ⊢ φ → C ∈ Cat
isofval2.i ⊢ I = Iso ⁡ C
Assertion isofval2 ⊢ φ → I = x ∈ B , y ∈ B ⟼ dom ⁡ x N y

Proof

Step Hyp Ref Expression
1 isofval2.b ⊢ B = Base C
2 isofval2.n ⊢ N = Inv ⁡ C
3 isofval2.c ⊢ φ → C ∈ Cat
4 isofval2.i ⊢ I = Iso ⁡ C
5 isofn ⊢ C ∈ Cat → Iso ⁡ C Fn Base C × Base C
6 4 fneq1i ⊢ I Fn B × B ↔ Iso ⁡ C Fn B × B
7 1 1 xpeq12i ⊢ B × B = Base C × Base C
8 7 fneq2i ⊢ Iso ⁡ C Fn B × B ↔ Iso ⁡ C Fn Base C × Base C
9 6 8 bitri ⊢ I Fn B × B ↔ Iso ⁡ C Fn Base C × Base C
10 5 9 sylibr ⊢ C ∈ Cat → I Fn B × B
11 fnov ⊢ I Fn B × B ↔ I = x ∈ B , y ∈ B ⟼ x I y
12 10 11 sylib ⊢ C ∈ Cat → I = x ∈ B , y ∈ B ⟼ x I y
13 3 12 syl ⊢ φ → I = x ∈ B , y ∈ B ⟼ x I y
14 3 3ad2ant1 ⊢ φ ∧ x ∈ B ∧ y ∈ B → C ∈ Cat
15 simp2 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ∈ B
16 simp3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → y ∈ B
17 1 2 14 15 16 4 isoval ⊢ φ ∧ x ∈ B ∧ y ∈ B → x I y = dom ⁡ x N y
18 17 mpoeq3dva ⊢ φ → x ∈ B , y ∈ B ⟼ x I y = x ∈ B , y ∈ B ⟼ dom ⁡ x N y
19 13 18 eqtrd ⊢ φ → I = x ∈ B , y ∈ B ⟼ dom ⁡ x N y