Theorem fuco2eld3

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

	Ref	Expression
Hypotheses	fuco2eld.w	|- ( ph -> W = ( S X. R ) )
	fuco2eld2.u	|- ( ph -> U e. W )
	fuco2eld2.s	|- Rel S
	fuco2eld2.r	|- Rel R
Assertion	fuco2eld3	|- ( ph -> ( ( 1st ` ( 1st ` U ) ) S ( 2nd ` ( 1st ` U ) ) /\ ( 1st ` ( 2nd ` U ) ) R ( 2nd ` ( 2nd ` U ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco2eld.w	|- ( ph -> W = ( S X. R ) )
2		fuco2eld2.u	|- ( ph -> U e. W )
3		fuco2eld2.s	|- Rel S
4		fuco2eld2.r	|- Rel R
5	1 2 3 4	fuco2eld2	|- ( ph -> U = <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. )
6	2 5 1	3eltr3d	|- ( ph -> <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. e. ( S X. R ) )
7		fuco2el	|- ( <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. e. ( S X. R ) <-> ( ( 1st ` ( 1st ` U ) ) S ( 2nd ` ( 1st ` U ) ) /\ ( 1st ` ( 2nd ` U ) ) R ( 2nd ` ( 2nd ` U ) ) ) )
8	6 7	sylib	|- ( ph -> ( ( 1st ` ( 1st ` U ) ) S ( 2nd ` ( 1st ` U ) ) /\ ( 1st ` ( 2nd ` U ) ) R ( 2nd ` ( 2nd ` U ) ) ) )