Metamath Proof Explorer

Theorem fuco2eld2

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 fuco2eld2 
|- ( ph -> U = <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 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 2 1 eleqtrd 
 |-  ( ph -> U e. ( S X. R ) )
6 1st2nd2 
 |-  ( U e. ( S X. R ) -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
7 5 6 syl 
 |-  ( ph -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
8 df-rel 
 |-  ( Rel S <-> S C_ ( _V X. _V ) )
9 3 8 mpbi 
 |-  S C_ ( _V X. _V )
10 xp1st 
 |-  ( U e. ( S X. R ) -> ( 1st ` U ) e. S )
11 9 10 sselid 
 |-  ( U e. ( S X. R ) -> ( 1st ` U ) e. ( _V X. _V ) )
12 1st2nd2 
 |-  ( ( 1st ` U ) e. ( _V X. _V ) -> ( 1st ` U ) = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. )
13 5 11 12 3syl 
 |-  ( ph -> ( 1st ` U ) = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. )
14 df-rel 
 |-  ( Rel R <-> R C_ ( _V X. _V ) )
15 4 14 mpbi 
 |-  R C_ ( _V X. _V )
16 xp2nd 
 |-  ( U e. ( S X. R ) -> ( 2nd ` U ) e. R )
17 15 16 sselid 
 |-  ( U e. ( S X. R ) -> ( 2nd ` U ) e. ( _V X. _V ) )
18 1st2nd2 
 |-  ( ( 2nd ` U ) e. ( _V X. _V ) -> ( 2nd ` U ) = <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. )
19 5 17 18 3syl 
 |-  ( ph -> ( 2nd ` U ) = <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. )
20 13 19 opeq12d 
 |-  ( ph -> <. ( 1st ` U ) , ( 2nd ` U ) >. = <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. )
21 7 20 eqtrd 
 |-  ( ph -> U = <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. )