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

Metamath Proof Explorer

Theorem sectid

Description: The identity is a section of itself. (Contributed by AV, 8-Apr-2020)

Ref Expression
Hypotheses invid.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
invid.i ⊢ 𝐼 = ( Id ‘ 𝐶 )
invid.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
invid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion sectid ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ( 𝑋 ( Sect ‘ 𝐶 ) 𝑋 ) ( 𝐼 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 invid.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 invid.i ⊢ 𝐼 = ( Id ‘ 𝐶 )
3 invid.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 invid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
7 1 5 2 3 4 catidcl ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
8 1 5 2 3 4 6 4 7 catlid ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) )
9 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
10 1 5 6 2 9 3 4 4 7 7 issect2 ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑋 ) ( 𝑋 ( Sect ‘ 𝐶 ) 𝑋 ) ( 𝐼 ‘ 𝑋 ) ↔ ( ( 𝐼 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) ) )
11 8 10 mpbird ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ( 𝑋 ( Sect ‘ 𝐶 ) 𝑋 ) ( 𝐼 ‘ 𝑋 ) )