Metamath Proof Explorer

Theorem oppfdiag1

Description: A constant functor for opposite categories is the opposite functor of the constant functor for original categories. (Contributed by Zhi Wang, 19-Nov-2025)

Ref Expression
Hypotheses oppfdiag.o 
|- O = ( oppCat ` C )
oppfdiag.p 
|- P = ( oppCat ` D )
oppfdiag.l 
|- L = ( C DiagFunc D )
oppfdiag.c 
|- ( ph -> C e. Cat )
oppfdiag.d 
|- ( ph -> D e. Cat )
oppfdiag1.f 
|- ( ph -> F = ( oppFunc |` ( D Func C ) ) )
oppfdiag1.a 
|- A = ( Base ` C )
oppfdiag1.x 
|- ( ph -> X e. A )
Assertion oppfdiag1 
|- ( ph -> ( F ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) )

Proof

Step Hyp Ref Expression
1 oppfdiag.o 
 |-  O = ( oppCat ` C )
2 oppfdiag.p 
 |-  P = ( oppCat ` D )
3 oppfdiag.l 
 |-  L = ( C DiagFunc D )
4 oppfdiag.c 
 |-  ( ph -> C e. Cat )
5 oppfdiag.d 
 |-  ( ph -> D e. Cat )
6 oppfdiag1.f 
 |-  ( ph -> F = ( oppFunc |` ( D Func C ) ) )
7 oppfdiag1.a 
 |-  A = ( Base ` C )
8 oppfdiag1.x 
 |-  ( ph -> X e. A )
9 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
10 9 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
11 3 4 5 9 diagcl 
 |-  ( ph -> L e. ( C Func ( D FuncCat C ) ) )
12 11 func1st2nd 
 |-  ( ph -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
13 7 10 12 funcf1 
 |-  ( ph -> ( 1st ` L ) : A --> ( D Func C ) )
14 13 8 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` L ) ` X ) e. ( D Func C ) )
15 6 14 opf11 
 |-  ( ph -> ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) = ( 1st ` ( ( 1st ` L ) ` X ) ) )
16 eqid 
 |-  ( Base ` D ) = ( Base ` D )
17 2 16 oppcbas 
 |-  ( Base ` D ) = ( Base ` P )
18 1 7 oppcbas 
 |-  A = ( Base ` O )
19 eqid 
 |-  ( oppCat ` ( D FuncCat C ) ) = ( oppCat ` ( D FuncCat C ) )
20 1 19 11 oppfoppc2 
 |-  ( ph -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) )
21 eqid 
 |-  ( P FuncCat O ) = ( P FuncCat O )
22 eqid 
 |-  ( D Nat C ) = ( D Nat C )
23 eqidd 
 |-  ( ph -> ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) = ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) )
24 2 1 9 19 21 22 6 23 5 4 fucoppcfunc 
 |-  ( ph -> F ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) )
25 df-br 
 |-  ( F ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) <-> <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. e. ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) )
26 24 25 sylib 
 |-  ( ph -> <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. e. ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) )
27 18 20 26 8 cofu1 
 |-  ( ph -> ( ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ` X ) = ( ( 1st ` <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` X ) ) )
28 24 func1st 
 |-  ( ph -> ( 1st ` <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. ) = F )
29 11 oppf1 
 |-  ( ph -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) )
30 29 fveq1d 
 |-  ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` X ) = ( ( 1st ` L ) ` X ) )
31 28 30 fveq12d 
 |-  ( ph -> ( ( 1st ` <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` X ) ) = ( F ` ( ( 1st ` L ) ` X ) ) )
32 27 31 eqtrd 
 |-  ( ph -> ( ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ` X ) = ( F ` ( ( 1st ` L ) ` X ) ) )
33 21 fucbas 
 |-  ( P Func O ) = ( Base ` ( P FuncCat O ) )
34 20 26 cofucl 
 |-  ( ph -> ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) )
35 34 func1st2nd 
 |-  ( ph -> ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) )
36 18 33 35 funcf1 
 |-  ( ph -> ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) : A --> ( P Func O ) )
37 36 8 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` ( <. F , ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n ( D Nat C ) m ) ) ) >. o.func ( oppFunc ` L ) ) ) ` X ) e. ( P Func O ) )
38 32 37 eqeltrrd 
 |-  ( ph -> ( F ` ( ( 1st ` L ) ` X ) ) e. ( P Func O ) )
