Definition df-bj-tag

Description: Definition of the tagged copy of a class, that is, the adjunction to (an isomorph of) A of a disjoint element (here, the empty set). Remark: this could be used for the one-point compactification of a topological space. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	df-bj-tag	$$⊢tagA=snglA\cup \left\{\varnothing \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	bj-ctag	$$classtagA$$
2	0	bj-csngl	$$classsnglA$$
3		c0	$$class\varnothing$$
4	3	csn	$$class\left\{\varnothing \right\}$$
5	2 4	cun	$$class\left(snglA\cup \left\{\varnothing \right\}\right)$$
6	1 5	wceq	$$wfftagA=snglA\cup \left\{\varnothing \right\}$$