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 =\left(f\in \mathrm{V}⟼\bigcup \left|.\right|\left[\mathrm{LBasis}\left(f\right)\right]\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldim	$$class\dim$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		chash	$$class\left|.\right|$$
4		clbs	$$class\mathrm{LBasis}$$
5	1	cv	$$setvarf$$
6	5 4	cfv	$$class\mathrm{LBasis}\left(f\right)$$
7	3 6	cima	$$class\left|.\right|\left[\mathrm{LBasis}\left(f\right)\right]$$
8	7	cuni	$$class\bigcup \left|.\right|\left[\mathrm{LBasis}\left(f\right)\right]$$
9	1 2 8	cmpt	$$class\left(f\in \mathrm{V}⟼\bigcup \left|.\right|\left[\mathrm{LBasis}\left(f\right)\right]\right)$$
10	0 9	wceq	$$wff\dim =\left(f\in \mathrm{V}⟼\bigcup \left|.\right|\left[\mathrm{LBasis}\left(f\right)\right]\right)$$