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 ffvelrnd ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
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 ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 )