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