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

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 ⊢ 𝐵 = ( Base ‘ 𝐶 )
isofval2.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
isofval2.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
isofval2.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
Assertion isofval2 ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ dom ( 𝑥 𝑁 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 isofval2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isofval2.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
3 isofval2.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 isofval2.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
5 isofn ⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
6 4 fneq1i ⊢ ( 𝐼 Fn ( 𝐵 × 𝐵 ) ↔ ( Iso ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) )
7 1 1 xpeq12i ⊢ ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
8 7 fneq2i ⊢ ( ( Iso ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) ↔ ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
9 6 8 bitri ⊢ ( 𝐼 Fn ( 𝐵 × 𝐵 ) ↔ ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
10 5 9 sylibr ⊢ ( 𝐶 ∈ Cat → 𝐼 Fn ( 𝐵 × 𝐵 ) )
11 fnov ⊢ ( 𝐼 Fn ( 𝐵 × 𝐵 ) ↔ 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐼 𝑦 ) ) )
12 10 11 sylib ⊢ ( 𝐶 ∈ Cat → 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐼 𝑦 ) ) )
13 3 12 syl ⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐼 𝑦 ) ) )
14 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Cat )
15 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
16 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
17 1 2 14 15 16 4 isoval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 𝐼 𝑦 ) = dom ( 𝑥 𝑁 𝑦 ) )
18 17 mpoeq3dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐼 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ dom ( 𝑥 𝑁 𝑦 ) ) )
19 13 18 eqtrd ⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ dom ( 𝑥 𝑁 𝑦 ) ) )