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	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-mat	⊢ Mat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) ⟩ ) )
2	1	reldmmpo	⊢ Rel dom Mat
3	2	ovprc	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 Mat 𝑅 ) = ∅ )
4	3	fveq2d	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ∅ ) )
5		base0	⊢ ∅ = ( Base ‘ ∅ )
6	4 5	eqtr4di	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )