:: MSSUBFAM semantic presentation

I is set

dom (doms M) is set
dom M is set

dom (rngs M) is set
dom M is set
I is set

dom (doms M) is set
dom M is set

dom (rngs M) is set
dom M is set

F1() is set
F2() is Relation-like F1() -defined Function-like total set
F3() is Relation-like F1() -defined Function-like total set
I is set
F3() . I is set
F2() . I is set
M is non empty set
SF is set
[:(F2() . I),M:] is Relation-like set
bool [:(F2() . I),M:] is set
SF is Relation-like F2() . I -defined M -valued Function-like total quasi_total Element of bool [:(F2() . I),M:]
[:(F2() . I),(F3() . I):] is Relation-like set
bool [:(F2() . I),(F3() . I):] is set
i is Relation-like F2() . I -defined F3() . I -valued Function-like quasi_total Element of bool [:(F2() . I),(F3() . I):]
B is set
ab is set
F3() . I is set
M is set
SF is set
F2() . I is set
[:(F2() . I),(F3() . I):] is Relation-like set
bool [:(F2() . I),(F3() . I):] is set
M is Relation-like F2() . I -defined F3() . I -valued Function-like quasi_total Element of bool [:(F2() . I),(F3() . I):]
SF is set
i is set
B is set
M . B is set
F3() . I is set

M is set
I . M is set
F2() . M is set
F3() . M is set
[:(F2() . M),(F3() . M):] is Relation-like set
bool [:(F2() . M),(F3() . M):] is set
SF is Relation-like F2() . M -defined F3() . M -valued Function-like quasi_total Element of bool [:(F2() . M),(F3() . M):]
M is Relation-like F1() -defined Function-like total Function-yielding V25() ManySortedFunction of F2(),F3()
SF is set
F2() . SF is set
F3() . SF is set
[:(F2() . SF),(F3() . SF):] is Relation-like set
bool [:(F2() . SF),(F3() . SF):] is set

I is set
bool I is set
bool (bool I) is set
M is Element of bool (bool I)
Intersect M is Element of bool I
union M is Element of bool I
meet M is Element of bool I
I is set
bool I is set
bool (bool I) is set
M is set
SF is Element of bool (bool I)
Intersect SF is Element of bool I
meet SF is Element of bool I
I is set
bool I is set
bool (bool I) is set
M is Element of bool (bool I)
Intersect M is Element of bool I
meet M is Element of bool I
I is set
bool I is set
bool (bool I) is set
M is Element of bool (bool I)
Intersect M is Element of bool I
SF is Element of bool I
meet M is Element of bool I
I is set
bool I is set
bool (bool I) is set
M is set
SF is Element of bool (bool I)
Intersect SF is Element of bool I
meet SF is Element of bool I
I is set
bool I is set
bool (bool I) is set
M is set
SF is set
i is Element of bool (bool I)
Intersect i is Element of bool I
meet i is Element of bool I
I is set
bool I is set
bool (bool I) is set
M is set
SF is set
i is Element of bool (bool I)
Intersect i is Element of bool I
meet i is Element of bool I
I is set
bool I is set
bool (bool I) is set
M is Element of bool (bool I)
Intersect M is Element of bool I
SF is Element of bool (bool I)
Intersect SF is Element of bool I
i is Element of bool (bool I)
SF \/ i is Element of bool (bool I)
Intersect i is Element of bool I
() /\ () is Element of bool I
meet SF is Element of bool I
(meet SF) /\ I is Element of bool I
() /\ I is Element of bool I
meet i is Element of bool I
I /\ (meet i) is Element of bool I
I /\ () is Element of bool I
meet i is Element of bool I
meet M is Element of bool I
meet SF is Element of bool I
I is set
bool I is set
bool (bool I) is set
M is Element of bool (bool I)
Intersect M is Element of bool I
SF is Element of bool I
{SF} is non empty finite set
meet M is Element of bool I
I is set
bool I is set
bool (bool I) is set
M is Element of bool (bool I)
Intersect M is Element of bool I
SF is Element of bool I
i is Element of bool I
{SF,i} is non empty finite set
SF /\ i is Element of bool I
meet M is Element of bool I
I is set

i is set
M . i is set
SF . i is set
I is set

i is set
M . i is set
SF . i is set
I is set
M is set

(rngs SF) . I is set
dom SF is set

