Definition df-struct 16485

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 6373, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 16495: 𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}).

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 4826). This is used critically in strle1 16592, strle2 16593, strle3 16594 and strleun 16591 to avoid sethood hypotheses on the "payload" sets: without this, ipsstr 16643 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 16644, which requires that the base set be 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 20557. (Contributed by Mario Carneiro, 29-Aug-2015.)

Assertion

Ref	Expression
df-struct	⊢ Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}

Distinct variable group:   𝑥,𝑓

Detailed syntax breakdown of Definition df-struct

Step	Hyp	Ref	Expression
1		cstr 16479	. 2 class Struct
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1536	. . . . 5 class 𝑥
4		cle 10676	. . . . . 6 class ≤
5		cn 11638	. . . . . . 7 class ℕ
6	5, 5	cxp 5553	. . . . . 6 class (ℕ × ℕ)
7	4, 6	cin 3935	. . . . 5 class ( ≤ ∩ (ℕ × ℕ))
8	3, 7	wcel 2114	. . . 4 wff 𝑥 ∈ ( ≤ ∩ (ℕ × ℕ))
9		vf	. . . . . . 7 setvar 𝑓
10	9	cv 1536	. . . . . 6 class 𝑓
11		c0 4291	. . . . . . 7 class ∅
12	11	csn 4567	. . . . . 6 class {∅}
13	10, 12	cdif 3933	. . . . 5 class (𝑓 ∖ {∅})
14	13	wfun 6349	. . . 4 wff Fun (𝑓 ∖ {∅})
15	10	cdm 5555	. . . . 5 class dom 𝑓
16		cfz 12893	. . . . . 6 class ...
17	3, 16	cfv 6355	. . . . 5 class (...‘𝑥)
18	15, 17	wss 3936	. . . 4 wff dom 𝑓 ⊆ (...‘𝑥)
19	8, 14, 18	w3a 1083	. . 3 wff (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))
20	19, 9, 2	copab 5128	. 2 class {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
21	1, 20	wceq 1537	1 wff Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}

This definition is referenced by:  brstruct  16492  isstruct2  16493