:: FINSET_1 semantic presentation

omega is non empty epsilon-transitive epsilon-connected ordinal set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

1 is non empty epsilon-transitive epsilon-connected ordinal natural Element of omega

{{},1} is non empty set

bool {} is non empty set

{{}} is non empty functional set

union {} is epsilon-transitive epsilon-connected ordinal set

F is set

{F} is non empty set

{{}} --> F is non empty Relation-like {{}} -defined {F} -valued Function-like constant V17({{}}) V18({{}},{F}) Element of bool [:{{}},{F}:]

[:{{}},{F}:] is non empty Relation-like set

bool [:{{}},{F}:] is non empty set

dom ({{}} --> F) is non empty functional Element of bool {{}}

bool {{}} is non empty set

proj2 ({{}} --> F) is non empty trivial set

proj1 ({{}} --> F) is non empty set

x is set

({{}} --> F) . {} is set

b is set

({{}} --> F) . b is set

rng ({{}} --> F) is non empty trivial Element of bool {F}

bool {F} is non empty set

the set is set

{ the set } is non empty set

F is set

proj2 {} is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural with_non-empty_elements set

proj1 {} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

F

F is Relation-like Function-like set

proj1 F is set

e is epsilon-transitive epsilon-connected ordinal set

F . e is set

F

F

F is set

e is set

F \/ e is set

x is Relation-like Function-like set

proj2 x is set

proj1 x is set

b is Relation-like Function-like set

proj2 b is set

proj1 b is set

c

a is epsilon-transitive epsilon-connected ordinal set

c

x is Relation-like Function-like set

proj1 x is set

proj2 x is set

y is set

z is set

x . z is set

Z is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal natural set

x . Z is set

Z is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal natural set

Z -^ y is epsilon-transitive epsilon-connected ordinal set

b . (Z -^ y) is set

y +^ (Z -^ y) is epsilon-transitive epsilon-connected ordinal set

Z is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal natural set

y is set

z is set

x . z is set

x . z is set

z is epsilon-transitive epsilon-connected ordinal natural set

z is set

b . z is set

y is epsilon-transitive epsilon-connected ordinal natural set

Z is epsilon-transitive epsilon-connected ordinal set

y +^ Z is epsilon-transitive epsilon-connected ordinal set

(y +^ Z) -^ y is epsilon-transitive epsilon-connected ordinal set

b . ((y +^ Z) -^ y) is set

x . (y +^ Z) is set

y is epsilon-transitive epsilon-connected ordinal natural set

z is epsilon-transitive epsilon-connected ordinal natural set

y +^ z is epsilon-transitive epsilon-connected ordinal natural set

F is set

{F} is non empty set

F is set

e is set

{F,e} is non empty set

{F} is non empty () set

{e} is non empty () set

{F} \/ {e} is non empty set

F is set

e is set

x is set

{F,e,x} is non empty set

{F} is non empty () set

{e,x} is non empty () set

{F} \/ {e,x} is non empty set

F is set

e is set

x is set

b is set

{F,e,x,b} is non empty set

{F} is non empty () set

{e,x,b} is non empty () set

{F} \/ {e,x,b} is non empty set

F is set

e is set

x is set

b is set

c

