Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-struct Unicode version

Definition df-struct 11867
 Description: Define a structure with components in . This is not a requirement for groups, posets, etc., but it is a useful assumption for component extraction theorems. As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set to be extensible structures. Because of 0nelfun 5109, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 11878: Struct . Allowing an extensible structure to contain the empty set ensures that expressions like are structures without asserting or implying that , , and are sets (if or is a proper class, then , see opprc 3694). (Contributed by Mario Carneiro, 29-Aug-2015.)
Assertion
Ref Expression
df-struct Struct
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-struct
StepHypRef Expression
1 cstr 11861 . 2 Struct
2 vx . . . . . 6
32cv 1313 . . . . 5
4 cle 7765 . . . . . 6
5 cn 8680 . . . . . . 7
65, 5cxp 4505 . . . . . 6
74, 6cin 3038 . . . . 5
83, 7wcel 1463 . . . 4
9 vf . . . . . . 7
109cv 1313 . . . . . 6
11 c0 3331 . . . . . . 7
1211csn 3495 . . . . . 6
1310, 12cdif 3036 . . . . 5
1413wfun 5085 . . . 4
1510cdm 4507 . . . . 5
16 cfz 9741 . . . . . 6
173, 16cfv 5091 . . . . 5
1815, 17wss 3039 . . . 4
198, 14, 18w3a 945 . . 3
2019, 9, 2copab 3956 . 2
211, 20wceq 1314 1 Struct
 Colors of variables: wff set class This definition is referenced by:  brstruct  11874  isstruct2im  11875  isstruct2r  11876
 Copyright terms: Public domain W3C validator