Metamath Proof Explorer

Theorem uptrlem3

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

Ref Expression
Hypotheses uptr.y 
|- ( ph -> ( R ` X ) = Y )
uptr.r 
|- ( ph -> R ( ( D Full E ) i^i ( D Faith E ) ) S )
uptr.k 
|- ( ph -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. )
uptr.b 
|- B = ( Base ` D )
uptr.x 
|- ( ph -> X e. B )
uptr.f 
|- ( ph -> F ( C Func D ) G )
uptr.n 
|- ( ph -> ( ( X S ( F ` Z ) ) ` M ) = N )
uptr.j 
|- J = ( Hom ` D )
uptr.m 
|- ( ph -> M e. ( X J ( F ` Z ) ) )
uptrlem3.a 
|- A = ( Base ` C )
uptrlem3.z 
|- ( ph -> Z e. A )
Assertion uptrlem3 
|- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) )

Proof

Step Hyp Ref Expression
1 uptr.y 
 |-  ( ph -> ( R ` X ) = Y )
2 uptr.r 
 |-  ( ph -> R ( ( D Full E ) i^i ( D Faith E ) ) S )
3 uptr.k 
 |-  ( ph -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. )
4 uptr.b 
 |-  B = ( Base ` D )
5 uptr.x 
 |-  ( ph -> X e. B )
6 uptr.f 
 |-  ( ph -> F ( C Func D ) G )
7 uptr.n 
 |-  ( ph -> ( ( X S ( F ` Z ) ) ` M ) = N )
8 uptr.j 
 |-  J = ( Hom ` D )
9 uptr.m 
 |-  ( ph -> M e. ( X J ( F ` Z ) ) )
10 uptrlem3.a 
 |-  A = ( Base ` C )
11 uptrlem3.z 
 |-  ( ph -> Z e. A )
12 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
13 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
14 eqid 
 |-  ( comp ` D ) = ( comp ` D )
15 eqid 
 |-  ( comp ` E ) = ( comp ` E )
16 5 4 eleqtrdi 
 |-  ( ph -> X e. ( Base ` D ) )
17 16 adantr 
 |-  ( ( ph /\ y e. A ) -> X e. ( Base ` D ) )
18 1 adantr 
 |-  ( ( ph /\ y e. A ) -> ( R ` X ) = Y )
19 11 10 eleqtrdi 
 |-  ( ph -> Z e. ( Base ` C ) )
20 19 adantr 
 |-  ( ( ph /\ y e. A ) -> Z e. ( Base ` C ) )
21 simpr 
 |-  ( ( ph /\ y e. A ) -> y e. A )
22 21 10 eleqtrdi 
 |-  ( ( ph /\ y e. A ) -> y e. ( Base ` C ) )
23 9 adantr 
 |-  ( ( ph /\ y e. A ) -> M e. ( X J ( F ` Z ) ) )
24 7 adantr 
 |-  ( ( ph /\ y e. A ) -> ( ( X S ( F ` Z ) ) ` M ) = N )
25 6 adantr 
 |-  ( ( ph /\ y e. A ) -> F ( C Func D ) G )
26 2 adantr 
 |-  ( ( ph /\ y e. A ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S )
27 3 adantr 
 |-  ( ( ph /\ y e. A ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. )
28 12 8 13 14 15 17 18 20 22 23 24 25 26 27 uptrlem1 
 |-  ( ( ph /\ y e. A ) -> ( A. h e. ( Y ( Hom ` E ) ( K ` y ) ) E! k e. ( Z ( Hom ` C ) y ) h = ( ( ( Z L y ) ` k ) ( <. Y , ( K ` Z ) >. ( comp ` E ) ( K ` y ) ) N ) <-> A. g e. ( X J ( F ` y ) ) E! k e. ( Z ( Hom ` C ) y ) g = ( ( ( Z G y ) ` k ) ( <. X , ( F ` Z ) >. ( comp ` D ) ( F ` y ) ) M ) ) )
