Description: A constructed two-slot structure. Version of 2strstr not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020) (Proof shortened by AV, 17-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2str1.g | |- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. } |
|
2str1.b | |- ( Base ` ndx ) < N |
||
2str1.n | |- N e. NN |
||
Assertion | 2strstr1 | |- G Struct <. ( Base ` ndx ) , N >. |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2str1.g | |- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. } |
|
2 | 2str1.b | |- ( Base ` ndx ) < N |
|
3 | 2str1.n | |- N e. NN |
|
4 | basendxnn | |- ( Base ` ndx ) e. NN |
|
5 | eqid | |- ( Base ` ndx ) = ( Base ` ndx ) |
|
6 | eqid | |- N = N |
|
7 | 4 5 2 3 6 | strle2 | |- { <. ( Base ` ndx ) , B >. , <. N , .+ >. } Struct <. ( Base ` ndx ) , N >. |
8 | 1 7 | eqbrtri | |- G Struct <. ( Base ` ndx ) , N >. |