# Metamath Proof Explorer

## Theorem imasvalstr

Description: Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 30-Apr-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypothesis imasvalstr.u
Assertion imasvalstr ${⊢}{U}\mathrm{Struct}⟨1,12⟩$

### Proof

Step Hyp Ref Expression
1 imasvalstr.u
2 eqid
3 2 ipsstr
4 9nn ${⊢}9\in ℕ$
5 tsetndx ${⊢}\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$
6 9lt10 ${⊢}9<10$
7 10nn ${⊢}10\in ℕ$
8 plendx ${⊢}{\le }_{\mathrm{ndx}}=10$
9 1nn0 ${⊢}1\in {ℕ}_{0}$
10 0nn0 ${⊢}0\in {ℕ}_{0}$
11 2nn ${⊢}2\in ℕ$
12 2pos ${⊢}0<2$
13 9 10 11 12 declt ${⊢}10<12$
14 9 11 decnncl ${⊢}12\in ℕ$
15 dsndx ${⊢}\mathrm{dist}\left(\mathrm{ndx}\right)=12$
16 4 5 6 7 8 13 14 15 strle3 ${⊢}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{O}⟩,⟨{\le }_{\mathrm{ndx}},{L}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),{D}⟩\right\}\mathrm{Struct}⟨9,12⟩$
17 8lt9 ${⊢}8<9$
18 3 16 17 strleun
19 1 18 eqbrtri ${⊢}{U}\mathrm{Struct}⟨1,12⟩$