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

Metamath Proof Explorer

Theorem invisoinvl

Description: The inverse of an isomorphism F (which is unique because of invf and is therefore denoted by ( ( X N Y )F ) , see also remark 3.12 in Adamek p. 28) is invers to the isomorphism. (Contributed by AV, 9-Apr-2020)

Ref Expression
Hypotheses invisoinv.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
invisoinv.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
invisoinv.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
invisoinv.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
invisoinv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
invisoinv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
invisoinv.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
Assertion invisoinvl ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 )

Proof

Step Hyp Ref Expression
1 invisoinv.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 invisoinv.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
3 invisoinv.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
4 invisoinv.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 invisoinv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 invisoinv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 invisoinv.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
8 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
9 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
10 1 9 4 6 idiso ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ∈ ( 𝑌 ( Iso ‘ 𝐶 ) 𝑌 ) )
11 2 a1i ⊢ ( 𝜑 → 𝐼 = ( Iso ‘ 𝐶 ) )
12 11 oveqd ⊢ ( 𝜑 → ( 𝑌 𝐼 𝑌 ) = ( 𝑌 ( Iso ‘ 𝐶 ) 𝑌 ) )
13 10 12 eleqtrrd ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ∈ ( 𝑌 𝐼 𝑌 ) )
14 1 3 4 5 6 2 7 8 6 13 invco ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ( 𝑋 𝑁 𝑌 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) )
15 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
16 1 15 2 4 5 6 isohom ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
17 16 7 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
18 1 15 9 4 5 8 6 17 catlid ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = 𝐹 )
19 3 a1i ⊢ ( 𝜑 → 𝑁 = ( Inv ‘ 𝐶 ) )
20 19 oveqd ⊢ ( 𝜑 → ( 𝑌 𝑁 𝑌 ) = ( 𝑌 ( Inv ‘ 𝐶 ) 𝑌 ) )
21 20 fveq1d ⊢ ( 𝜑 → ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( 𝑌 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
22 1 9 4 6 idinv ⊢ ( 𝜑 → ( ( 𝑌 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
23 21 22 eqtrd ⊢ ( 𝜑 → ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
24 23 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) = ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
25 1 15 2 4 6 5 isohom ⊢ ( 𝜑 → ( 𝑌 𝐼 𝑋 ) ⊆ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
26 1 3 4 5 6 2 invf ⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) : ( 𝑋 𝐼 𝑌 ) ⟶ ( 𝑌 𝐼 𝑋 ) )
27 26 7 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
28 25 27 sseldd ⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
29 1 15 9 4 6 8 5 28 catrid ⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
30 24 29 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) = ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
31 14 18 30 3brtr3d ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
32 1 3 4 6 5 invsym ⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 ↔ 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) )
33 31 32 mpbird ⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 )