Step |
Hyp |
Ref |
Expression |
1 |
|
opabssxp |
|- { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) } C_ ( Field X. Field ) |
2 |
|
df-br |
|- ( E /FldExt F <-> <. E , F >. e. /FldExt ) |
3 |
2
|
biimpi |
|- ( E /FldExt F -> <. E , F >. e. /FldExt ) |
4 |
|
df-fldext |
|- /FldExt = { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) } |
5 |
3 4
|
eleqtrdi |
|- ( E /FldExt F -> <. E , F >. e. { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) } ) |
6 |
1 5
|
sselid |
|- ( E /FldExt F -> <. E , F >. e. ( Field X. Field ) ) |
7 |
|
opelxp1 |
|- ( <. E , F >. e. ( Field X. Field ) -> E e. Field ) |
8 |
6 7
|
syl |
|- ( E /FldExt F -> E e. Field ) |