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 (N \in V \land R \in V) \to {Base}_{(N Mat R)} = \emptyset$

Step	Hyp	Ref	Expression
1		df-mat	$⊢ Mat = (n \in Fin, r \in V ⟼ (r freeLMod (n \times n)) sSet ⟨\cdot_{ndx}, r maMul ⟨n, n, n⟩⟩)$
2	1	reldmmpo	$⊢ Rel dom Mat$
3	2	ovprc	$⊢ \neg (N \in V \land R \in V) \to N Mat R = \emptyset$
4	3	fveq2d	$⊢ \neg (N \in V \land R \in V) \to {Base}_{(N Mat R)} = {Base}_{\emptyset}$
5		base0	$⊢ \emptyset = {Base}_{\emptyset}$
6	4 5	eqtr4di	$⊢ \neg (N \in V \land R \in V) \to {Base}_{(N Mat R)} = \emptyset$

Metamath Proof Explorer