Definition df-struct 13332

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 5390, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 13343: 𝐹 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 3920). (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 13326	. 2 class Struct
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1401	. . . . 5 class 𝑥
4		cle 8351	. . . . . 6 class ≤
5		cn 9283	. . . . . . 7 class ℕ
6	5, 5	cxp 4767	. . . . . 6 class (ℕ × ℕ)
7	4, 6	cin 3219	. . . . 5 class ( ≤ ∩ (ℕ × ℕ))
8	3, 7	wcel 2209	. . . 4 wff 𝑥 ∈ ( ≤ ∩ (ℕ × ℕ))
9		vf	. . . . . . 7 setvar 𝑓
10	9	cv 1401	. . . . . 6 class 𝑓
11		c0 3520	. . . . . . 7 class ∅
12	11	csn 3705	. . . . . 6 class {∅}
13	10, 12	cdif 3217	. . . . 5 class (𝑓 ∖ {∅})
14	13	wfun 5366	. . . 4 wff Fun (𝑓 ∖ {∅})
15	10	cdm 4769	. . . . 5 class dom 𝑓
16		cfz 10390	. . . . . 6 class ...
17	3, 16	cfv 5372	. . . . 5 class (...‘𝑥)
18	15, 17	wss 3220	. . . 4 wff dom 𝑓 ⊆ (...‘𝑥)
19	8, 14, 18	w3a 1009	. . 3 wff (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))
20	19, 9, 2	copab 4186	. 2 class {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
21	1, 20	wceq 1402	1 wff Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}

This definition is referenced by:  brstruct  13339  isstruct2im  13340  isstruct2r  13341