Definition df-struct 12464

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 5235, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 12475: 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 3800). (Contributed by Mario Carneiro, 29-Aug-2015.)

Assertion

Ref	Expression
df-struct	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }

Distinct variable group:   x, f

Detailed syntax breakdown of Definition df-struct

Step	Hyp	Ref	Expression
1		cstr 12458	. 2 class Struct
2		vx	. . . . . 6 setvar x
3	2	cv 1352	. . . . 5 class x
4		cle 7993	. . . . . 6 class <_
5		cn 8919	. . . . . . 7 class NN
6	5, 5	cxp 4625	. . . . . 6 class ( NN X. NN )
7	4, 6	cin 3129	. . . . 5 class ( <_ i^i ( NN X. NN ) )
8	3, 7	wcel 2148	. . . 4 wff x e. ( <_ i^i ( NN X. NN ) )
9		vf	. . . . . . 7 setvar f
10	9	cv 1352	. . . . . 6 class f
11		c0 3423	. . . . . . 7 class (/)
12	11	csn 3593	. . . . . 6 class { (/) }
13	10, 12	cdif 3127	. . . . 5 class ( f \ { (/) } )
14	13	wfun 5211	. . . 4 wff Fun ( f \ { (/) } )
15	10	cdm 4627	. . . . 5 class dom f
16		cfz 10008	. . . . . 6 class ...
17	3, 16	cfv 5217	. . . . 5 class ( ... ` x )
18	15, 17	wss 3130	. . . 4 wff dom f C_ ( ... ` x )
19	8, 14, 18	w3a 978	. . 3 wff ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) )
20	19, 9, 2	copab 4064	. 2 class { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
21	1, 20	wceq 1353	1 wff Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }

This definition is referenced by:  brstruct  12471  isstruct2im  12472  isstruct2r  12473