Theorem sectrcl2

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

	Ref	Expression
Hypotheses	sectrcl.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
	sectrcl.f	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
	sectrcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	sectrcl2	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sectrcl.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
2		sectrcl.f	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
3		sectrcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		df-br	⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑆 𝑌 ) )
5	2 4	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑆 𝑌 ) )
6		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
8		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
9	1 2	sectrcl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
10	3 6 7 8 1 9	sectffval	⊢ ( 𝜑 → 𝑆 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) )
11	10	oveqd	⊢ ( 𝜑 → ( 𝑋 𝑆 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) 𝑌 ) )
12	5 11	eleqtrd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) 𝑌 ) )
13		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } )
14	13	elmpocl	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
15	12 14	syl	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )