Theorem cic1st2ndbr

Description: Rewrite the predicate of isomorphic objects with separated parts. (Contributed by Zhi Wang, 27-Oct-2025)

	Ref	Expression
Assertion	cic1st2ndbr	$$⊢P\in {\simeq }_{𝑐}\left(C\right)\to 1^{st}\left(P\right){\simeq }_{𝑐}\left(C\right)2^{nd}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		cic1st2nd	$$⊢P\in {\simeq }_{𝑐}\left(C\right)\to P=⟨1^{st}\left(P\right),2^{nd}\left(P\right)⟩$$
2		id	$$⊢P\in {\simeq }_{𝑐}\left(C\right)\to P\in {\simeq }_{𝑐}\left(C\right)$$
3	1 2	eqeltrrd	$$⊢P\in {\simeq }_{𝑐}\left(C\right)\to ⟨1^{st}\left(P\right),2^{nd}\left(P\right)⟩\in {\simeq }_{𝑐}\left(C\right)$$
4		df-br	$$⊢1^{st}\left(P\right){\simeq }_{𝑐}\left(C\right)2^{nd}\left(P\right)\leftrightarrow ⟨1^{st}\left(P\right),2^{nd}\left(P\right)⟩\in {\simeq }_{𝑐}\left(C\right)$$
5	3 4	sylibr	$$⊢P\in {\simeq }_{𝑐}\left(C\right)\to 1^{st}\left(P\right){\simeq }_{𝑐}\left(C\right)2^{nd}\left(P\right)$$