Certain Facts about Families of Subsets of Many Sorted Sets
Artur Korni · 1996
For simplicity we follow the rules: I, G, H will denote sets, i will be arbitrary, A, B, M will denote many sorted sets indexed by I, s1, s2, s3 will denote families of subsets of I, v, w will denote subsets of I, and F will denote a many sorted function of I. The scheme MSFExFunc deals with a set A, a many sorted set B indexed by A, a many sorted set C indexed by A, and a ternary predicate P, and states that: There exists a many sorted function F from B into C such that for arbitrary i if i ∈ A, then there exists a function f from B(i) into C(i) such that f = F (i) and for arbitrary x such that x ∈ B(i) holds P[f(x), x, i] provided the following condition is satisfied: • Let i be arbitrary. Suppose i ∈ A. Let x be arbitrary. If x ∈ B(i), then there exists arbitrary y such that y ∈ C(i) and P[y, x, i]. We now state a number of propositions: (1) If s1 6= ∅, then Intersect(s1) ⊆ ⋃ s1. (2) If G ∈ s1, then Intersect(s1) ⊆ G. (3) If ∅ ∈ s1, then Intersect(s1) = ∅.