Theorem fuco2eld

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

	Ref	Expression
Hypotheses	fuco2eld.w	$$⊢\phi \to W=S\times R$$
	fuco2eld.u	$$⊢\phi \to U=⟨⟨K,L⟩,⟨F,G⟩⟩$$
	fuco2eld.k	$$⊢\phi \to KSL$$
	fuco2eld.f	$$⊢\phi \to FRG$$
Assertion	fuco2eld	$$⊢\phi \to U\in W$$

Proof

Step	Hyp	Ref	Expression
1		fuco2eld.w	$$⊢\phi \to W=S\times R$$
2		fuco2eld.u	$$⊢\phi \to U=⟨⟨K,L⟩,⟨F,G⟩⟩$$
3		fuco2eld.k	$$⊢\phi \to KSL$$
4		fuco2eld.f	$$⊢\phi \to FRG$$
5		fuco2el	$$⊢⟨⟨K,L⟩,⟨F,G⟩⟩\in \left(S\times R\right)\leftrightarrow \left(KSL\wedge FRG\right)$$
6	3 4 5	sylanbrc	$$⊢\phi \to ⟨⟨K,L⟩,⟨F,G⟩⟩\in \left(S\times R\right)$$
7	6 2 1	3eltr4d	$$⊢\phi \to U\in W$$