Description: The base set of a submagma. (Contributed by AV, 26-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | submgmmgm.h | ⊢ 𝐻 = ( 𝑀 ↾s 𝑆 ) | |
Assertion | submgmbas | ⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑆 = ( Base ‘ 𝐻 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | submgmmgm.h | ⊢ 𝐻 = ( 𝑀 ↾s 𝑆 ) | |
2 | eqid | ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) | |
3 | 2 | submgmss | ⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) ) |
4 | 1 2 | ressbas2 | ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → 𝑆 = ( Base ‘ 𝐻 ) ) |
5 | 3 4 | syl | ⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑆 = ( Base ‘ 𝐻 ) ) |