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	⊢ tag 𝐴 = ( sngl 𝐴 ∪ { ∅ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	bj-ctag	⊢ tag 𝐴
2	0	bj-csngl	⊢ sngl 𝐴
3		c0	⊢ ∅
4	3	csn	⊢ { ∅ }
5	2 4	cun	⊢ ( sngl 𝐴 ∪ { ∅ } )
6	1 5	wceq	⊢ tag 𝐴 = ( sngl 𝐴 ∪ { ∅ } )