Definition df-dim

Description: Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim , all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023)

	Ref	Expression
Assertion	df-dim	⊢ dim = ( 𝑓 ∈ V ↦ ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldim	⊢ dim
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		chash	⊢ ♯
4		clbs	⊢ LBasis
5	1	cv	⊢ 𝑓
6	5 4	cfv	⊢ ( LBasis ‘ 𝑓 )
7	3 6	cima	⊢ ( ♯ “ ( LBasis ‘ 𝑓 ) )
8	7	cuni	⊢ ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) )
9	1 2 8	cmpt	⊢ ( 𝑓 ∈ V ↦ ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) ) )
10	0 9	wceq	⊢ dim = ( 𝑓 ∈ V ↦ ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) ) )