Step |
Hyp |
Ref |
Expression |
1 |
|
odrngstr.w |
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) |
2 |
|
eqid |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } |
3 |
2
|
rngstr |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } Struct <. 1 , 3 >. |
4 |
|
9nn |
|- 9 e. NN |
5 |
|
tsetndx |
|- ( TopSet ` ndx ) = 9 |
6 |
|
9lt10 |
|- 9 < ; 1 0 |
7 |
|
10nn |
|- ; 1 0 e. NN |
8 |
|
plendx |
|- ( le ` ndx ) = ; 1 0 |
9 |
|
1nn0 |
|- 1 e. NN0 |
10 |
|
0nn0 |
|- 0 e. NN0 |
11 |
|
2nn |
|- 2 e. NN |
12 |
|
2pos |
|- 0 < 2 |
13 |
9 10 11 12
|
declt |
|- ; 1 0 < ; 1 2 |
14 |
9 11
|
decnncl |
|- ; 1 2 e. NN |
15 |
|
dsndx |
|- ( dist ` ndx ) = ; 1 2 |
16 |
4 5 6 7 8 13 14 15
|
strle3 |
|- { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } Struct <. 9 , ; 1 2 >. |
17 |
|
3lt9 |
|- 3 < 9 |
18 |
3 16 17
|
strleun |
|- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) Struct <. 1 , ; 1 2 >. |
19 |
1 18
|
eqbrtri |
|- W Struct <. 1 , ; 1 2 >. |