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 |
|
upeu3.y |
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 |- |
5 |
|
eqid |
|
6 |
|
eqid |
|
7 |
|
eqid |
|
8 |
|
eqid |
|
9 |
|
eqid |
|
10 |
3
|
uprcl2 |
|
11 |
3 5
|
uprcl4 |
|
12 |
4 5
|
uprcl4 |
|
13 |
3 6
|
uprcl3 |
|
14 |
3 8
|
uprcl5 |
|
15 |
5 7 8 9 3
|
isup2 |
|
16 |
4 8
|
uprcl5 |
|
17 |
5 7 8 9 4
|
isup2 |
|
18 |
5 6 7 8 9 10 11 12 13 14 15 16 17
|
upeu |
|
19 |
1
|
oveqd |
|
20 |
2
|
oveqd |
Could not format ( ph -> ( ( ( X G Y ) ` r ) .o. M ) = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) : No typesetting found for |- ( ph -> ( ( ( X G Y ) ` r ) .o. M ) = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) with typecode |- |
21 |
20
|
eqeq2d |
Could not format ( ph -> ( N = ( ( ( X G Y ) ` r ) .o. M ) <-> N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) ) : No typesetting found for |- ( ph -> ( N = ( ( ( X G Y ) ` r ) .o. M ) <-> N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) ) with typecode |- |
22 |
19 21
|
reueqbidv |
Could not format ( ph -> ( E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) <-> E! r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) ) : No typesetting found for |- ( ph -> ( E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) <-> E! r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) ) with typecode |- |
23 |
18 22
|
mpbird |
Could not format ( ph -> E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) ) : No typesetting found for |- ( ph -> E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) ) with typecode |- |