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

Definition df-bj-tag 31613
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.)
Assertion
Ref Expression
df-bj-tag  |- tag  A  =  (sngl  A  u.  { (/)
} )

Detailed syntax breakdown of Definition df-bj-tag
StepHypRef Expression
1 cA . . 3  class  A
21bj-ctag 31612 . 2  class tag  A
31bj-csngl 31603 . . 3  class sngl  A
4 c0 3742 . . . 4  class  (/)
54csn 3979 . . 3  class  { (/) }
63, 5cun 3413 . 2  class  (sngl  A  u.  { (/) } )
72, 6wceq 1454 1  wff tag  A  =  (sngl  A  u.  { (/)
} )
Colors of variables: wff setvar class
This definition is referenced by:  bj-tageq  31614  bj-eltag  31615  bj-0eltag  31616  bj-tagss  31618  bj-snglsstag  31619  bj-sngltag  31621  bj-tagex  31625
  Copyright terms: Public domain W3C validator