39 38 func1st2nd 
 |-  ( ph -> ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) ( P Func O ) ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) )
40 17 18 39 funcf1 
 |-  ( ph -> ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) : ( Base ` D ) --> A )
41 15 40 feq1dd 
 |-  ( ph -> ( 1st ` ( ( 1st ` L ) ` X ) ) : ( Base ` D ) --> A )
42 41 ffnd 
 |-  ( ph -> ( 1st ` ( ( 1st ` L ) ` X ) ) Fn ( Base ` D ) )
43 eqid 
 |-  ( O DiagFunc P ) = ( O DiagFunc P )
44 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
45 4 44 syl 
 |-  ( ph -> O e. Cat )
46 2 oppccat 
 |-  ( D e. Cat -> P e. Cat )
47 5 46 syl 
 |-  ( ph -> P e. Cat )
48 43 45 47 21 diagcl 
 |-  ( ph -> ( O DiagFunc P ) e. ( O Func ( P FuncCat O ) ) )
49 48 func1st2nd 
 |-  ( ph -> ( 1st ` ( O DiagFunc P ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( O DiagFunc P ) ) )
50 18 33 49 funcf1 
 |-  ( ph -> ( 1st ` ( O DiagFunc P ) ) : A --> ( P Func O ) )
51 50 8 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` ( O DiagFunc P ) ) ` X ) e. ( P Func O ) )
52 51 func1st2nd 
 |-  ( ph -> ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) ( P Func O ) ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) )
53 17 18 52 funcf1 
 |-  ( ph -> ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) : ( Base ` D ) --> A )
54 53 ffnd 
 |-  ( ph -> ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) Fn ( Base ` D ) )
55 4 adantr 
 |-  ( ( ph /\ y e. ( Base ` D ) ) -> C e. Cat )
56 5 adantr 
 |-  ( ( ph /\ y e. ( Base ` D ) ) -> D e. Cat )
57 8 adantr 
 |-  ( ( ph /\ y e. ( Base ` D ) ) -> X e. A )
58 eqid 
 |-  ( ( 1st ` L ) ` X ) = ( ( 1st ` L ) ` X )
59 simpr 
 |-  ( ( ph /\ y e. ( Base ` D ) ) -> y e. ( Base ` D ) )
60 3 55 56 7 57 58 16 59 diag11 
 |-  ( ( ph /\ y e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` y ) = X )
61 45 adantr 
 |-  ( ( ph /\ y e. ( Base ` D ) ) -> O e. Cat )
62 47 adantr 
 |-  ( ( ph /\ y e. ( Base ` D ) ) -> P e. Cat )
63 eqid 
 |-  ( ( 1st ` ( O DiagFunc P ) ) ` X ) = ( ( 1st ` ( O DiagFunc P ) ) ` X )
64 43 61 62 18 57 63 17 59 diag11 
 |-  ( ( ph /\ y e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) ` y ) = X )
65 60 64 eqtr4d 
 |-  ( ( ph /\ y e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` y ) = ( ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) ` y ) )
66 42 54 65 eqfnfvd 
 |-  ( ph -> ( 1st ` ( ( 1st ` L ) ` X ) ) = ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) )
67 15 66 eqtrd 
 |-  ( ph -> ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) = ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) )
68 17 39 funcfn2 
 |-  ( ph -> ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
69 17 52 funcfn2 
 |-  ( ph -> ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
70 6 14 opf12 
 |-  ( ph -> ( y ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) z ) = ( z ( 2nd ` ( ( 1st ` L ) ` X ) ) y ) )
