Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-tag Structured version   Visualization version   GIF version

Definition df-bj-tag 34788
Description: Definition of the tagged copy of a class, that is, the adjunction to (an isomorph of) 𝐴 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.)
Assertion
Ref Expression
df-bj-tag tag 𝐴 = (sngl 𝐴 ∪ {∅})

Detailed syntax breakdown of Definition df-bj-tag
StepHypRef Expression
1 cA . . 3 class 𝐴
21bj-ctag 34787 . 2 class tag 𝐴
31bj-csngl 34778 . . 3 class sngl 𝐴
4 c0 4211 . . . 4 class
54csn 4516 . . 3 class {∅}
63, 5cun 3841 . 2 class (sngl 𝐴 ∪ {∅})
72, 6wceq 1542 1 wff tag 𝐴 = (sngl 𝐴 ∪ {∅})
Colors of variables: wff setvar class
This definition is referenced by:  bj-tageq  34789  bj-eltag  34790  bj-0eltag  34791  bj-tagss  34793  bj-snglsstag  34794  bj-sngltag  34796  bj-tagex  34800
  Copyright terms: Public domain W3C validator