Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-struct GIF version

Definition df-struct 11661
 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 5067, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 11672: 𝐹 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 3665). (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 11655 . 2 class Struct
2 vx . . . . . 6 setvar 𝑥
32cv 1295 . . . . 5 class 𝑥
4 cle 7620 . . . . . 6 class
5 cn 8520 . . . . . . 7 class
65, 5cxp 4465 . . . . . 6 class (ℕ × ℕ)
74, 6cin 3012 . . . . 5 class ( ≤ ∩ (ℕ × ℕ))
83, 7wcel 1445 . . . 4 wff 𝑥 ∈ ( ≤ ∩ (ℕ × ℕ))
9 vf . . . . . . 7 setvar 𝑓
109cv 1295 . . . . . 6 class 𝑓
11 c0 3302 . . . . . . 7 class
1211csn 3466 . . . . . 6 class {∅}
1310, 12cdif 3010 . . . . 5 class (𝑓 ∖ {∅})
1413wfun 5043 . . . 4 wff Fun (𝑓 ∖ {∅})
1510cdm 4467 . . . . 5 class dom 𝑓
16 cfz 9573 . . . . . 6 class ...
173, 16cfv 5049 . . . . 5 class (...‘𝑥)
1815, 17wss 3013 . . . 4 wff dom 𝑓 ⊆ (...‘𝑥)
198, 14, 18w3a 927 . . 3 wff (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))
2019, 9, 2copab 3920 . 2 class {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
211, 20wceq 1296 1 wff Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
 Colors of variables: wff set class This definition is referenced by:  brstruct  11668  isstruct2im  11669  isstruct2r  11670
 Copyright terms: Public domain W3C validator