71 70 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) z ) = ( z ( 2nd ` ( ( 1st ` L ) ` X ) ) y ) )
72 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
73 72 2 oppchom 
 |-  ( y ( Hom ` P ) z ) = ( z ( Hom ` D ) y )
74 73 a1i 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( Hom ` P ) z ) = ( z ( Hom ` D ) y ) )
75 eqid 
 |-  ( Hom ` P ) = ( Hom ` P )
76 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
77 39 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) ( P Func O ) ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) )
78 simprl 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
79 simprr 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> z e. ( Base ` D ) )
80 17 75 76 77 78 79 funcf2 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) z ) : ( y ( Hom ` P ) z ) --> ( ( ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) ` y ) ( Hom ` O ) ( ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) ` z ) ) )
81 74 80 feq2dd 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) z ) : ( z ( Hom ` D ) y ) --> ( ( ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) ` y ) ( Hom ` O ) ( ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) ` z ) ) )
82 71 81 feq1dd 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( z ( 2nd ` ( ( 1st ` L ) ` X ) ) y ) : ( z ( Hom ` D ) y ) --> ( ( ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) ` y ) ( Hom ` O ) ( ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) ` z ) ) )
83 82 ffnd 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( z ( 2nd ` ( ( 1st ` L ) ` X ) ) y ) Fn ( z ( Hom ` D ) y ) )
84 52 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) ( P Func O ) ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) )
85 17 75 76 84 78 79 funcf2 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) z ) : ( y ( Hom ` P ) z ) --> ( ( ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) ` y ) ( Hom ` O ) ( ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) ` z ) ) )
86 74 85 feq2dd 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) z ) : ( z ( Hom ` D ) y ) --> ( ( ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) ` y ) ( Hom ` O ) ( ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) ` z ) ) )
87 86 ffnd 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) z ) Fn ( z ( Hom ` D ) y ) )
88 eqid 
 |-  ( Id ` C ) = ( Id ` C )
89 1 88 oppcid 
 |-  ( C e. Cat -> ( Id ` O ) = ( Id ` C ) )
90 4 89 syl 
 |-  ( ph -> ( Id ` O ) = ( Id ` C ) )
91 90 fveq1d 
 |-  ( ph -> ( ( Id ` O ) ` X ) = ( ( Id ` C ) ` X ) )
92 91 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> ( ( Id ` O ) ` X ) = ( ( Id ` C ) ` X ) )
93 4 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> C e. Cat )
94 93 44 syl 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> O e. Cat )
95 5 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> D e. Cat )
96 95 46 syl 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> P e. Cat )
97 8 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> X e. A )
98 78 adantr 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> y e. ( Base ` D ) )
99 eqid 
 |-  ( Id ` O ) = ( Id ` O )
100 79 adantr 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> z e. ( Base ` D ) )
101 simpr 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> f e. ( z ( Hom ` D ) y ) )
102 101 73 eleqtrrdi 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> f e. ( y ( Hom ` P ) z ) )
103 43 94 96 18 97 63 17 98 75 99 100 102 diag12 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> ( ( y ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) z ) ` f ) = ( ( Id ` O ) ` X ) )
104 3 93 95 7 97 58 16 100 72 88 98 101 diag12 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> ( ( z ( 2nd ` ( ( 1st ` L ) ` X ) ) y ) ` f ) = ( ( Id ` C ) ` X ) )
105 92 103 104 3eqtr4rd 
 |-  ( ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ f e. ( z ( Hom ` D ) y ) ) -> ( ( z ( 2nd ` ( ( 1st ` L ) ` X ) ) y ) ` f ) = ( ( y ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) z ) ` f ) )
106 83 87 105 eqfnfvd 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( z ( 2nd ` ( ( 1st ` L ) ` X ) ) y ) = ( y ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) z ) )
107 71 106 eqtrd 
 |-  ( ( ph /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) z ) = ( y ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) z ) )
108 68 69 107 eqfnovd 
 |-  ( ph -> ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) = ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) )
109 67 108 opeq12d 
 |-  ( ph -> <. ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) , ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) >. = <. ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) , ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) >. )
110 relfunc 
 |-  Rel ( P Func O )
111 1st2nd 
 |-  ( ( Rel ( P Func O ) /\ ( F ` ( ( 1st ` L ) ` X ) ) e. ( P Func O ) ) -> ( F ` ( ( 1st ` L ) ` X ) ) = <. ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) , ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) >. )
112 110 38 111 sylancr 
 |-  ( ph -> ( F ` ( ( 1st ` L ) ` X ) ) = <. ( 1st ` ( F ` ( ( 1st ` L ) ` X ) ) ) , ( 2nd ` ( F ` ( ( 1st ` L ) ` X ) ) ) >. )
113 1st2nd 
 |-  ( ( Rel ( P Func O ) /\ ( ( 1st ` ( O DiagFunc P ) ) ` X ) e. ( P Func O ) ) -> ( ( 1st ` ( O DiagFunc P ) ) ` X ) = <. ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) , ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) >. )
114 110 51 113 sylancr 
 |-  ( ph -> ( ( 1st ` ( O DiagFunc P ) ) ` X ) = <. ( 1st ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) , ( 2nd ` ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) >. )
115 109 112 114 3eqtr4d 
 |-  ( ph -> ( F ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) )