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 5136, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 11961: 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 3721). (Contributed by Mario Carneiro, 29-Aug-2015.) |
Ref | Expression |
---|---|
df-struct | Struct |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cstr 11944 | . 2 Struct | |
2 | vx | . . . . . 6 | |
3 | 2 | cv 1330 | . . . . 5 |
4 | cle 7794 | . . . . . 6 | |
5 | cn 8713 | . . . . . . 7 | |
6 | 5, 5 | cxp 4532 | . . . . . 6 |
7 | 4, 6 | cin 3065 | . . . . 5 |
8 | 3, 7 | wcel 1480 | . . . 4 |
9 | vf | . . . . . . 7 | |
10 | 9 | cv 1330 | . . . . . 6 |
11 | c0 3358 | . . . . . . 7 | |
12 | 11 | csn 3522 | . . . . . 6 |
13 | 10, 12 | cdif 3063 | . . . . 5 |
14 | 13 | wfun 5112 | . . . 4 |
15 | 10 | cdm 4534 | . . . . 5 |
16 | cfz 9783 | . . . . . 6 | |
17 | 3, 16 | cfv 5118 | . . . . 5 |
18 | 15, 17 | wss 3066 | . . . 4 |
19 | 8, 14, 18 | w3a 962 | . . 3 |
20 | 19, 9, 2 | copab 3983 | . 2 |
21 | 1, 20 | wceq 1331 | 1 Struct |
Colors of variables: wff set class |
This definition is referenced by: brstruct 11957 isstruct2im 11958 isstruct2r 11959 |
Copyright terms: Public domain | W3C validator |