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	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	sectpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
Assertion	sectpropd	$$⊢\phi \to \mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		sectpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
2		sectpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
3	1 2	sectpropdlem	$$⊢\left(\phi \wedge f\in \mathrm{Sect}\left(C\right)\right)\to f\in \mathrm{Sect}\left(D\right)$$
4	1	eqcomd	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
5	2	eqcomd	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(C\right)$$
6	4 5	sectpropdlem	$$⊢\left(\phi \wedge f\in \mathrm{Sect}\left(D\right)\right)\to f\in \mathrm{Sect}\left(C\right)$$
7	3 6	impbida	$$⊢\phi \to \left(f\in \mathrm{Sect}\left(C\right)\leftrightarrow f\in \mathrm{Sect}\left(D\right)\right)$$
8	7	eqrdv	$$⊢\phi \to \mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(D\right)$$