| Step |
Hyp |
Ref |
Expression |
| 1 |
|
idlsrgstr.1 |
⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } ) |
| 2 |
|
eqid |
⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } |
| 3 |
2
|
rngstr |
⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } Struct ⟨ 1 , 3 ⟩ |
| 4 |
|
9nn |
⊢ 9 ∈ ℕ |
| 5 |
|
tsetndx |
⊢ ( TopSet ‘ ndx ) = 9 |
| 6 |
|
9lt10 |
⊢ 9 < ; 1 0 |
| 7 |
|
10nn |
⊢ ; 1 0 ∈ ℕ |
| 8 |
|
plendx |
⊢ ( le ‘ ndx ) = ; 1 0 |
| 9 |
4 5 6 7 8
|
strle2 |
⊢ { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } Struct ⟨ 9 , ; 1 0 ⟩ |
| 10 |
|
3lt9 |
⊢ 3 < 9 |
| 11 |
3 9 10
|
strleun |
⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } ) Struct ⟨ 1 , ; 1 0 ⟩ |
| 12 |
1 11
|
eqbrtri |
⊢ 𝑊 Struct ⟨ 1 , ; 1 0 ⟩ |