Definition df-struct 17325

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 6557, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 17329: 𝐹 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 4855). This is used critically in strle1 17336, strle2 17337, strle3 17338 and strleun 17335 to avoid sethood hypotheses on the "payload" sets: without this, ipsstr 17507 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 17508, 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 21692. (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 17324	. 2 class Struct
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1568	. . . . 5 class 𝑥
4		cle 11344	. . . . . 6 class ≤
5		cn 12335	. . . . . . 7 class ℕ
6	5, 5	cxp 5648	. . . . . 6 class (ℕ × ℕ)
7	4, 6	cin 4089	. . . . 5 class ( ≤ ∩ (ℕ × ℕ))
8	3, 7	wcel 2144	. . . 4 wff 𝑥 ∈ ( ≤ ∩ (ℕ × ℕ))
9		vf	. . . . . . 7 setvar 𝑓
10	9	cv 1568	. . . . . 6 class 𝑓
11		c0 4278	. . . . . . 7 class ∅
12	11	csn 4583	. . . . . 6 class {∅}
13	10, 12	cdif 4045	. . . . 5 class (𝑓 ∖ {∅})
14	13	wfun 6532	. . . 4 wff Fun (𝑓 ∖ {∅})
15	10	cdm 5650	. . . . 5 class dom 𝑓
16		cfz 13639	. . . . . 6 class ...
17	3, 16	cfv 6538	. . . . 5 class (...‘𝑥)
18	15, 17	wss 3895	. . . 4 wff dom 𝑓 ⊆ (...‘𝑥)
19	8, 14, 18	w3a 1103	. . 3 wff (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))
20	19, 9, 2	copab 5166	. 2 class {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
21	1, 20	wceq 1569	1 wff Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}

This definition is used by:  brstruct  17326  isstruct2  17327