Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-struct | Unicode version |
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 5216, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 12429: 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 3786). (Contributed by Mario Carneiro, 29-Aug-2015.) |
Ref | Expression |
---|---|
df-struct | Struct |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cstr 12412 | . 2 Struct | |
2 | vx | . . . . . 6 | |
3 | 2 | cv 1347 | . . . . 5 |
4 | cle 7955 | . . . . . 6 | |
5 | cn 8878 | . . . . . . 7 | |
6 | 5, 5 | cxp 4609 | . . . . . 6 |
7 | 4, 6 | cin 3120 | . . . . 5 |
8 | 3, 7 | wcel 2141 | . . . 4 |
9 | vf | . . . . . . 7 | |
10 | 9 | cv 1347 | . . . . . 6 |
11 | c0 3414 | . . . . . . 7 | |
12 | 11 | csn 3583 | . . . . . 6 |
13 | 10, 12 | cdif 3118 | . . . . 5 |
14 | 13 | wfun 5192 | . . . 4 |
15 | 10 | cdm 4611 | . . . . 5 |
16 | cfz 9965 | . . . . . 6 | |
17 | 3, 16 | cfv 5198 | . . . . 5 |
18 | 15, 17 | wss 3121 | . . . 4 |
19 | 8, 14, 18 | w3a 973 | . . 3 |
20 | 19, 9, 2 | copab 4049 | . 2 |
21 | 1, 20 | wceq 1348 | 1 Struct |
Colors of variables: wff set class |
This definition is referenced by: brstruct 12425 isstruct2im 12426 isstruct2r 12427 |
Copyright terms: Public domain | W3C validator |