Metamath Proof Explorer

Theorem yonedalem3a

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses yoneda.y 
|- Y = ( Yon ` C )
yoneda.b 
|- B = ( Base ` C )
yoneda.1 
|- .1. = ( Id ` C )
yoneda.o 
|- O = ( oppCat ` C )
yoneda.s 
|- S = ( SetCat ` U )
yoneda.t 
|- T = ( SetCat ` V )
yoneda.q 
|- Q = ( O FuncCat S )
yoneda.h 
|- H = ( HomF ` Q )
yoneda.r 
|- R = ( ( Q Xc. O ) FuncCat T )
yoneda.e 
|- E = ( O evalF S )
yoneda.z 
|- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
yoneda.c 
|- ( ph -> C e. Cat )
yoneda.w 
|- ( ph -> V e. W )
yoneda.u 
|- ( ph -> ran ( Homf ` C ) C_ U )
yoneda.v 
|- ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
yonedalem21.f 
|- ( ph -> F e. ( O Func S ) )
yonedalem21.x 
|- ( ph -> X e. B )
yonedalem3a.m 
|- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
Assertion yonedalem3a 
|- ( ph -> ( ( F M X ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) /\ ( F M X ) : ( F ( 1st ` Z ) X ) --> ( F ( 1st ` E ) X ) ) )

Proof

Step Hyp Ref Expression
1 yoneda.y 
 |-  Y = ( Yon ` C )
2 yoneda.b 
 |-  B = ( Base ` C )
3 yoneda.1 
 |-  .1. = ( Id ` C )
4 yoneda.o 
 |-  O = ( oppCat ` C )
5 yoneda.s 
 |-  S = ( SetCat ` U )
6 yoneda.t 
 |-  T = ( SetCat ` V )
7 yoneda.q 
 |-  Q = ( O FuncCat S )
8 yoneda.h 
 |-  H = ( HomF ` Q )
9 yoneda.r 
 |-  R = ( ( Q Xc. O ) FuncCat T )
10 yoneda.e 
 |-  E = ( O evalF S )
11 yoneda.z 
 |-  Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
12 yoneda.c 
 |-  ( ph -> C e. Cat )
13 yoneda.w 
 |-  ( ph -> V e. W )
14 yoneda.u 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
15 yoneda.v 
 |-  ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
16 yonedalem21.f 
 |-  ( ph -> F e. ( O Func S ) )
17 yonedalem21.x 
 |-  ( ph -> X e. B )
18 yonedalem3a.m 
 |-  M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
19 simpr 
 |-  ( ( f = F /\ x = X ) -> x = X )
20 19 fveq2d 
 |-  ( ( f = F /\ x = X ) -> ( ( 1st ` Y ) ` x ) = ( ( 1st ` Y ) ` X ) )
21 simpl 
 |-  ( ( f = F /\ x = X ) -> f = F )
22 20 21 oveq12d 
 |-  ( ( f = F /\ x = X ) -> ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) = ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )
23 19 fveq2d 
 |-  ( ( f = F /\ x = X ) -> ( a ` x ) = ( a ` X ) )
24 19 fveq2d 
 |-  ( ( f = F /\ x = X ) -> ( .1. ` x ) = ( .1. ` X ) )
25 23 24 fveq12d 
 |-  ( ( f = F /\ x = X ) -> ( ( a ` x ) ` ( .1. ` x ) ) = ( ( a ` X ) ` ( .1. ` X ) ) )
26 22 25 mpteq12dv 
 |-  ( ( f = F /\ x = X ) -> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) )
27 ovex 
 |-  ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) e. _V
28 27 mptex 
 |-  ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) e. _V
29 26 18 28 ovmpoa 
 |-  ( ( F e. ( O Func S ) /\ X e. B ) -> ( F M X ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) )
30 16 17 29 syl2anc 
 |-  ( ph -> ( F M X ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) )
31 eqid 
 |-  ( O Nat S ) = ( O Nat S )
32 simpr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )
33 31 32 nat1st2nd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> a e. ( <. ( 1st ` ( ( 1st ` Y ) ` X ) ) , ( 2nd ` ( ( 1st ` Y ) ` X ) ) >. ( O Nat S ) <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
34 4 2 oppcbas 
 |-  B = ( Base ` O )
35 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
36 17 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> X e. B )
37 31 33 34 35 36 natcl 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( a ` X ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` X ) ) )
38 15 unssbd 
 |-  ( ph -> U C_ V )
