Description: There is no matrix with a proper class either as dimension or as underlying ring. (Contributed by AV, 28-Dec-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | matbas0pc | |- ( -. ( N e. _V /\ R e. _V ) -> ( Base ` ( N Mat R ) ) = (/) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mat | |- Mat = ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) ) |
|
2 | 1 | reldmmpo | |- Rel dom Mat |
3 | 2 | ovprc | |- ( -. ( N e. _V /\ R e. _V ) -> ( N Mat R ) = (/) ) |
4 | 3 | fveq2d | |- ( -. ( N e. _V /\ R e. _V ) -> ( Base ` ( N Mat R ) ) = ( Base ` (/) ) ) |
5 | base0 | |- (/) = ( Base ` (/) ) |
|
6 | 4 5 | eqtr4di | |- ( -. ( N e. _V /\ R e. _V ) -> ( Base ` ( N Mat R ) ) = (/) ) |