MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-struct Structured version   Visualization version   GIF version

Definition df-struct 15906
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 5944, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 15916: 𝐹 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 4456). This is used critically in strle1 16020, strle2 16021, strle3 16022 and strleun 16019 to avoid sethood hypotheses on the "payload" sets: without this, ipsstr 16071 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 16072, 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 19806. (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
StepHypRef Expression
1 cstr 15900 . 2 class Struct
2 vx . . . . . 6 setvar 𝑥
32cv 1522 . . . . 5 class 𝑥
4 cle 10113 . . . . . 6 class
5 cn 11058 . . . . . . 7 class
65, 5cxp 5141 . . . . . 6 class (ℕ × ℕ)
74, 6cin 3606 . . . . 5 class ( ≤ ∩ (ℕ × ℕ))
83, 7wcel 2030 . . . 4 wff 𝑥 ∈ ( ≤ ∩ (ℕ × ℕ))
9 vf . . . . . . 7 setvar 𝑓
109cv 1522 . . . . . 6 class 𝑓
11 c0 3948 . . . . . . 7 class
1211csn 4210 . . . . . 6 class {∅}
1310, 12cdif 3604 . . . . 5 class (𝑓 ∖ {∅})
1413wfun 5920 . . . 4 wff Fun (𝑓 ∖ {∅})
1510cdm 5143 . . . . 5 class dom 𝑓
16 cfz 12364 . . . . . 6 class ...
173, 16cfv 5926 . . . . 5 class (...‘𝑥)
1815, 17wss 3607 . . . 4 wff dom 𝑓 ⊆ (...‘𝑥)
198, 14, 18w3a 1054 . . 3 wff (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))
2019, 9, 2copab 4745 . 2 class {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
211, 20wceq 1523 1 wff Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
Colors of variables: wff setvar class
This definition is referenced by:  brstruct  15913  isstruct2  15914
  Copyright terms: Public domain W3C validator