Metamath Proof Explorer

Theorem 2initoinv

Description: Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
initoeu1.b ⊢ ( 𝜑 → 𝐵 ∈ ( InitO ‘ 𝐶 ) )
Assertion 2initoinv ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐹 ( 𝐴 ( Inv ‘ 𝐶 ) 𝐵 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
3 initoeu1.b ⊢ ( 𝜑 → 𝐵 ∈ ( InitO ‘ 𝐶 ) )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
7 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐶 ∈ Cat )
8 initoo ⊢ ( 𝐶 ∈ Cat → ( 𝐴 ∈ ( InitO ‘ 𝐶 ) → 𝐴 ∈ ( Base ‘ 𝐶 ) ) )
9 1 2 8 sylc ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐶 ) )
10 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐴 ∈ ( Base ‘ 𝐶 ) )
11 initoo ⊢ ( 𝐶 ∈ Cat → ( 𝐵 ∈ ( InitO ‘ 𝐶 ) → 𝐵 ∈ ( Base ‘ 𝐶 ) ) )
12 1 3 11 sylc ⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ 𝐶 ) )
13 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐵 ∈ ( Base ‘ 𝐶 ) )
14 simp3 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) )
15 simp2 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
16 4 5 6 7 10 13 10 14 15 catcocl ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐴 ) 𝐹 ) ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐴 ) )
17 4 5 1 initoid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝐴 ( Hom ‘ 𝐶 ) 𝐴 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝐴 ) } )
18 2 17 mpdan ⊢ ( 𝜑 → ( 𝐴 ( Hom ‘ 𝐶 ) 𝐴 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝐴 ) } )
19 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( 𝐴 ( Hom ‘ 𝐶 ) 𝐴 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝐴 ) } )
20 19 eleq2d ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐴 ) 𝐹 ) ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐴 ) ↔ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐴 ) 𝐹 ) ∈ { ( ( Id ‘ 𝐶 ) ‘ 𝐴 ) } ) )
21 elsni ⊢ ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐴 ) 𝐹 ) ∈ { ( ( Id ‘ 𝐶 ) ‘ 𝐴 ) } → ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐴 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝐴 ) )
22 20 21 syl6bi ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐴 ) 𝐹 ) ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐴 ) → ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐴 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝐴 ) ) )
23 16 22 mpd ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐴 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝐴 ) )
24 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
25 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
26 4 5 6 24 25 7 10 13 14 15 issect2 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( 𝐹 ( 𝐴 ( Sect ‘ 𝐶 ) 𝐵 ) 𝐺 ↔ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐴 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝐴 ) ) )
27 23 26 mpbird ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐹 ( 𝐴 ( Sect ‘ 𝐶 ) 𝐵 ) 𝐺 )
28 4 5 6 7 13 10 13 15 14 catcocl ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝐵 ) 𝐺 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐵 ) )
29 4 5 1 initoid ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝐵 ( Hom ‘ 𝐶 ) 𝐵 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝐵 ) } )
30 3 29 mpdan ⊢ ( 𝜑 → ( 𝐵 ( Hom ‘ 𝐶 ) 𝐵 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝐵 ) } )
31 30 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( 𝐵 ( Hom ‘ 𝐶 ) 𝐵 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝐵 ) } )
32 31 eleq2d ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝐵 ) 𝐺 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐵 ) ↔ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝐵 ) 𝐺 ) ∈ { ( ( Id ‘ 𝐶 ) ‘ 𝐵 ) } ) )
33 elsni ⊢ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝐵 ) 𝐺 ) ∈ { ( ( Id ‘ 𝐶 ) ‘ 𝐵 ) } → ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝐵 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝐵 ) )
34 32 33 syl6bi ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝐵 ) 𝐺 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐵 ) → ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝐵 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝐵 ) ) )
35 28 34 mpd ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝐵 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝐵 ) )
36 4 5 6 24 25 7 13 10 15 14 issect2 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( 𝐺 ( 𝐵 ( Sect ‘ 𝐶 ) 𝐴 ) 𝐹 ↔ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ( comp ‘ 𝐶 ) 𝐵 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝐵 ) ) )
37 35 36 mpbird ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐺 ( 𝐵 ( Sect ‘ 𝐶 ) 𝐴 ) 𝐹 )
38 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
39 4 38 1 9 12 25 isinv ⊢ ( 𝜑 → ( 𝐹 ( 𝐴 ( Inv ‘ 𝐶 ) 𝐵 ) 𝐺 ↔ ( 𝐹 ( 𝐴 ( Sect ‘ 𝐶 ) 𝐵 ) 𝐺 ∧ 𝐺 ( 𝐵 ( Sect ‘ 𝐶 ) 𝐴 ) 𝐹 ) ) )
40 39 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → ( 𝐹 ( 𝐴 ( Inv ‘ 𝐶 ) 𝐵 ) 𝐺 ↔ ( 𝐹 ( 𝐴 ( Sect ‘ 𝐶 ) 𝐵 ) 𝐺 ∧ 𝐺 ( 𝐵 ( Sect ‘ 𝐶 ) 𝐴 ) 𝐹 ) ) )
41 27 37 40 mpbir2and ⊢ ( ( 𝜑 ∧ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐵 ) ) → 𝐹 ( 𝐴 ( Inv ‘ 𝐶 ) 𝐵 ) 𝐺 )