Theorem fuco2eld

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

	Ref	Expression
Hypotheses	fuco2eld.w	|- ( ph -> W = ( S X. R ) )
	fuco2eld.u	|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
	fuco2eld.k	|- ( ph -> K S L )
	fuco2eld.f	|- ( ph -> F R G )
Assertion	fuco2eld	|- ( ph -> U e. W )

Proof

Step	Hyp	Ref	Expression
1		fuco2eld.w	|- ( ph -> W = ( S X. R ) )
2		fuco2eld.u	|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
3		fuco2eld.k	|- ( ph -> K S L )
4		fuco2eld.f	|- ( ph -> F R G )
5		fuco2el	|- ( <. <. K , L >. , <. F , G >. >. e. ( S X. R ) <-> ( K S L /\ F R G ) )
6	3 4 5	sylanbrc	|- ( ph -> <. <. K , L >. , <. F , G >. >. e. ( S X. R ) )
7	6 2 1	3eltr4d	|- ( ph -> U e. W )