Theorem sectpropd

Description: Two structures with the same base, hom-sets and composition operation have the same sections. (Contributed by Zhi Wang, 27-Oct-2025)

	Ref	Expression
Hypotheses	sectpropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
	sectpropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
Assertion	sectpropd	⊢ ( 𝜑 → ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		sectpropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2		sectpropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3	1 2	sectpropdlem	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Sect ‘ 𝐶 ) ) → 𝑓 ∈ ( Sect ‘ 𝐷 ) )
4	1	eqcomd	⊢ ( 𝜑 → ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐶 ) )
5	2	eqcomd	⊢ ( 𝜑 → ( compf ‘ 𝐷 ) = ( compf ‘ 𝐶 ) )
6	4 5	sectpropdlem	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Sect ‘ 𝐷 ) ) → 𝑓 ∈ ( Sect ‘ 𝐶 ) )
7	3 6	impbida	⊢ ( 𝜑 → ( 𝑓 ∈ ( Sect ‘ 𝐶 ) ↔ 𝑓 ∈ ( Sect ‘ 𝐷 ) ) )
8	7	eqrdv	⊢ ( 𝜑 → ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐷 ) )