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	⊢ ( 𝜑 → 𝐺 = 𝐻 )

Metamath Proof Explorer

Theorem sectcan

Proof