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

Metamath Proof Explorer

Theorem sectcan

Description: If G is a section of F and F is a section of H , then G = H . Proposition 3.10 of Adamek p. 28. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses sectcan.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
sectcan.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
sectcan.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
sectcan.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
sectcan.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
sectcan.1 ⊢ ( 𝜑 → 𝐺 ( 𝑋 𝑆 𝑌 ) 𝐹 )
sectcan.2 ⊢ ( 𝜑 → 𝐹 ( 𝑌 𝑆 𝑋 ) 𝐻 )
Assertion sectcan ( 𝜑 → 𝐺 = 𝐻 )

Proof

Step Hyp Ref Expression
1 sectcan.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 sectcan.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
3 sectcan.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 sectcan.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 sectcan.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 sectcan.1 ⊢ ( 𝜑 → 𝐺 ( 𝑋 𝑆 𝑌 ) 𝐹 )
7 sectcan.2 ⊢ ( 𝜑 → 𝐹 ( 𝑌 𝑆 𝑋 ) 𝐻 )
8 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
10 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
11 1 8 9 10 2 3 4 5 issect ⊢ ( 𝜑 → ( 𝐺 ( 𝑋 𝑆 𝑌 ) 𝐹 ↔ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
12 6 11 mpbid ⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
13 12 simp1d ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
14 1 8 9 10 2 3 5 4 issect ⊢ ( 𝜑 → ( 𝐹 ( 𝑌 𝑆 𝑋 ) 𝐻 ↔ ( 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( 𝐻 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) )
15 7 14 mpbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( 𝐻 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
16 15 simp1d ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
17 15 simp2d ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
18 1 8 9 3 4 5 4 13 16 5 17 catass ⊢ ( 𝜑 → ( ( 𝐻 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) = ( 𝐻 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) ) )
19 15 simp3d ⊢ ( 𝜑 → ( 𝐻 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
20 19 oveq1d ⊢ ( 𝜑 → ( ( 𝐻 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) )
21 12 simp3d ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
22 21 oveq2d ⊢ ( 𝜑 → ( 𝐻 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) ) = ( 𝐻 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
23 18 20 22 3eqtr3d ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) = ( 𝐻 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
24 1 8 10 3 4 9 5 13 catlid ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) = 𝐺 )
25 1 8 10 3 4 9 5 17 catrid ⊢ ( 𝜑 → ( 𝐻 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = 𝐻 )
26 23 24 25 3eqtr3d ⊢ ( 𝜑 → 𝐺 = 𝐻 )