39 13 38 ssexd 
 |-  ( ph -> U e. _V )
40 39 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> U e. _V )
41 eqid 
 |-  ( Base ` S ) = ( Base ` S )
42 relfunc 
 |-  Rel ( O Func S )
43 1 2 12 17 4 5 39 14 yon1cl 
 |-  ( ph -> ( ( 1st ` Y ) ` X ) e. ( O Func S ) )
44 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ ( ( 1st ` Y ) ` X ) e. ( O Func S ) ) -> ( 1st ` ( ( 1st ` Y ) ` X ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` X ) ) )
45 42 43 44 sylancr 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` X ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` X ) ) )
46 34 41 45 funcf1 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> ( Base ` S ) )
47 46 17 ffvelrnd 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) e. ( Base ` S ) )
48 5 39 setcbas 
 |-  ( ph -> U = ( Base ` S ) )
49 47 48 eleqtrrd 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) e. U )
50 49 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) e. U )
51 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ F e. ( O Func S ) ) -> ( 1st ` F ) ( O Func S ) ( 2nd ` F ) )
52 42 16 51 sylancr 
 |-  ( ph -> ( 1st ` F ) ( O Func S ) ( 2nd ` F ) )
53 34 41 52 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` S ) )
54 53 17 ffvelrnd 
 |-  ( ph -> ( ( 1st ` F ) ` X ) e. ( Base ` S ) )
55 54 48 eleqtrrd 
 |-  ( ph -> ( ( 1st ` F ) ` X ) e. U )
56 55 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( 1st ` F ) ` X ) e. U )
57 5 40 35 50 56 elsetchom 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` X ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` X ) ) <-> ( a ` X ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) --> ( ( 1st ` F ) ` X ) ) )
58 37 57 mpbid 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( a ` X ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) --> ( ( 1st ` F ) ` X ) )
59 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
60 2 59 3 12 17 catidcl 
 |-  ( ph -> ( .1. ` X ) e. ( X ( Hom ` C ) X ) )
61 1 2 12 17 59 17 yon11 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) = ( X ( Hom ` C ) X ) )
62 60 61 eleqtrrd 
 |-  ( ph -> ( .1. ` X ) e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) )
63 62 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( .1. ` X ) e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) )
64 58 63 ffvelrnd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` X ) ` ( .1. ` X ) ) e. ( ( 1st ` F ) ` X ) )
65 64 fmpttd 
 |-  ( ph -> ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) : ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) --> ( ( 1st ` F ) ` X ) )
66 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 yonedalem21 
 |-  ( ph -> ( F ( 1st ` Z ) X ) = ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )
67 4 oppccat 
 |-  ( C e. Cat -> O e. Cat )
68 12 67 syl 
 |-  ( ph -> O e. Cat )
69 5 setccat 
 |-  ( U e. _V -> S e. Cat )
70 39 69 syl 
 |-  ( ph -> S e. Cat )
71 10 68 70 34 16 17 evlf1 
 |-  ( ph -> ( F ( 1st ` E ) X ) = ( ( 1st ` F ) ` X ) )
72 30 66 71 feq123d 
 |-  ( ph -> ( ( F M X ) : ( F ( 1st ` Z ) X ) --> ( F ( 1st ` E ) X ) <-> ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) : ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) --> ( ( 1st ` F ) ` X ) ) )
73 65 72 mpbird 
 |-  ( ph -> ( F M X ) : ( F ( 1st ` Z ) X ) --> ( F ( 1st ` E ) X ) )
74 30 73 jca 
 |-  ( ph -> ( ( F M X ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) /\ ( F M X ) : ( F ( 1st ` Z ) X ) --> ( F ( 1st ` E ) X ) ) )