Step |
Hyp |
Ref |
Expression |
1 |
|
maxidln1.1 |
|- H = ( 2nd ` R ) |
2 |
|
maxidln1.2 |
|- U = ( GId ` H ) |
3 |
|
eqid |
|- ( 1st ` R ) = ( 1st ` R ) |
4 |
|
eqid |
|- ran ( 1st ` R ) = ran ( 1st ` R ) |
5 |
3 4
|
maxidlnr |
|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> M =/= ran ( 1st ` R ) ) |
6 |
|
maxidlidl |
|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> M e. ( Idl ` R ) ) |
7 |
3 1 4 2
|
1idl |
|- ( ( R e. RingOps /\ M e. ( Idl ` R ) ) -> ( U e. M <-> M = ran ( 1st ` R ) ) ) |
8 |
7
|
necon3bbid |
|- ( ( R e. RingOps /\ M e. ( Idl ` R ) ) -> ( -. U e. M <-> M =/= ran ( 1st ` R ) ) ) |
9 |
6 8
|
syldan |
|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> ( -. U e. M <-> M =/= ran ( 1st ` R ) ) ) |
10 |
5 9
|
mpbird |
|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> -. U e. M ) |