Theorem fuco2eld3

Description: Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025)

	Ref	Expression
Hypotheses	fuco2eld.w	$$⊢\phi \to W=S\times R$$
	fuco2eld2.u	$$⊢\phi \to U\in W$$
	fuco2eld2.s	$$⊢\mathrm{Rel}S$$
	fuco2eld2.r	$$⊢\mathrm{Rel}R$$
Assertion	fuco2eld3	$$⊢\phi \to \left(1^{st}\left(1^{st}\left(U\right)\right)S{2}^{nd}\left(1^{st}\left(U\right)\right)\wedge 1^{st}\left(2^{nd}\left(U\right)\right)R{2}^{nd}\left(2^{nd}\left(U\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fuco2eld.w	$$⊢\phi \to W=S\times R$$
2		fuco2eld2.u	$$⊢\phi \to U\in W$$
3		fuco2eld2.s	$$⊢\mathrm{Rel}S$$
4		fuco2eld2.r	$$⊢\mathrm{Rel}R$$
5	1 2 3 4	fuco2eld2	$$⊢\phi \to U=⟨⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩,⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩⟩$$
6	2 5 1	3eltr3d	$$⊢\phi \to ⟨⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩,⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩⟩\in \left(S\times R\right)$$
7		fuco2el	$$⊢⟨⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩,⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩⟩\in \left(S\times R\right)\leftrightarrow \left(1^{st}\left(1^{st}\left(U\right)\right)S{2}^{nd}\left(1^{st}\left(U\right)\right)\wedge 1^{st}\left(2^{nd}\left(U\right)\right)R{2}^{nd}\left(2^{nd}\left(U\right)\right)\right)$$
8	6 7	sylib	$$⊢\phi \to \left(1^{st}\left(1^{st}\left(U\right)\right)S{2}^{nd}\left(1^{st}\left(U\right)\right)\wedge 1^{st}\left(2^{nd}\left(U\right)\right)R{2}^{nd}\left(2^{nd}\left(U\right)\right)\right)$$