:: WELLSET1 semantic presentation
begin
theorem
:: WELLSET1:1
for
x
being ( ( ) ( )
set
)
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
x
: ( ( ) ( )
set
)
in
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
) iff ex
y
being ( ( ) ( )
set
) st
(
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) or
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) ) ) ;
theorem
:: WELLSET1:2
for
X
,
Y
being ( ( ) ( )
set
)
for
W
being ( (
Relation-like
) (
Relation-like
)
Relation
) st
X
: ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
Function-like
one-to-one
constant
functional
)
set
) &
Y
: ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
Function-like
one-to-one
constant
functional
)
set
) &
W
: ( (
Relation-like
) (
Relation-like
)
Relation
)
=
[:
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) holds
field
W
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
=
X
: ( ( ) ( )
set
)
\/
Y
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
scheme
:: WELLSET1:sch 1
RSeparation
{
F
1
()
->
( ( ) ( )
set
) ,
P
1
[ ( (
Relation-like
) (
Relation-like
)
Relation
) ] } :
ex
B
being ( ( ) ( )
set
) st
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
in
B
: ( ( ) ( )
set
) iff (
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
in
F
1
( ( ( ) ( )
set
) ) : ( ( ) ( )
set
) &
P
1
[
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) ] ) )
proof
end;
theorem
:: WELLSET1:3
for
x
,
y
being ( ( ) ( )
set
)
for
W
being ( (
Relation-like
) (
Relation-like
)
Relation
) st
x
: ( ( ) ( )
set
)
in
field
W
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
field
W
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
) &
W
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
well-ordering
& not
x
: ( ( ) ( )
set
)
in
W
: ( (
Relation-like
) (
Relation-like
)
Relation
)
-Seg
y
: ( ( ) ( )
set
) : ( ( ) ( )
set
) holds
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
W
: ( (
Relation-like
) (
Relation-like
)
Relation
) ;
theorem
:: WELLSET1:4
for
x
,
y
being ( ( ) ( )
set
)
for
W
being ( (
Relation-like
) (
Relation-like
)
Relation
) st
x
: ( ( ) ( )
set
)
in
field
W
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
field
W
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
) &
W
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
well-ordering
&
x
: ( ( ) ( )
set
)
in
W
: ( (
Relation-like
) (
Relation-like
)
Relation
)
-Seg
y
: ( ( ) ( )
set
) : ( ( ) ( )
set
) holds
not
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
W
: ( (
Relation-like
) (
Relation-like
)
Relation
) ;
theorem
:: WELLSET1:5
for
F
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
for
D
being ( ( ) ( )
set
) st ( for
X
being ( ( ) ( )
set
) st
X
: ( (
Relation-like
) (
Relation-like
)
Relation
)
in
D
: ( ( ) ( )
set
) holds
( not
F
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
X
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
in
X
: ( (
Relation-like
) (
Relation-like
)
Relation
) &
F
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
X
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
in
union
D
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
ex
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) st
(
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
c=
union
D
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
well-ordering
& not
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
in
D
: ( ( ) ( )
set
) & ( for
y
being ( ( ) ( )
set
) st
y
: ( ( ) ( )
set
)
in
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
-Seg
y
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
in
D
: ( ( ) ( )
set
) &
F
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
-Seg
y
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
y
: ( ( ) ( )
set
) ) ) ) ;
theorem
:: WELLSET1:6
for
N
being ( ( ) ( )
set
) ex
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) st
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
well-ordering
&
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
=
N
: ( ( ) ( )
set
) ) ;