Metamath Proof Explorer
Description: The base set of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015)
|
|
Ref |
Expression |
|
Hypotheses |
opsrbas.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
|
|
opsrbas.o |
⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) |
|
|
opsrbas.t |
⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) ) |
|
Assertion |
opsrbas |
⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑂 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
opsrbas.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
2 |
|
opsrbas.o |
⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) |
3 |
|
opsrbas.t |
⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) ) |
4 |
|
df-base |
⊢ Base = Slot 1 |
5 |
|
1nn |
⊢ 1 ∈ ℕ |
6 |
|
1lt10 |
⊢ 1 < ; 1 0 |
7 |
1 2 3 4 5 6
|
opsrbaslem |
⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑂 ) ) |