Metamath Proof Explorer

Theorem matbas0pc

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 ) ) = (/) )

Proof

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 ) ) = (/) )