Metamath Proof Explorer

Theorem uptrlem1

Description: Lemma for uptr . (Contributed by Zhi Wang, 16-Nov-2025)

Ref Expression
Hypotheses uptrlem1.h 
|- H = ( Hom ` C )
uptrlem1.i 
|- I = ( Hom ` D )
uptrlem1.j 
|- J = ( Hom ` E )
uptrlem1.d 
|- .xb = ( comp ` D )
uptrlem1.e 
|- .o. = ( comp ` E )
uptrlem1.x 
|- ( ph -> X e. ( Base ` D ) )
uptrlem1.y 
|- ( ph -> ( M ` X ) = Y )
uptrlem1.z 
|- ( ph -> Z e. ( Base ` C ) )
uptrlem1.w 
|- ( ph -> W e. ( Base ` C ) )
uptrlem1.a 
|- ( ph -> A e. ( X I ( F ` Z ) ) )
uptrlem1.b 
|- ( ph -> ( ( X N ( F ` Z ) ) ` A ) = B )
uptrlem1.f 
|- ( ph -> F ( C Func D ) G )
uptrlem1.m 
|- ( ph -> M ( ( D Full E ) i^i ( D Faith E ) ) N )
uptrlem1.k 
|- ( ph -> ( <. M , N >. o.func <. F , G >. ) = <. K , L >. )
Assertion uptrlem1 
|- ( ph -> ( A. h e. ( Y J ( K ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> A. g e. ( X I ( F ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) )

Proof

Step Hyp Ref Expression
1 uptrlem1.h 
 |-  H = ( Hom ` C )
2 uptrlem1.i 
 |-  I = ( Hom ` D )
3 uptrlem1.j 
 |-  J = ( Hom ` E )
4 uptrlem1.d 
 |-  .xb = ( comp ` D )
5 uptrlem1.e 
 |-  .o. = ( comp ` E )
6 uptrlem1.x 
 |-  ( ph -> X e. ( Base ` D ) )
7 uptrlem1.y 
 |-  ( ph -> ( M ` X ) = Y )
8 uptrlem1.z 
 |-  ( ph -> Z e. ( Base ` C ) )
9 uptrlem1.w 
 |-  ( ph -> W e. ( Base ` C ) )
10 uptrlem1.a 
 |-  ( ph -> A e. ( X I ( F ` Z ) ) )
11 uptrlem1.b 
 |-  ( ph -> ( ( X N ( F ` Z ) ) ` A ) = B )
12 uptrlem1.f 
 |-  ( ph -> F ( C Func D ) G )
13 uptrlem1.m 
 |-  ( ph -> M ( ( D Full E ) i^i ( D Faith E ) ) N )
14 uptrlem1.k 
 |-  ( ph -> ( <. M , N >. o.func <. F , G >. ) = <. K , L >. )
15 eqid 
 |-  ( Base ` D ) = ( Base ` D )
16 eqid 
 |-  ( Base ` C ) = ( Base ` C )
17 16 15 12 funcf1 
 |-  ( ph -> F : ( Base ` C ) --> ( Base ` D ) )
18 17 9 ffvelcdmd 
 |-  ( ph -> ( F ` W ) e. ( Base ` D ) )
19 15 2 3 13 6 18 ffthf1o 
 |-  ( ph -> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-onto-> ( ( M ` X ) J ( M ` ( F ` W ) ) ) )
20 inss1 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Full E )
21 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
22 20 21 sstri 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Func E )
23 22 ssbri 
 |-  ( M ( ( D Full E ) i^i ( D Faith E ) ) N -> M ( D Func E ) N )
24 13 23 syl 
 |-  ( ph -> M ( D Func E ) N )
25 16 12 24 14 9 cofu1a 
 |-  ( ph -> ( M ` ( F ` W ) ) = ( K ` W ) )
26 7 25 oveq12d 
 |-  ( ph -> ( ( M ` X ) J ( M ` ( F ` W ) ) ) = ( Y J ( K ` W ) ) )
27 26 f1oeq3d 
 |-  ( ph -> ( ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-onto-> ( ( M ` X ) J ( M ` ( F ` W ) ) ) <-> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-onto-> ( Y J ( K ` W ) ) ) )
28 19 27 mpbid 
 |-  ( ph -> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-onto-> ( Y J ( K ` W ) ) )
29 f1of 
 |-  ( ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-onto-> ( Y J ( K ` W ) ) -> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) --> ( Y J ( K ` W ) ) )
30 28 29 syl 
 |-  ( ph -> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) --> ( Y J ( K ` W ) ) )
31 30 ffvelcdmda 
 |-  ( ( ph /\ g e. ( X I ( F ` W ) ) ) -> ( ( X N ( F ` W ) ) ` g ) e. ( Y J ( K ` W ) ) )
32 f1ofo 
 |-  ( ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-onto-> ( Y J ( K ` W ) ) -> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -onto-> ( Y J ( K ` W ) ) )
33 28 32 syl 
 |-  ( ph -> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -onto-> ( Y J ( K ` W ) ) )
34 foelrn 
 |-  ( ( ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -onto-> ( Y J ( K ` W ) ) /\ h e. ( Y J ( K ` W ) ) ) -> E. g e. ( X I ( F ` W ) ) h = ( ( X N ( F ` W ) ) ` g ) )
35 33 34 sylan 
 |-  ( ( ph /\ h e. ( Y J ( K ` W ) ) ) -> E. g e. ( X I ( F ` W ) ) h = ( ( X N ( F ` W ) ) ` g ) )
36 simpl3 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> h = ( ( X N ( F ` W ) ) ` g ) )
37 36 eqeq1d 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> ( h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) )
38 24 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> M ( D Func E ) N )
39 6 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> X e. ( Base ` D ) )
40 17 8 ffvelcdmd 
 |-  ( ph -> ( F ` Z ) e. ( Base ` D ) )
41 40 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( F ` Z ) e. ( Base ` D ) )
42 18 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( F ` W ) e. ( Base ` D ) )
43 10 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> A e. ( X I ( F ` Z ) ) )
44 16 1 2 12 8 9 funcf2 
 |-  ( ph -> ( Z G W ) : ( Z H W ) --> ( ( F ` Z ) I ( F ` W ) ) )
45 44 adantr 
 |-  ( ( ph /\ g e. ( X I ( F ` W ) ) ) -> ( Z G W ) : ( Z H W ) --> ( ( F ` Z ) I ( F ` W ) ) )
46 45 ffvelcdmda 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( Z G W ) ` k ) e. ( ( F ` Z ) I ( F ` W ) ) )
47 15 2 4 5 38 39 41 42 43 46 funcco 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) = ( ( ( ( F ` Z ) N ( F ` W ) ) ` ( ( Z G W ) ` k ) ) ( <. ( M ` X ) , ( M ` ( F ` Z ) ) >. .o. ( M ` ( F ` W ) ) ) ( ( X N ( F ` Z ) ) ` A ) ) )
48 7 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( M ` X ) = Y )
49 16 12 24 14 8 cofu1a 
 |-  ( ph -> ( M ` ( F ` Z ) ) = ( K ` Z ) )
50 49 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( M ` ( F ` Z ) ) = ( K ` Z ) )
51 48 50 opeq12d 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> <. ( M ` X ) , ( M ` ( F ` Z ) ) >. = <. Y , ( K ` Z ) >. )
52 25 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( M ` ( F ` W ) ) = ( K ` W ) )
53 51 52 oveq12d 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( <. ( M ` X ) , ( M ` ( F ` Z ) ) >. .o. ( M ` ( F ` W ) ) ) = ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) )
54 12 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> F ( C Func D ) G )
55 14 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( <. M , N >. o.func <. F , G >. ) = <. K , L >. )
56 8 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> Z e. ( Base ` C ) )
57 9 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> W e. ( Base ` C ) )
58 simpr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> k e. ( Z H W ) )
59 16 54 38 55 56 57 1 58 cofu2a 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( F ` Z ) N ( F ` W ) ) ` ( ( Z G W ) ` k ) ) = ( ( Z L W ) ` k ) )
60 11 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( X N ( F ` Z ) ) ` A ) = B )
61 53 59 60 oveq123d 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( ( F ` Z ) N ( F ` W ) ) ` ( ( Z G W ) ` k ) ) ( <. ( M ` X ) , ( M ` ( F ` Z ) ) >. .o. ( M ` ( F ` W ) ) ) ( ( X N ( F ` Z ) ) ` A ) ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) )
62 47 61 eqtrd 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) )
63 62 eqeq2d 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) <-> ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) )
64 f1of1 
 |-  ( ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-onto-> ( Y J ( K ` W ) ) -> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-> ( Y J ( K ` W ) ) )
65 28 64 syl 
 |-  ( ph -> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-> ( Y J ( K ` W ) ) )
66 65 ad2antrr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-> ( Y J ( K ` W ) ) )
67 simplr 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> g e. ( X I ( F ` W ) ) )
68 38 funcrcl2 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> D e. Cat )
69 15 2 4 68 39 41 42 43 46 catcocl 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) e. ( X I ( F ` W ) ) )
70 f1fveq 
 |-  ( ( ( X N ( F ` W ) ) : ( X I ( F ` W ) ) -1-1-> ( Y J ( K ` W ) ) /\ ( g e. ( X I ( F ` W ) ) /\ ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) e. ( X I ( F ` W ) ) ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) )
71 66 67 69 70 syl12anc 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) )
72 63 71 bitr3d 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) )
73 72 3adantl3 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) )
74 37 73 bitrd 
 |-  ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> ( h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) )
75 74 reubidva 
 |-  ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) -> ( E! k e. ( Z H W ) h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> E! k e. ( Z H W ) g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) )
76 31 35 75 ralxfrd2 
 |-  ( ph -> ( A. h e. ( Y J ( K ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> A. g e. ( X I ( F ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) )