Theorem sectrcl

Description: Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	sectrcl.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
	sectrcl.f	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
Assertion	sectrcl	⊢ ( 𝜑 → 𝐶 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		sectrcl.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
2		sectrcl.f	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
3		df-br	⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑆 𝑌 ) )
4		df-ov	⊢ ( 𝑋 𝑆 𝑌 ) = ( 𝑆 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
5	4	eleq2i	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑆 𝑌 ) ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
6	3 5	bitri	⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
7		elfvne0	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) → 𝑆 ≠ ∅ )
8	6 7	sylbi	⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 → 𝑆 ≠ ∅ )
9	1	neeq1i	⊢ ( 𝑆 ≠ ∅ ↔ ( Sect ‘ 𝐶 ) ≠ ∅ )
10		n0	⊢ ( ( Sect ‘ 𝐶 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( Sect ‘ 𝐶 ) )
11	9 10	bitri	⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( Sect ‘ 𝐶 ) )
12	8 11	sylib	⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 → ∃ 𝑥 𝑥 ∈ ( Sect ‘ 𝐶 ) )
13		df-sect	⊢ Sect = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } ) )
14	13	mptrcl	⊢ ( 𝑥 ∈ ( Sect ‘ 𝐶 ) → 𝐶 ∈ Cat )
15	14	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ ( Sect ‘ 𝐶 ) → 𝐶 ∈ Cat )
16	2 12 15	3syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )