Metamath Proof Explorer

Theorem catcsect

Description: The property " F is a section of G " in a category of small categories (in a universe). (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses catcsect.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
catcsect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
catcsect.i ⊢ 𝐼 = ( idfunc ‘ 𝑋 )
catcsect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
Assertion catcsect ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ∘func 𝐹 ) = 𝐼 ) )

Proof

Step Hyp Ref Expression
1 catcsect.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 catcsect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 catcsect.i ⊢ 𝐼 = ( idfunc ‘ 𝑋 )
4 catcsect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
5 id ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
6 4 5 sectrcl ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 → 𝐶 ∈ Cat )
7 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8 4 5 7 sectrcl2 ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
9 6 8 jca ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 → ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) )
10 simpl ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
11 1 2 10 catcrcl ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝑈 ∈ V )
12 1 catccat ⊢ ( 𝑈 ∈ V → 𝐶 ∈ Cat )
13 11 12 syl ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝐶 ∈ Cat )
14 1 2 10 7 catcrcl2 ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
15 13 14 jca ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) )
16 15 3adant3 ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) )
17 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
18 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
19 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
20 simprl ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
21 simprr ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
22 7 2 17 18 4 19 20 21 issect ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
23 9 16 22 pm5.21nii ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
24 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
25 15 20 syl ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
26 15 21 syl ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
27 1 2 10 elcatchom ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝐹 ∈ ( 𝑋 Func 𝑌 ) )
28 simpr ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) )
29 1 2 28 elcatchom ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝐺 ∈ ( 𝑌 Func 𝑋 ) )
30 1 7 11 17 25 26 25 27 29 catcco ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )
31 1 7 18 3 11 25 catcid ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = 𝐼 )
32 30 31 eqeq12d ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ↔ ( 𝐺 ∘func 𝐹 ) = 𝐼 ) )
33 32 pm5.32i ⊢ ( ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ∘func 𝐹 ) = 𝐼 ) )
34 23 24 33 3bitri ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ∘func 𝐹 ) = 𝐼 ) )