Metamath Proof Explorer

Theorem thincsect

Description: In a thin category, one morphism is a section of another iff they are pointing towards each other. (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses thincsect.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
thincsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thincsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thincsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thincsect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
thincsect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion thincsect ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 thincsect.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2 thincsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 thincsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 thincsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 thincsect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
6 thincsect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
7 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
8 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
9 1 thinccd ⊢ ( 𝜑 → 𝐶 ∈ Cat )
10 2 6 7 8 5 9 3 4 issect ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
11 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
12 10 11 bitrdi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
13 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) → 𝐶 ∈ ThinCat )
14 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
15 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) → 𝐶 ∈ Cat )
16 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) → 𝑌 ∈ 𝐵 )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
18 simprr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) → 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) )
19 2 6 7 15 14 16 14 17 18 catcocl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑋 ) )
20 13 2 6 14 8 19 thincid ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
21 12 20 mpbiran3d ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ) )