| 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 ) ) |