Step |
Hyp |
Ref |
Expression |
1 |
|
invisoinv.b |
|
2 |
|
invisoinv.i |
|
3 |
|
invisoinv.n |
|
4 |
|
invisoinv.c |
|
5 |
|
invisoinv.x |
|
6 |
|
invisoinv.y |
|
7 |
|
invisoinv.f |
|
8 |
|
invcoisoid.1 |
|
9 |
|
isocoinvid.o |
Could not format .o. = ( <. Y , X >. ( comp ` C ) Y ) : No typesetting found for |- .o. = ( <. Y , X >. ( comp ` C ) Y ) with typecode |- |
10 |
1 2 3 4 5 6 7
|
invisoinvl |
|
11 |
|
eqid |
|
12 |
1 3 4 6 5 11
|
isinv |
|
13 |
|
simpl |
|
14 |
12 13
|
syl6bi |
|
15 |
10 14
|
mpd |
|
16 |
|
eqid |
|
17 |
|
eqid |
|
18 |
1 16 2 4 6 5
|
isohom |
|
19 |
1 3 4 5 6 2
|
invf |
|
20 |
19 7
|
ffvelrnd |
|
21 |
18 20
|
sseldd |
|
22 |
1 16 2 4 5 6
|
isohom |
|
23 |
22 7
|
sseldd |
|
24 |
1 16 17 8 11 4 6 5 21 23
|
issect2 |
|
25 |
9
|
a1i |
Could not format ( ph -> .o. = ( <. Y , X >. ( comp ` C ) Y ) ) : No typesetting found for |- ( ph -> .o. = ( <. Y , X >. ( comp ` C ) Y ) ) with typecode |- |
26 |
25
|
eqcomd |
Could not format ( ph -> ( <. Y , X >. ( comp ` C ) Y ) = .o. ) : No typesetting found for |- ( ph -> ( <. Y , X >. ( comp ` C ) Y ) = .o. ) with typecode |- |
27 |
26
|
oveqd |
Could not format ( ph -> ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( F .o. ( ( X N Y ) ` F ) ) ) : No typesetting found for |- ( ph -> ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( F .o. ( ( X N Y ) ` F ) ) ) with typecode |- |
28 |
27
|
eqeq1d |
Could not format ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( .1. ` Y ) <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) : No typesetting found for |- ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( .1. ` Y ) <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) with typecode |- |
29 |
24 28
|
bitrd |
Could not format ( ph -> ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) : No typesetting found for |- ( ph -> ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) with typecode |- |
30 |
15 29
|
mpbid |
Could not format ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) : No typesetting found for |- ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) with typecode |- |