rng i is set
I is set
M is set

(doms SF) . I is set
dom SF is set

dom i is set
I is set

dom (SF ** M) is set
dom M is set
dom SF is set
(dom M) /\ (dom SF) is set
I /\ (dom SF) is set
I /\ I is set
I is set

is non empty functional finite V39() set

bool [:I,:] is set

i is set
M . i is set

[:(M . i),(() . i):] is Relation-like set
bool [:(M . i),(() . i):] is set

I is set

B is set
M . B is set
SF . B is set
[:(M . B),(SF . B):] is Relation-like set
bool [:(M . B),(SF . B):] is set

(doms i) . B is set
ab is Relation-like M . B -defined SF . B -valued Function-like quasi_total Element of bool [:(M . B),(SF . B):]
dom ab is set
B is set
(rngs i) . B is set
SF . B is set
M . B is set
[:(M . B),(SF . B):] is Relation-like set
bool [:(M . B),(SF . B):] is set

ab is Relation-like M . B -defined SF . B -valued Function-like quasi_total Element of bool [:(M . B),(SF . B):]
rng ab is set
I is set

SF is set
M . SF is set

I is set

is non empty functional finite V39() set

bool [:I,:] is set
I is set

bool [:I,:] is set

I is set

i is set
M . i is set
SF . i is set
I is set

I is set

i is set
(M \/ SF) . i is set
M . i is finite set
SF . i is finite set
(M . i) \/ (SF . i) is finite set
I is set

i is set
(M /\ SF) . i is set
M . i is set
SF . i is finite set
(M . i) /\ (SF . i) is finite set
I is set

I is set

i is set
(SF \ M) . i is set
SF . i is finite set
M . i is set
(SF . i) \ (M . i) is finite Element of bool (SF . i)
bool (SF . i) is finite V39() set
I is set

i is set
(M .:.: SF) . i is set

SF . i is finite set
B .: (SF . i) is finite set
I is set

i is set
[|M,SF|] . i is set
M . i is finite set
SF . i is finite set
[:(M . i),(SF . i):] is Relation-like finite set
I is set

i is set
SF . i is set
[|SF,M|] . i is set
M . i is set
[:(SF . i),(M . i):] is Relation-like set
I is set

i is set
SF . i is set
[|M,SF|] . i is set
M . i is set
[:(M . i),(SF . i):] is Relation-like set
I is set

SF is set
(bool M) . SF is set
M . SF is set
bool (M . SF) is Element of bool (bool (M . SF))
bool (M . SF) is set
bool (bool (M . SF)) is set
SF is set
M . SF is set
(bool M) . SF is set
bool (M . SF) is Element of bool (bool (M . SF))
bool (M . SF) is set
bool (bool (M . SF)) is set
I is set

I is set

SF is set
() . SF is set
M . SF is set

B is set

{SF} is non empty finite set

{B} is non empty finite set

bool [:{SF},{B}:] is finite V39() set
i +* (SF .--> B) is Relation-like Function-like set
dom (i +* (SF .--> B)) is set
dom (SF .--> B) is finite set

ab . SF is set
(SF .--> B) . SF is set
Q is set
ab . Q is set
M . Q is set
i . Q is set
union (M . SF) is set
I is set

SF is set
M . SF is set
() . SF is set
union (M . SF) is set

i is set
SF . i is set
() . i is set
M . i is set
union (M . i) is set
I is set

SF is set
(rngs M) . SF is set

(doms M) . SF is set

dom i is set
rng i is set
I is set

i is set
M . i is set

(rngs SF) . i is set

rng B is set
B " (M . i) is set
I is set

i is set
((Funcs) (M,SF)) . i is set
M . i is finite set
SF . i is finite set
Funcs ((M . i),(SF . i)) is functional set
I is set

(M \ SF) \/ (SF \ M) is Relation-like I -defined Function-like total finite-yielding set
I is set

B is set
SF . B is set
i . B is set
M . B is set
[|SF,i|] . B is set
[:(SF . B),(i . B):] is Relation-like set

ab is set
B . ab is set
SF . ab is set
i . ab is set
M . ab is set

Q is set
B . Q is set
Q is set
B . Q is set
SF . Q is set
Q is set
ab . Q is set
Q is set
ab . Q is set
i . Q is set
Q is set
M . Q is set
[|B,ab|] . Q is set
B . Q is set
ab . Q is set
[:(B . Q),(ab . Q):] is Relation-like set
I is set

B is set
SF . B is set
M . B is set
i . B is set
[|SF,i|] . B is set
[:(SF . B),(i . B):] is Relation-like set
ab is set
[:ab,(i . B):] is Relation-like set

ab is set
B . ab is set
ab is set
B . ab is set
SF . ab is set
ab is set
M . ab is set
[|B,i|] . ab is set
B . ab is set
i . ab is set
[:(B . ab),(i . ab):] is Relation-like set
I is set

SF is set
M . SF is finite set

ab is set
Q is set

{SF} is non empty finite set

{ab} is non empty finite set

bool [:{SF},{ab}:] is finite V39() set
dom (SF .--> ab) is finite set

{Q} is non empty finite set

bool [:{SF},{Q}:] is finite V39() set
i +* (SF .--> Q) is Relation-like Function-like set
dom (i +* (SF .--> Q)) is set
dom (SF .--> Q) is finite set

K . SF is set
(SF .--> Q) . SF is set
q is set
K . q is set
M . q is finite set
i . q is set
B +* (SF .--> ab) is Relation-like Function-like set
dom (B +* (SF .--> ab)) is set

qb . SF is set
(SF .--> ab) . SF is set
j is set
qb . j is set
M . j is finite set
B . j is set
i is set
B is set

i is set
SF . i is set
M . i is finite set

B is set
SF . B is set
i . B is set
M . B is finite set
I is set

SF is set
M . SF is finite set

ab is set
Q is set

{SF} is non empty finite set

{ab} is non empty finite set

bool [:{SF},{ab}:] is finite V39() set
dom (SF .--> ab) is finite set

{Q} is non empty finite set

bool [:{SF},{Q}:] is finite V39() set
i +* (SF .--> Q) is Relation-like Function-like set
dom (i +* (SF .--> Q)) is set
dom (SF .--> Q) is finite set

K . SF is set
(SF .--> Q) . SF is set
q is set
K . q is set
M . q is finite set
i . q is set
B +* (SF .--> ab) is Relation-like Function-like set
dom (B +* (SF .--> ab)) is set

qb . SF is set
(SF .--> ab) . SF is set
j is set
qb . j is set
M . j is finite set
B . j is set
i is set
B is set

i is set
SF . i is set
M . i is finite set

B is set
i . B is set
SF . B is set
M . B is finite set
I is set

i is set

(doms M) . i is set
SF . i is set

rng B is set
(rngs M) . i is set
dom B is set
ab is set
B .: ab is set

B is set
i . B is set
(doms M) . B is set

SF . B is set

ab .: (i . B) is set
B is set
i . B is set

(doms M) . B is set
SF . B is set

ab .: (i . B) is set
B is set

i . B is set
(doms M) . B is set
SF . B is set
(M .:.: i) . B is set

ab .: (i . B) is set
I is set
I is set

I is set

I is set

bool [:I,:] is set

I is set

bool [:I,:] is set

I is set

I is non empty set

i is Element of I
SF . i is set
M . i is set
bool (M . i) is set
bool (bool (M . i)) is set

(I,M) . i is non empty set
I is set
M is set

SF . I is set
bool (SF . I) is set
bool (bool (SF . I)) is set

i . I is set

(M,SF) . I is set
I is set

I is set

I is set

(I,M) /\ (I,M) is Relation-like I -defined Function-like total set
I is set

I is set

(SF \ i) \/ (i \ SF) is Relation-like I -defined Function-like total set
I is set

I is set

I is set

i is set
bool i is set
bool (bool i) is set
B is Element of bool (bool i)
union B is Element of bool i
i is set
(union SF) . i is set
M . i is set
SF . i is set
bool (M . i) is set
bool (bool (M . i)) is set
union (SF . i) is set
I is set

i is set
M . i is set
bool (M . i) is set
bool (bool (M . i)) is set
SF . i is set
B is Element of bool (bool (M . i))
Intersect B is Element of bool (M . i)

{()} is non empty finite set
[:I,{()}:] is Relation-like set
bool [:I,{()}:] is set

ab . i is set

ab is set
M . ab is set
bool (M . ab) is set
bool (bool (M . ab)) is set
SF . ab is set
i . ab is set
B . ab is set
Q is Element of bool (bool (M . ab))
Intersect Q is Element of bool (M . ab)
B9 is Element of bool (bool (M . ab))
Intersect B9 is Element of bool (M . ab)
I is set

