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 𝑅 ) ) = ∅ ) |
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 𝑅 ) ) = ∅ ) |