{F,e,x,b,c

{F} is non empty () set

{e,x,b,c

{F} \/ {e,x,b,c

F is set

e is set

x is set

b is set

c

a is set

{F,e,x,b,c

{F} is non empty () set

{e,x,b,c

{F} \/ {e,x,b,c

F is set

e is set

x is set

b is set

c

a is set

x is set

{F,e,x,b,c

{F} is non empty () set

{e,x,b,c

{F} \/ {e,x,b,c

F is set

e is set

x is set

b is set

c

a is set

x is set

y is set

{F,e,x,b,c

{F} is non empty () set

{e,x,b,c

{F} \/ {e,x,b,c

F is () set

bool F is non empty set

e is Element of bool F

x is set

b is Relation-like Function-like set

proj2 b is set

proj1 b is set

c

proj1 c

a is set

x is set

b . x is set

c

x is set

c

b . x is set

b . x is set

b . x is set

proj2 c

F is () set

e is () set

F \/ e is set

F is set

e is set

F is set

e is set

F \/ e is set

F is set

e is () set

F /\ e is set

F is () set

e is set

F /\ e is () set

F \ e is () Element of bool F

bool F is non empty set

F is set

e is set

F /\ e is set

F is set

e is set

F \ e is Element of bool F

bool F is non empty set

F is Relation-like Function-like set

e is () set

F .: e is set

proj1 F is set

(proj1 F) /\ e is () set

b is Relation-like Function-like set

proj2 b is set

proj1 b is set

b * F is Relation-like Function-like set

proj2 (b * F) is set

proj1 (b * F) is set

F .: ((proj1 F) /\ e) is set

F is set

e is Relation-like Function-like set

e .: F is set

F is set

bool F is non empty set

bool (bool F) is non empty set

e is Element of bool (bool F)

x is Relation-like Function-like set

proj2 x is set

proj1 x is set

bool (proj1 x) is non empty Element of bool (bool (proj1 x))

bool (proj1 x) is non empty set

bool (bool (proj1 x)) is non empty set

b is set

c

the Element of e is Element of e

x " the Element of e is set

x .: (x " the Element of e) is set

c

bool (bool {}) is non empty set

x is Element of bool (bool {})

y is set

x is epsilon-transitive epsilon-connected ordinal set

bool x is non empty set

bool (bool x) is non empty set

succ x is non empty epsilon-transitive epsilon-connected ordinal set

bool (succ x) is non empty set

bool (bool (succ x)) is non empty set

y is Element of bool (bool (succ x))

{x} is non empty () set

bool x is non empty Element of bool (bool x)

z is set

y is set

the Element of y is Element of y

x \/ {x} is non empty set

the Element of y \ {x} is Element of bool the Element of y

bool the Element of y is non empty set

(x \/ {x}) \ {x} is Element of bool (x \/ {x})

bool (x \/ {x}) is non empty set

x \ {x} is Element of bool x

y is Element of bool (bool x)

Z is set

X1 is set

X1 \ {x} is Element of bool X1

bool X1 is non empty set

Z \/ {x} is non empty set

A is non empty set

B is set

B \ {x} is Element of bool B

bool B is non empty set

(B \ {x}) \/ {x} is non empty set

A \ {x} is Element of bool A

bool A is non empty set

Z \ {x} is Element of bool Z

bool Z is non empty set

X1 \/ {x} is non empty set

A is set

B is set

B \ {x} is Element of bool B

bool B is non empty set

A \ {x} is Element of bool A

bool A is non empty set

A \/ {x} is non empty set

(B \ {x}) \/ {x} is non empty set

B \/ {x} is non empty set

x is set

B is set

c

x is epsilon-transitive epsilon-connected ordinal set

bool x is non empty set

bool (bool x) is non empty set

y is Element of bool (bool x)

x is set

x .: x is set

y is set

x " (x .: x) is set

x " y is set

x .: (x " y) is set

y is set

F

bool F

bool F

bool (bool F

F is set

e is set

e is Element of bool (bool F

x is set

F

the Element of F

{ the Element of F

x \/ { the Element of F

c

b is set

F is set

union F is set

bool F is non empty Element of bool (bool F)

bool F is non empty set

bool (bool F) is non empty set

e is set

x is set

b is set

{x} is non empty () set

b \/ {x} is non empty set

union (b \/ {x}) is set

union b is set

union {x} is set

(union b) \/ (union {x}) is set

(union b) \/ x is set

c

union c

x is set

union x is set

F is () set

e is () set

[:F,e:] is Relation-like set

x is set

{x} is non empty () set

[:F,{x}:] is Relation-like set

b is Relation-like Function-like set

proj1 b is set

proj2 b is set

c

a is set

b . a is set

[a,x] is V1() set

{a,x} is non empty () set

{a} is non empty () set

{{a,x},{a}} is non empty () set

a is set

x is set

[a,x] is V1() set

{a,x} is non empty () set

{a} is non empty () set

{{a,x},{a}} is non empty () set

b . a is set

b .: F is () set

bool [:F,e:] is non empty Element of bool (bool [:F,e:])

bool [:F,e:] is non empty set

bool (bool [:F,e:]) is non empty set

x is set

union x is set

b is set

c

c

a is set

[c

{c

{c

{{c

{a} is non empty () set

[:F,{a}:] is Relation-like set

b is Relation-like Function-like set

proj1 b is set

proj2 b is set

c

a is set

b . a is set

{a} is non empty () set

[:F,{a}:] is Relation-like set

a is set

{a} is non empty () set

[:F,{a}:] is Relation-like set

b . a is set

b .: e is () set

c

a is set

{a} is non empty () set

[:F,{a}:] is Relation-like set

F is () set

e is () set

x is () set

[:F,e,x:] is set

[:F,e:] is Relation-like () set

[:[:F,e:],x:] is Relation-like () set

F is () set

e is () set

x is () set

b is () set

[:F,e,x,b:] is set

[:F,e,x:] is () set

[:[:F,e,x:],b:] is Relation-like () set

F is () set

bool F is non empty Element of bool (bool F)

bool F is non empty set

bool (bool F) is non empty set

e is set

bool {} is non empty Element of bool (bool {})

bool (bool {}) is non empty set

x is set

b is set

{x} is non empty () set

b \/ {x} is non empty set

bool b is non empty Element of bool (bool b)

bool b is non empty set

bool (bool b) is non empty set

c

y is set

a is set

y \/ {x} is non empty set

z is set

x is set

z \/ {x} is non empty set

c

c

a is set

a \/ {x} is non empty set

c

proj1 c

proj2 c

bool (b \/ {x}) is non empty set

bool (b \/ {x}) is non empty Element of bool (bool (b \/ {x}))

bool (bool (b \/ {x})) is non empty set

(bool (b \/ {x})) \ (bool b) is Element of bool (bool (b \/ {x}))

a is set

x is set

c

y is set

y \/ {x} is non empty set

a \ {x} is Element of bool a

bool a is non empty set

y is set

c

y is set

y \/ {x} is non empty set

a \/ {x} is non empty set

c

((bool (b \/ {x})) \ (bool b)) \/ (bool b) is non empty set

(bool (b \/ {x})) \/ (bool b) is non empty set

F is set

union F is set

bool (union F) is non empty Element of bool (bool (union F))

bool (union F) is non empty set

bool (bool (union F)) is non empty set

e is set

F is Relation-like Function-like set

proj1 F is set

proj2 F is set

F .: (proj1 F) is set

F is set

e is Relation-like Function-like set

proj2 e is set

e " F is set

e .: (e " F) is set

F is () set

e is () set

F \+\ e is set

F \ e is () set

e \ F is () set

(F \ e) \/ (e \ F) is () set

F is non empty set

bool F is non empty set

the Element of F is Element of F

{ the Element of F} is non empty () Element of bool F

F is Relation-like Function-like set

proj1 F is set

proj2 F is set

[:(proj1 F),(proj2 F):] is Relation-like set

proj2 F is set

[:(proj1 F),(proj2 F):] is Relation-like set

pr1 ((proj1 F),(proj2 F)) is Relation-like [:(proj1 F),(proj2 F):] -defined proj1 F -valued Function-like V18([:(proj1 F),(proj2 F):], proj1 F) Element of bool [:[:(proj1 F),(proj2 F):],(proj1 F):]

[:[:(proj1 F),(proj2 F):],(proj1 F):] is Relation-like set

bool [:[:(proj1 F),(proj2 F):],(proj1 F):] is non empty set

(pr1 ((proj1 F),(proj2 F))) .: F is Element of bool (proj1 F)

bool (proj1 F) is non empty set

F is set

e is set

x is set

{e} is non empty () set

x \/ {e} is non empty set

b is set

c

b is set

b is set

{e} is non empty () set

x \/ {e} is non empty set

c

c

a is set

x is set

b is set

{e} is non empty () set

x \/ {e} is non empty set

{e} is non empty () set

x \/ {e} is non empty set

b is set

e is set

F is set

e is set

x is set

{e} is non empty () set

x \/ {e} is non empty set

b is set

c

b is set

b is set

{e} is non empty () set

x \/ {e} is non empty set

c

c

a is set

x is set

b is set

{e} is non empty () set

x \/ {e} is non empty set

{e} is non empty () set

x \/ {e} is non empty set

b is set

e is set

F is set

e is set

x is set

[:e,x:] is Relation-like set

b is Relation-like Function-like set

proj1 b is set

c

proj1 c

proj2 b is set

a is set

proj2 c

x is set

[:a,x:] is Relation-like set

y is set

z is set

b . z is set

y is set

z is set

[y,z] is V1() set

{y,z} is non empty () set

{y} is non empty () set

{{y,z},{y}} is non empty () set

z `1 is set

y is set

z is set

c

y is set

z is set

[y,z] is V1() set

{y,z} is non empty () set

{y} is non empty () set

{{y,z},{y}} is non empty () set

z `2 is set

y is set

z is set

y is set

[z,y] is V1() set

{z,y} is non empty () set

{z} is non empty () set

{{z,y},{z}} is non empty () set

c

y `2 is set

b . y is set

y `1 is set

F is set

e is set

x is set

[:e,x:] is Relation-like set

b is Relation-like Function-like set

proj1 b is set

proj2 b is set

c

[:c

a is set

x is set

b . x is set

y is set

z is set

[y,z] is V1() set

{y,z} is non empty () set

{y} is non empty () set

{{y,z},{y}} is non empty () set

x `1 is set

a is set

x is set

y is set

[x,y] is V1() set

{x,y} is non empty () set

{x} is non empty () set

{{x,y},{x}} is non empty () set

b . a is set

a `1 is set

[{},{}] is V1() set

{{},{}} is non empty functional () set

{{{},{}},{{}}} is non empty () set

{[{},{}]} is non empty Relation-like Function-like () set

F is Relation-like () set

proj1 F is set

e is Relation-like Function-like set

proj1 e is set

x is set

proj2 e is set

b is set

e . b is set

b `2 is set

[x,(b `2)] is V1() set

{x,(b `2)} is non empty () set

{x} is non empty () set

{{x,(b `2)},{x}} is non empty () set

b `1 is set

c

a is set

[c

{c

{c

{{c

b is set

[x,b] is V1() set

{x,b} is non empty () set

{x} is non empty () set

{{x,b},{x}} is non empty () set

e . [x,b] is set

[x,b] `1 is set

e is Relation-like Function-like () set

F is Relation-like Function-like set

e * F is Relation-like Function-like set

proj1 (e * F) is set

proj1 e is () set

F is () set

e is set

[:F,e:] is Relation-like set

bool [:F,e:] is non empty set

x is Relation-like F -defined e -valued Function-like V18(F,e) Element of bool [:F,e:]

dom x is () Element of bool F

bool F is non empty () set

F is set

e is set

F .--> e is Relation-like {F} -defined Function-like one-to-one set

{F} is non empty () set

{F} --> e is non empty Relation-like {F} -defined {e} -valued Function-like constant V17({F}) V18({F},{e}) () Element of bool [:{F},{e}:]

{e} is non empty () set

[:{F},{e}:] is non empty Relation-like () set

bool [:{F},{e}:] is non empty () set

F is Relation-like () set

proj2 F is set

e is Relation-like Function-like set

proj1 e is set

x is set

proj2 e is set

b is set

e . b is set

b `1 is set

[(b `1),x] is V1() set

{(b `1),x} is non empty () set

{(b `1)} is non empty () set

{{(b `1),x},{(b `1)}} is non empty () set

b `2 is set

c

a is set

[c

{c

{c

{{c

b is set

[b,x] is V1() set

{b,x} is non empty () set

{b} is non empty () set

{{b,x},{b}} is non empty () set

e . [b,x] is set

[b,x] `2 is set

F is Relation-like Function-like () set

e is set

F " e is set

proj1 F is () set

F is Relation-like Function-like () set

e is Relation-like Function-like () set

F +* e is Relation-like Function-like set

proj1 (F +* e) is set

proj1 F is () set

proj1 e is () set

(proj1 F) \/ (proj1 e) is () set

F is Relation-like Function-like set

proj1 F is set

e is set

F . e is set

proj2 F is set

F . e is set

e is set

proj2 F is set

x is set

F . x is set

F is set

e is Relation-like F -defined Function-like set

x is set

dom e is Element of bool F

bool F is non empty set

e . x is set

dom e is Element of bool F

bool F is non empty set

e . x is set

dom e is Element of bool F

bool F is non empty set

x is set

proj1 e is set

e . x is set

dom e is Element of bool F

bool F is non empty set

F is set

e is set

[:e,F:] is Relation-like set

x is set

{x} is non empty () set

[x,{x}] is V1() set

{x,{x}} is non empty () set

{{x,{x}},{x}} is non empty () set

F is set

e is Relation-like F -defined Function-like set

F is set

e is set

F is non empty set

e is non empty set

the Element of F is Element of F

the Element of e is Element of e

{ the Element of F} is non empty () set

the Element of F .--> the Element of e is Relation-like F -defined { the Element of F} -defined e -valued Function-like one-to-one () set

{ the Element of F} --> the Element of e is non empty Relation-like { the Element of F} -defined e -valued { the Element of e} -valued Function-like constant V17({ the Element of F}) V18({ the Element of F},{ the Element of e}) () Element of bool [:{ the Element of F},{ the Element of e}:]

{ the Element of e} is non empty () set

[:{ the Element of F},{ the Element of e}:] is non empty Relation-like () set

bool [:{ the Element of F},{ the Element of e}:] is non empty () set

c

F is set

e is Relation-like () set

F |` e is Relation-like set

e is Relation-like () set

F is set

e | F is Relation-like set

e is Relation-like Function-like set

F is () set

e | F is Relation-like Function-like set

proj1 (e | F) is set

F is Relation-like () set

field F is set

proj1 F is () set

proj2 F is () set

(proj1 F) \/ (proj2 F) is () set

F is set

e is set

{e} is non empty () set

F is set

F is non trivial set

bool F is non empty set

e is set

x is set

{e,x} is non empty () set

b is Element of bool F

F is set

e is set

x is set

b is set

(F,e) --> (x,b) is set

F .--> x is Relation-like {F} -defined Function-like one-to-one () set

{F} is non empty () set

{F} --> x is non empty Relation-like {F} -defined {x} -valued Function-like constant V17({F}) V18({F},{x}) () Element of bool [:{F},{x}:]

{x} is non empty () set

[:{F},{x}:] is non empty Relation-like () set

bool [:{F},{x}:] is non empty () set

e .--> b is Relation-like {e} -defined Function-like one-to-one () set

{e} is non empty () set

{e} --> b is non empty Relation-like {e} -defined {b} -valued Function-like constant V17({e}) V18({e},{b}) () Element of bool [:{e},{b}:]

{b} is non empty () set

[:{e},{b}:] is non empty Relation-like () set

bool [:{e},{b}:] is non empty () set

(F .--> x) +* (e .--> b) is Relation-like Function-like () set

F is set

e is set

F is () set

e is Element of F

{{{}}} is non empty () set

F is non empty () set

e is set

F is () set

{F} is non empty () set

e is set

bool F is non empty () Element of bool (bool F)

bool F is non empty () set

bool (bool F) is non empty () set

e is set

e is () set

{F,e} is non empty () set

x is set

F is () set

bool F is non empty set

e is Element of bool F

x is set

e is () set

F \/ e is set

x is set

F is () () set

union F is set

e is set

{{{}}} is non empty () () set

{{}} .--> {{}} is Relation-like {{{}}} -defined Function-like one-to-one () set

{{{}}} --> {{}} is non empty Relation-like non-empty {{{}}} -defined {{{}}} -valued Function-like constant V17({{{}}}) V18({{{}}},{{{}}}) () Element of bool [:{{{}}},{{{}}}:]

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

bool [:{{{}}},{{{}}}:] is non empty () () set

F is Relation-like {{{}}} -defined Function-like one-to-one () set

e is set

F . e is set

F is Relation-like set

e is set

proj2 F is set

F is Relation-like Function-like () set

e is set

F . e is set

proj1 F is set

proj1 F is set

proj1 F is set

F is Relation-like () set

proj2 F is set

e is set