| Step |
Hyp |
Ref |
Expression |
| 1 |
|
srhmsubc.s |
|- A. r e. S r e. Ring |
| 2 |
|
srhmsubc.c |
|- C = ( U i^i S ) |
| 3 |
1 2
|
srhmsubclem1 |
|- ( X e. C -> X e. ( U i^i Ring ) ) |
| 4 |
3
|
adantl |
|- ( ( U e. V /\ X e. C ) -> X e. ( U i^i Ring ) ) |
| 5 |
|
eqid |
|- ( RingCat ` U ) = ( RingCat ` U ) |
| 6 |
|
eqid |
|- ( Base ` ( RingCat ` U ) ) = ( Base ` ( RingCat ` U ) ) |
| 7 |
|
id |
|- ( U e. V -> U e. V ) |
| 8 |
5 6 7
|
ringcbas |
|- ( U e. V -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) ) |
| 9 |
8
|
adantr |
|- ( ( U e. V /\ X e. C ) -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) ) |
| 10 |
4 9
|
eleqtrrd |
|- ( ( U e. V /\ X e. C ) -> X e. ( Base ` ( RingCat ` U ) ) ) |