Definition df-struct 15859

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 5906, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 15869: 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 4424). This is used critically in strle1 15973, strle2 15974, strle3 15975 and strleun 15972 to avoid sethood hypotheses on the "payload" sets: without this, ipsstr 16024 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 16025, which requires that the base set is a set but not any of the other components. Usually, a concrete structure like ℂ_fld does not contain the empty set, and therefore is a function, see cnfldfun 19758. (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 15853	. 2 class Struct
2		vx	. . . . . 6 setvar x
3	2	cv 1482	. . . . 5 class x
4		cle 10075	. . . . . 6 class <_
5		cn 11020	. . . . . . 7 class NN
6	5, 5	cxp 5112	. . . . . 6 class ( NN X. NN )
7	4, 6	cin 3573	. . . . 5 class ( <_ i^i ( NN X. NN ) )
8	3, 7	wcel 1990	. . . 4 wff x e. ( <_ i^i ( NN X. NN ) )
9		vf	. . . . . . 7 setvar f
10	9	cv 1482	. . . . . 6 class f
11		c0 3915	. . . . . . 7 class (/)
12	11	csn 4177	. . . . . 6 class { (/) }
13	10, 12	cdif 3571	. . . . 5 class ( f \ { (/) } )
14	13	wfun 5882	. . . 4 wff Fun ( f \ { (/) } )
15	10	cdm 5114	. . . . 5 class dom f
16		cfz 12326	. . . . . 6 class ...
17	3, 16	cfv 5888	. . . . 5 class ( ... ` x )
18	15, 17	wss 3574	. . . 4 wff dom f C_ ( ... ` x )
19	8, 14, 18	w3a 1037	. . 3 wff ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) )
20	19, 9, 2	copab 4712	. 2 class { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
21	1, 20	wceq 1483	1 wff Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }

This definition is referenced by:  brstruct  15866  isstruct2  15867