29 28 ralbidva 
 |-  ( ph -> ( A. y e. A A. h e. ( Y ( Hom ` E ) ( K ` y ) ) E! k e. ( Z ( Hom ` C ) y ) h = ( ( ( Z L y ) ` k ) ( <. Y , ( K ` Z ) >. ( comp ` E ) ( K ` y ) ) N ) <-> A. y e. A A. g e. ( X J ( F ` y ) ) E! k e. ( Z ( Hom ` C ) y ) g = ( ( ( Z G y ) ` k ) ( <. X , ( F ` Z ) >. ( comp ` D ) ( F ` y ) ) M ) ) )
30 eqid 
 |-  ( Base ` E ) = ( Base ` E )
31 inss1 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Full E )
32 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
33 31 32 sstri 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Func E )
34 33 ssbri 
 |-  ( R ( ( D Full E ) i^i ( D Faith E ) ) S -> R ( D Func E ) S )
35 2 34 syl 
 |-  ( ph -> R ( D Func E ) S )
36 4 30 35 funcf1 
 |-  ( ph -> R : B --> ( Base ` E ) )
37 36 5 ffvelcdmd 
 |-  ( ph -> ( R ` X ) e. ( Base ` E ) )
38 1 37 eqeltrrd 
 |-  ( ph -> Y e. ( Base ` E ) )
39 6 35 cofucla 
 |-  ( ph -> ( <. R , S >. o.func <. F , G >. ) e. ( C Func E ) )
40 3 39 eqeltrrd 
 |-  ( ph -> <. K , L >. e. ( C Func E ) )
41 df-br 
 |-  ( K ( C Func E ) L <-> <. K , L >. e. ( C Func E ) )
42 40 41 sylibr 
 |-  ( ph -> K ( C Func E ) L )
43 10 4 6 funcf1 
 |-  ( ph -> F : A --> B )
44 43 11 ffvelcdmd 
 |-  ( ph -> ( F ` Z ) e. B )
45 4 8 13 35 5 44 funcf2 
 |-  ( ph -> ( X S ( F ` Z ) ) : ( X J ( F ` Z ) ) --> ( ( R ` X ) ( Hom ` E ) ( R ` ( F ` Z ) ) ) )
46 45 9 ffvelcdmd 
 |-  ( ph -> ( ( X S ( F ` Z ) ) ` M ) e. ( ( R ` X ) ( Hom ` E ) ( R ` ( F ` Z ) ) ) )
47 10 6 35 3 11 cofu1a 
 |-  ( ph -> ( R ` ( F ` Z ) ) = ( K ` Z ) )
48 1 47 oveq12d 
 |-  ( ph -> ( ( R ` X ) ( Hom ` E ) ( R ` ( F ` Z ) ) ) = ( Y ( Hom ` E ) ( K ` Z ) ) )
49 46 7 48 3eltr3d 
 |-  ( ph -> N e. ( Y ( Hom ` E ) ( K ` Z ) ) )
50 10 30 12 13 15 38 42 11 49 isup 
 |-  ( ph -> ( Z ( <. K , L >. ( C UP E ) Y ) N <-> A. y e. A A. h e. ( Y ( Hom ` E ) ( K ` y ) ) E! k e. ( Z ( Hom ` C ) y ) h = ( ( ( Z L y ) ` k ) ( <. Y , ( K ` Z ) >. ( comp ` E ) ( K ` y ) ) N ) ) )
51 10 4 12 8 14 5 6 11 9 isup 
 |-  ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> A. y e. A A. g e. ( X J ( F ` y ) ) E! k e. ( Z ( Hom ` C ) y ) g = ( ( ( Z G y ) ` k ) ( <. X , ( F ` Z ) >. ( comp ` D ) ( F ` y ) ) M ) ) )
52 29 50 51 3bitr4rd 
 |-  ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) )