Step |
Hyp |
Ref |
Expression |
1 |
|
odrngstr.w |
⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ) |
2 |
1
|
odrngstr |
⊢ 𝑊 Struct ⟨ 1 , ; 1 2 ⟩ |
3 |
|
baseid |
⊢ Base = Slot ( Base ‘ ndx ) |
4 |
|
snsstp1 |
⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } |
5 |
|
ssun1 |
⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ) |
6 |
5 1
|
sseqtrri |
⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ⊆ 𝑊 |
7 |
4 6
|
sstri |
⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ 𝑊 |
8 |
2 3 7
|
strfv |
⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝑊 ) ) |