consider R being Relation of F1() such that
A5:
for x, y being Element of F1() holds
( [x,y] in R iff P1[x,y] )
from RELSET_1:sch 2();
A6:
R is_transitive_in F1()
proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( not x in F1() or not y in F1() or not z in F1() or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that A7:
x in F1()
and A8:
y in F1()
and A9:
z in F1()
;
( not [x,y] in R or not [y,z] in R or [x,z] in R )
reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
F1()
by A7, A8, A9;
assume that A10:
[x,y] in R
and A11:
[y,z] in R
;
[x,z] in R
A12:
P1[
y9,
z9]
by A5, A11;
P1[
x9,
y9]
by A5, A10;
then
P1[
x9,
z9]
by A3, A12;
hence
[x,z] in R
by A5;
verum
end;
F1() c= dom R
then
dom R = F1()
;
then A13:
F1() c= field R
by XBOOLE_1:7;
field R = (dom R) \/ (rng R)
;
then A14:
field R = F1()
by A13;
A15:
R is_reflexive_in F1()
by A1, A5;
A16:
F1() has_upper_Zorn_property_wrt R
proof
let Y be
set ;
ORDERS_1:def 10 ( Y c= F1() & R |_2 Y is being_linear-order implies ex x being set st
( x in F1() & ( for y being set st y in Y holds
[y,x] in R ) ) )
assume that A17:
Y c= F1()
and A18:
R |_2 Y is
being_linear-order
;
ex x being set st
( x in F1() & ( for y being set st y in Y holds
[y,x] in R ) )
for
x,
y being
Element of
F1() st
x in Y &
y in Y &
P1[
x,
y] holds
P1[
y,
x]
proof
let x,
y be
Element of
F1();
( x in Y & y in Y & P1[x,y] implies P1[y,x] )
assume that A19:
x in Y
and A20:
y in Y
;
( P1[x,y] or P1[y,x] )
A21:
(
R |_2 Y is
reflexive &
R |_2 Y is
connected )
by A18;
Y c= field (R |_2 Y)
then A24:
Y =
field ((R |_2 Y) |_2 Y)
by A21, Lm7
.=
field (R |_2 Y)
by WELLORD1:21
;
then A25:
R |_2 Y is_connected_in Y
by A21;
A26:
R |_2 Y is_reflexive_in Y
by A21, A24;
(
x = y or
x <> y )
;
then
(
[x,y] in R |_2 Y or
[y,x] in R |_2 Y )
by A19, A20, A25, A26;
then
(
[x,y] in R or
[y,x] in R )
by XBOOLE_0:def 4;
hence
(
P1[
x,
y] or
P1[
y,
x] )
by A5;
verum
end;
then consider y being
Element of
F1()
such that A27:
for
x being
Element of
F1() st
x in Y holds
P1[
x,
y]
by A4, A17;
take
y
;
( y in F1() & ( for y being set st y in Y holds
[y,y] in R ) )
thus
y in F1()
;
for y being set st y in Y holds
[y,y] in R
let x be
set ;
( x in Y implies [x,y] in R )
assume A28:
x in Y
;
[x,y] in R
then
P1[
x,
y]
by A17, A27;
hence
[x,y] in R
by A5, A17, A28;
verum
end;
R is_antisymmetric_in F1()
proof
let x,
y be
object ;
RELAT_2:def 4 ( not x in F1() or not y in F1() or not [x,y] in R or not [y,x] in R or x = y )
assume that A29:
x in F1()
and A30:
y in F1()
;
( not [x,y] in R or not [y,x] in R or x = y )
reconsider x9 =
x,
y9 =
y as
Element of
F1()
by A29, A30;
assume that A31:
[x,y] in R
and A32:
[y,x] in R
;
x = y
A33:
P1[
y9,
x9]
by A5, A32;
P1[
x9,
y9]
by A5, A31;
hence
x = y
by A2, A33;
verum
end;
then
R partially_orders F1()
by A15, A6;
then consider x being set such that
A34:
x is_maximal_in R
by A14, A16, Th63;
take
x
; ( x is Element of F1() & ( for y being Element of F1() st x <> y holds
not P1[x,y] ) )
thus
x is Element of F1()
by A14, A34; for y being Element of F1() st x <> y holds
not P1[x,y]
let y be Element of F1(); ( x <> y implies not P1[x,y] )
assume
x <> y
; P1[x,y]
then A35:
not [x,y] in R
by A14, A34;
x in F1()
by A14, A34;
hence
P1[x,y]
by A5, A35; verum