(I,M,SF) is Relation-like I -defined Function-like total set
i is set
(I,M,SF) . i is set
M . i is set
bool (M . i) is set
bool (bool (M . i)) is set
SF . i is set
B is Element of bool (bool (M . i))
Intersect B is Element of bool (M . i)
I is set

bool [:I,:] is set

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M
i is set
M . i is set
bool (M . i) is set
bool (bool (M . i)) is set
SF . i is set
(I,M,SF) . i is set
B is Element of bool (bool (M . i))
Intersect B is Element of bool (M . i)
I is set

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

i is set
(I,M,SF) . i is set
(union SF) . i is set
M . i is set
bool (M . i) is set
bool (bool (M . i)) is set
SF . i is set
B is Element of bool (bool (M . i))
Intersect B is Element of bool (M . i)
meet B is Element of bool (M . i)
union B is Element of bool (M . i)
I is set

(I,M,i) is Relation-like I -defined Function-like total ManySortedSubset of M
B is set
(I,M,i) . B is set
SF . B is set
M . B is set
bool (M . B) is set
bool (bool (M . B)) is set
i . B is set
ab is Element of bool (bool (M . B))
Intersect ab is Element of bool (M . B)
meet ab is Element of bool (M . B)
I is set

bool [:I,:] is set

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M
i is set
M . i is set
bool (M . i) is set
bool (bool (M . i)) is set
SF . i is set
(I,M,SF) . i is set
B is Element of bool (bool (M . i))
Intersect B is Element of bool (M . i)

meet B is Element of bool (M . i)
I is set

(I,SF,i) is Relation-like I -defined Function-like total ManySortedSubset of SF
B is set
M . B is set
(I,SF,i) . B is set

SF . B is set
bool (SF . B) is set
bool (bool (SF . B)) is set
i . B is set
Q is Element of bool (bool (SF . B))
Intersect Q is Element of bool (SF . B)
B9 is set

{B} is non empty finite set

{B9} is non empty finite set

bool [:{B},{B9}:] is finite V39() set
ab +* (B .--> B9) is Relation-like Function-like set
dom (ab +* (B .--> B9)) is set
dom (B .--> B9) is finite set

K . B is set
(B .--> B9) . B is set
q is set
K . q is set
i . q is set
ab . q is set
meet Q is Element of bool (SF . B)
I is set

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

(I,M,i) is Relation-like I -defined Function-like total ManySortedSubset of M
B is set
(I,M,i) . B is set
(I,M,SF) . B is set
M . B is set
bool (M . B) is set
bool (bool (M . B)) is set
SF . B is set
ab is Element of bool (bool (M . B))
Intersect ab is Element of bool (M . B)
i . B is set
Q is Element of bool (bool (M . B))
Intersect Q is Element of bool (M . B)
I is set

(I,M,B) is Relation-like I -defined Function-like total ManySortedSubset of M
ab is set
(I,M,B) . ab is set
i . ab is set
SF . ab is set
M . ab is set
bool (M . ab) is set
bool (bool (M . ab)) is set
B . ab is set
Q is Element of bool (bool (M . ab))
Intersect Q is Element of bool (M . ab)
meet Q is Element of bool (M . ab)
I is set

bool [:I,:] is set

(I,M,B) is Relation-like I -defined Function-like total ManySortedSubset of M
(I,M,B) /\ i is Relation-like I -defined Function-like total set
ab is set
M . ab is set
bool (M . ab) is set
bool (bool (M . ab)) is set
B . ab is set
(I,M,B) . ab is set
Q is Element of bool (bool (M . ab))
Intersect Q is Element of bool (M . ab)
SF . ab is set
i . ab is set
(SF . ab) /\ (i . ab) is set

meet Q is Element of bool (M . ab)
(meet Q) /\ (i . ab) is Element of bool (M . ab)
((I,M,B) /\ i) . ab is set
I is set

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

(I,M,i) is Relation-like I -defined Function-like total ManySortedSubset of M

