Description: Define a structure with components in M ... N . 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 , such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun : F Struct X -> Fun ( F \ { (/) } ) .
Allowing an extensible structure to contain the empty set ensures that expressions like { <. A , B >. , <. C , D >. } are structures without asserting or implying that A , B , C and D are sets (if A or B is a proper class, then <. A , B >. = (/) , see opprc ). This is used critically in strle1 , strle2 , strle3 and strleun to avoid sethood hypotheses on the "payload" sets: without this, ipsstr and theorems like it will have many sethood assumptions, and may not even be usable in the empty context. Instead, the sethood assumption is deferred until it is actually needed, e.g., ipsbase , which requires that the base set be a set but not any of the other components. Usually, a concrete structure like CCfld does not contain the empty set, and therefore is a function, see cnfldfun . (Contributed by Mario Carneiro, 29-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-struct | |- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cstr | |- Struct |
|
| 1 | vf | |- f |
|
| 2 | vx | |- x |
|
| 3 | 2 | cv | |- x |
| 4 | cle | |- <_ |
|
| 5 | cn | |- NN |
|
| 6 | 5 5 | cxp | |- ( NN X. NN ) |
| 7 | 4 6 | cin | |- ( <_ i^i ( NN X. NN ) ) |
| 8 | 3 7 | wcel | |- x e. ( <_ i^i ( NN X. NN ) ) |
| 9 | 1 | cv | |- f |
| 10 | c0 | |- (/) |
|
| 11 | 10 | csn | |- { (/) } |
| 12 | 9 11 | cdif | |- ( f \ { (/) } ) |
| 13 | 12 | wfun | |- Fun ( f \ { (/) } ) |
| 14 | 9 | cdm | |- dom f |
| 15 | cfz | |- ... |
|
| 16 | 3 15 | cfv | |- ( ... ` x ) |
| 17 | 14 16 | wss | |- dom f C_ ( ... ` x ) |
| 18 | 8 13 17 | w3a | |- ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) |
| 19 | 18 1 2 | copab | |- { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) } |
| 20 | 0 19 | wceq | |- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) } |