Step |
Hyp |
Ref |
Expression |
1 |
|
upeu3.i |
|
2 |
|
upeu3.o |
Could not format ( ph -> .o. = ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) ) : No typesetting found for |- ( ph -> .o. = ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) ) with typecode |- |
3 |
|
upeu3.x |
Could not format ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode |- |
4 |
|
upeu4.k |
|
5 |
|
upeu4.n |
Could not format ( ph -> N = ( ( ( X G Y ) ` K ) .o. M ) ) : No typesetting found for |- ( ph -> N = ( ( ( X G Y ) ` K ) .o. M ) ) with typecode |- |
6 |
|
eqid |
|
7 |
|
eqid |
|
8 |
|
eqid |
|
9 |
|
eqid |
|
10 |
|
eqid |
|
11 |
3
|
uprcl2 |
|
12 |
3 6
|
uprcl4 |
|
13 |
11
|
funcrcl2 |
|
14 |
|
isofn |
|
15 |
13 14
|
syl |
|
16 |
1
|
fneq1d |
|
17 |
15 16
|
mpbird |
|
18 |
|
fnov |
|
19 |
17 18
|
sylib |
|
20 |
19
|
oveqd |
|
21 |
4 20
|
eleqtrd |
|
22 |
|
eqid |
|
23 |
22
|
elmpocl2 |
|
24 |
21 23
|
syl |
|
25 |
3 7
|
uprcl3 |
|
26 |
3 9
|
uprcl5 |
|
27 |
6 8 9 10 3
|
isup2 |
|
28 |
|
eqid |
|
29 |
1
|
oveqd |
|
30 |
4 29
|
eleqtrd |
|
31 |
2
|
oveqd |
Could not format ( ph -> ( ( ( X G Y ) ` K ) .o. M ) = ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) : No typesetting found for |- ( ph -> ( ( ( X G Y ) ` K ) .o. M ) = ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) with typecode |- |
32 |
5 31
|
eqtrd |
|
33 |
6 7 8 9 10 11 12 24 25 26 27 28 30 32
|
upeu2 |
|
34 |
33
|
simprd |
|
35 |
33
|
simpld |
|
36 |
6 7 8 9 10 25 11 24 35
|
isup |
Could not format ( ph -> ( Y ( <. F , G >. ( D UP E ) W ) N <-> A. y e. ( Base ` D ) A. g e. ( W ( Hom ` E ) ( F ` y ) ) E! k e. ( Y ( Hom ` D ) y ) g = ( ( ( Y G y ) ` k ) ( <. W , ( F ` Y ) >. ( comp ` E ) ( F ` y ) ) N ) ) ) : No typesetting found for |- ( ph -> ( Y ( <. F , G >. ( D UP E ) W ) N <-> A. y e. ( Base ` D ) A. g e. ( W ( Hom ` E ) ( F ` y ) ) E! k e. ( Y ( Hom ` D ) y ) g = ( ( ( Y G y ) ` k ) ( <. W , ( F ` Y ) >. ( comp ` E ) ( F ` y ) ) N ) ) ) with typecode |- |
37 |
34 36
|
mpbird |
Could not format ( ph -> Y ( <. F , G >. ( D UP E ) W ) N ) : No typesetting found for |- ( ph -> Y ( <. F , G >. ( D UP E ) W ) N ) with typecode |- |