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 5188, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 12214: 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 3762). (Contributed by Mario Carneiro, 29-Aug-2015.) |
Ref | Expression |
---|---|
df-struct | Struct |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cstr 12197 | . 2 Struct | |
2 | vx | . . . . . 6 | |
3 | 2 | cv 1334 | . . . . 5 |
4 | cle 7913 | . . . . . 6 | |
5 | cn 8833 | . . . . . . 7 | |
6 | 5, 5 | cxp 4584 | . . . . . 6 |
7 | 4, 6 | cin 3101 | . . . . 5 |
8 | 3, 7 | wcel 2128 | . . . 4 |
9 | vf | . . . . . . 7 | |
10 | 9 | cv 1334 | . . . . . 6 |
11 | c0 3394 | . . . . . . 7 | |
12 | 11 | csn 3560 | . . . . . 6 |
13 | 10, 12 | cdif 3099 | . . . . 5 |
14 | 13 | wfun 5164 | . . . 4 |
15 | 10 | cdm 4586 | . . . . 5 |
16 | cfz 9912 | . . . . . 6 | |
17 | 3, 16 | cfv 5170 | . . . . 5 |
18 | 15, 17 | wss 3102 | . . . 4 |
19 | 8, 14, 18 | w3a 963 | . . 3 |
20 | 19, 9, 2 | copab 4024 | . 2 |
21 | 1, 20 | wceq 1335 | 1 Struct |
Colors of variables: wff set class |
This definition is referenced by: brstruct 12210 isstruct2im 12211 isstruct2r 12212 |
Copyright terms: Public domain | W3C validator |