Definition df-cp

Description: Define the metric completion of the algebraic completion of the p -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	df-cp	|- Cp = ( cplMetSp o. _Qp )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccp	|- Cp
1		ccpms	|- cplMetSp
2		cqpa	|- _Qp
3	1 2	ccom	|- ( cplMetSp o. _Qp )
4	0 3	wceq	|- Cp = ( cplMetSp o. _Qp )