# 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 ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}=\varnothing$

### Proof

Step Hyp Ref Expression
1 df-mat ${⊢}\mathrm{Mat}=\left({n}\in \mathrm{Fin},{r}\in \mathrm{V}⟼\left({r}\mathrm{freeLMod}\left({n}×{n}\right)\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{r}\mathrm{maMul}⟨{n},{n},{n}⟩⟩\right)$
2 1 reldmmpo ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{Mat}$
3 2 ovprc ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {N}\mathrm{Mat}{R}=\varnothing$
4 3 fveq2d ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}={\mathrm{Base}}_{\varnothing }$
5 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
6 4 5 eqtr4di ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}=\varnothing$