Metamath Proof Explorer


Theorem srngbase

Description: The base set of a constructed star ring. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypothesis srngstr.r โŠข ๐‘… = ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , + โŸฉ , โŸจ ( .r โ€˜ ndx ) , ยท โŸฉ } โˆช { โŸจ ( *๐‘Ÿ โ€˜ ndx ) , โˆ— โŸฉ } )
Assertion srngbase ( ๐ต โˆˆ ๐‘‹ โ†’ ๐ต = ( Base โ€˜ ๐‘… ) )

Proof

Step Hyp Ref Expression
1 srngstr.r โŠข ๐‘… = ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , + โŸฉ , โŸจ ( .r โ€˜ ndx ) , ยท โŸฉ } โˆช { โŸจ ( *๐‘Ÿ โ€˜ ndx ) , โˆ— โŸฉ } )
2 1 srngstr โŠข ๐‘… Struct โŸจ 1 , 4 โŸฉ
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 ) , ยท โŸฉ } โˆช { โŸจ ( *๐‘Ÿ โ€˜ ndx ) , โˆ— โŸฉ } )
6 5 1 sseqtrri โŠข { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , + โŸฉ , โŸจ ( .r โ€˜ ndx ) , ยท โŸฉ } โІ ๐‘…
7 4 6 sstri โŠข { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ } โІ ๐‘…
8 2 3 7 strfv โŠข ( ๐ต โˆˆ ๐‘‹ โ†’ ๐ต = ( Base โ€˜ ๐‘… ) )