(I,M,B) is Relation-like I -defined Function-like total ManySortedSubset of M
(I,M,i) /\ (I,M,B) is Relation-like I -defined Function-like total set
ab is set
M . ab is set
bool (M . ab) is set
bool (bool (M . ab)) is set
i . ab is set
(I,M,i) . ab is set
Q is Element of bool (bool (M . ab))
Intersect Q is Element of bool (M . ab)
SF . ab is set
(I,M,SF) . ab is set
B9 is Element of bool (bool (M . ab))
Intersect B9 is Element of bool (M . ab)
B . ab is set
(I,M,B) . ab is set
K is Element of bool (bool (M . ab))
Intersect K is Element of bool (M . ab)
Q \/ K is Element of bool (bool (M . ab))
meet B9 is Element of bool (M . ab)
meet Q is Element of bool (M . ab)
meet K is Element of bool (M . ab)
(meet Q) /\ (meet K) is Element of bool (M . ab)
((I,M,i) . ab) /\ (meet K) is Element of bool (M . ab)
((I,M,i) . ab) /\ ((I,M,B) . ab) is set
((I,M,i) /\ (I,M,B)) . ab is set
((I,M,i) . ab) /\ (M . ab) is set
((I,M,i) . ab) /\ ((I,M,B) . ab) is set
((I,M,i) /\ (I,M,B)) . ab is set
(M . ab) /\ ((I,M,B) . ab) is set
((I,M,i) . ab) /\ ((I,M,B) . ab) is set
((I,M,i) /\ (I,M,B)) . ab is set
() /\ () is Element of bool (M . ab)
((I,M,i) /\ (I,M,B)) . ab is set
((I,M,i) /\ (I,M,B)) . ab is set
((I,M,i) /\ (I,M,B)) . ab is set
I is set

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

B is set
M . B is set
bool (M . B) is set
bool (bool (M . B)) is set
SF . B is set
(I,M,SF) . B is set
ab is Element of bool (bool (M . B))
Intersect ab is Element of bool (M . B)
meet ab is Element of bool (M . B)
i . B is set
{(i . B)} is non empty finite set
meet {(i . B)} is set
I is set

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

ab is set
M . ab is set
bool (M . ab) is set
bool (bool (M . ab)) is set
SF . ab is set
(I,M,SF) . ab is set
{i,B} . ab is finite set
meet ({i,B} . ab) is set
i . ab is set
B . ab is set
{(i . ab),(B . ab)} is non empty finite set
meet {(i . ab),(B . ab)} is set
(i . ab) /\ (B . ab) is set
(i /\ B) . ab is set
Q is Element of bool (bool (M . ab))
Intersect Q is Element of bool (M . ab)
I is set

(I,M,i) is Relation-like I -defined Function-like total ManySortedSubset of M

ab is set
SF . ab is set
B . ab is set
(I,M,i) . ab is set
i . ab is set
M . ab is set
bool (M . ab) is set
bool (bool (M . ab)) is set
Q is Element of bool (bool (M . ab))
Intersect Q is Element of bool (M . ab)
I is set

(I,SF,i) is Relation-like I -defined Function-like total ManySortedSubset of SF
B is set
M . B is set
(I,SF,i) . B is set

SF . B is set
bool (SF . B) is set
bool (bool (SF . B)) is set
i . B is set
Q is Element of bool (bool (SF . B))
Intersect Q is Element of bool (SF . B)
B9 is set

{B} is non empty finite set

{B9} is non empty finite set

bool [:{B},{B9}:] is finite V39() set
ab +* (B .--> B9) is Relation-like Function-like set
dom (ab +* (B .--> B9)) is set
dom (B .--> B9) is finite set

K . B is set
(B .--> B9) . B is set
q is set
K . q is set
i . q is set
ab . q is set
I is set

I is set

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M

bool [:I,:] is set
I is set

I is set

I is set

I is set

(I,M,ab) is Relation-like I -defined Function-like total ManySortedSubset of M
I is set

bool [:I,:] is set
(I,M) is Relation-like non-empty I -defined Function-like total (I,M) (I,M) (I,M) (I,M) (I,M) (I,M) ManySortedSubset of bool M

(I,M,SF) is Relation-like I -defined Function-like total ManySortedSubset of M
I is set

i is set
SF . i is set
I is set

bool [:I,:] is set
(I,M) is Relation-like non-empty I -defined Function-like total (I,M) (I,M) (I,M) (I,M) (I,M) (I,M) ManySortedSubset of bool M

I is set

bool [:I,:] is set
i is set
SF . i is set