set bX = bool F1();
consider R being Relation such that
A3:
R well_orders F1()
by WELLORD2:17;
R /\ [:F1(),F1():] c= [:F1(),F1():]
by XBOOLE_1:17;
then reconsider R2 = R |_2 F1() as Relation of F1() by WELLORD1:def 6;
reconsider RS = RelStr(# F1(),R2 #) as non empty RelStr ;
set cRS = the carrier of RS;
defpred S1[ object , object , object ] means for p being Element of F1()
for f being PartFunc of the carrier of RS,(bool F1()) st $1 = p & $2 = f holds
( ( ( for q being Element of F1() st q in union (rng f) holds
P1[p,q] ) implies $3 = (union (rng f)) \/ {p} ) & ( ex q being Element of F1() st
( q in union (rng f) & P1[p,q] ) implies $3 = union (rng f) ) );
A4:
for x, y being object st x in the carrier of RS & y in PFuncs ( the carrier of RS,(bool F1())) holds
ex z being object st
( z in bool F1() & S1[x,y,z] )
consider h being Function of [: the carrier of RS,(PFuncs ( the carrier of RS,(bool F1()))):],(bool F1()) such that
A9:
for x, y being object st x in the carrier of RS & y in PFuncs ( the carrier of RS,(bool F1())) holds
S1[x,y,h . (x,y)]
from BINOP_1:sch 1(A4);
set IRS = the InternalRel of RS;
A10:
R2 well_orders F1()
by A3, PCOMPS_2:1;
then
R2 is_well_founded_in F1()
by WELLORD1:def 5;
then A11:
RS is well_founded
by WELLFND1:def 2;
then consider f being Function of the carrier of RS,(bool F1()) such that
A12:
f is_recursively_expressed_by h
by WELLFND1:11;
defpred S2[ set ] means ( f . $1 c= ( the InternalRel of RS -Seg $1) \/ {$1} & ( $1 in f . $1 implies for r being Element of F1() st r in union (rng (f | ( the InternalRel of RS -Seg $1))) holds
P1[$1,r] ) & ( not $1 in f . $1 implies ex r being Element of F1() st
( r in union (rng (f | ( the InternalRel of RS -Seg $1))) & P1[$1,r] ) ) );
reconsider rngf = rng f as Subset of (bool F1()) ;
take A = union rngf; ( ( for x, y being Element of F1() st x in A & y in A & x <> y holds
P1[x,y] ) & ( for x being Element of F1() ex y being Element of F1() st
( y in A & P1[x,y] ) ) )
A13:
field R2 = F1()
by A3, PCOMPS_2:1;
then A14:
R2 is well-ordering
by A10, WELLORD1:4;
A15:
for x being Element of RS st ( for y being Element of RS st y <> x & [y,x] in the InternalRel of RS holds
S2[y] ) holds
S2[x]
proof
let x be
Element of
RS;
( ( for y being Element of RS st y <> x & [y,x] in the InternalRel of RS holds
S2[y] ) implies S2[x] )
assume A16:
for
y being
Element of
RS st
y <> x &
[y,x] in the
InternalRel of
RS holds
S2[
y]
;
S2[x]
set fIx =
f | ( the InternalRel of RS -Seg x);
A17:
union (rng (f | ( the InternalRel of RS -Seg x))) c= the
InternalRel of
RS -Seg x
proof
let y be
object ;
TARSKI:def 3 ( not y in union (rng (f | ( the InternalRel of RS -Seg x))) or y in the InternalRel of RS -Seg x )
assume
y in union (rng (f | ( the InternalRel of RS -Seg x)))
;
y in the InternalRel of RS -Seg x
then consider z being
set such that A18:
y in z
and A19:
z in rng (f | ( the InternalRel of RS -Seg x))
by TARSKI:def 4;
consider t being
object such that A20:
t in dom (f | ( the InternalRel of RS -Seg x))
and A21:
(f | ( the InternalRel of RS -Seg x)) . t = z
by A19, FUNCT_1:def 3;
A22:
t in the
InternalRel of
RS -Seg x
by A20, RELAT_1:57;
reconsider t =
t as
Element of
RS by A20;
A23:
{t} c= the
InternalRel of
RS -Seg x
by A22, ZFMISC_1:31;
A24:
[t,x] in the
InternalRel of
RS
by A22, WELLORD1:1;
then
the
InternalRel of
RS -Seg t c= the
InternalRel of
RS -Seg x
by A13, A14, WELLORD1:29;
then A25:
( the InternalRel of RS -Seg t) \/ {t} c= the
InternalRel of
RS -Seg x
by A23, XBOOLE_1:8;
t <> x
by A22, WELLORD1:1;
then A26:
f . t c= ( the InternalRel of RS -Seg t) \/ {t}
by A16, A24;
(f | ( the InternalRel of RS -Seg x)) . t = f . t
by A20, FUNCT_1:47;
then
y in ( the InternalRel of RS -Seg t) \/ {t}
by A18, A21, A26;
hence
y in the
InternalRel of
RS -Seg x
by A25;
verum
end;
A27:
f | ( the InternalRel of RS -Seg x) in PFuncs ( the
carrier of
RS,
(bool F1()))
by PARTFUN1:45;
A28:
f . x = h . (
x,
(f | ( the InternalRel of RS -Seg x)))
by A12, WELLFND1:def 5;
per cases
( for q being Element of F1() st q in union (rng (f | ( the InternalRel of RS -Seg x))) holds
P1[x,q] or ex q being Element of F1() st
( q in union (rng (f | ( the InternalRel of RS -Seg x))) & P1[x,q] ) )
;
suppose A29:
for
q being
Element of
F1() st
q in union (rng (f | ( the InternalRel of RS -Seg x))) holds
P1[
x,
q]
;
S2[x]then A30:
f . x = (union (rng (f | ( the InternalRel of RS -Seg x)))) \/ {x}
by A9, A28, A27;
hence
f . x c= ( the InternalRel of RS -Seg x) \/ {x}
by A17, XBOOLE_1:9;
( ( x in f . x implies for r being Element of F1() st r in union (rng (f | ( the InternalRel of RS -Seg x))) holds
P1[x,r] ) & ( not x in f . x implies ex r being Element of F1() st
( r in union (rng (f | ( the InternalRel of RS -Seg x))) & P1[x,r] ) ) )thus
(
x in f . x implies for
r being
Element of
F1() st
r in union (rng (f | ( the InternalRel of RS -Seg x))) holds
P1[
x,
r] )
by A29;
( not x in f . x implies ex r being Element of F1() st
( r in union (rng (f | ( the InternalRel of RS -Seg x))) & P1[x,r] ) )A31:
x in {x}
by TARSKI:def 1;
assume
not
x in f . x
;
ex r being Element of F1() st
( r in union (rng (f | ( the InternalRel of RS -Seg x))) & P1[x,r] )hence
ex
r being
Element of
F1() st
(
r in union (rng (f | ( the InternalRel of RS -Seg x))) &
P1[
x,
r] )
by A30, A31, XBOOLE_0:def 3;
verum end;
end;
A34:
for x being Element of RS holds S2[x]
from WELLFND1:sch 3(A15, A11);
thus
for x, y being Element of F1() st x in A & y in A & x <> y holds
P1[x,y]
for x being Element of F1() ex y being Element of F1() st
( y in A & P1[x,y] )proof
A35:
now for x being Element of F1() st x in A holds
x in f . xlet x be
Element of
F1();
( x in A implies x in f . x )assume
x in A
;
x in f . xthen consider y being
set such that A36:
x in y
and A37:
y in rng f
by TARSKI:def 4;
defpred S3[
set ]
means x in f . $1;
consider z being
object such that A38:
z in dom f
and A39:
f . z = y
by A37, FUNCT_1:def 3;
reconsider z =
z as
Element of
RS by A38;
A40:
S3[
z]
by A36, A39;
consider p being
Element of
RS such that A41:
S3[
p]
and A42:
for
q being
Element of
RS holds
( not
p <> q or not
S3[
q] or not
[q,p] in the
InternalRel of
RS )
from WELLFND1:sch 2(A40, A11);
p = x
proof
set fIp =
f | ( the InternalRel of RS -Seg p);
A43:
f | ( the InternalRel of RS -Seg p) in PFuncs ( the
carrier of
RS,
(bool F1()))
by PARTFUN1:45;
A44:
f . p = h . (
p,
(f | ( the InternalRel of RS -Seg p)))
by A12, WELLFND1:def 5;
assume A45:
p <> x
;
contradiction
then consider y9 being
set such that A48:
x in y9
and A49:
y9 in rng (f | ( the InternalRel of RS -Seg p))
by TARSKI:def 4;
consider z9 being
object such that A50:
z9 in dom (f | ( the InternalRel of RS -Seg p))
and A51:
(f | ( the InternalRel of RS -Seg p)) . z9 = y9
by A49, FUNCT_1:def 3;
reconsider z9 =
z9 as
Point of
RS by A50;
A52:
z9 in the
InternalRel of
RS -Seg p
by A50, RELAT_1:57;
then A53:
z9 <> p
by WELLORD1:1;
A54:
[z9,p] in the
InternalRel of
RS
by A52, WELLORD1:1;
S3[
z9]
by A48, A50, A51, FUNCT_1:47;
hence
contradiction
by A42, A53, A54;
verum
end; hence
x in f . x
by A41;
verum end;
A55:
now for x, y being Element of F1() st x in A & y in A & x <> y & [x,y] in the InternalRel of RS holds
P1[x,y]A56:
dom f = the
carrier of
RS
by FUNCT_2:def 1;
let x,
y be
Element of
F1();
( x in A & y in A & x <> y & [x,y] in the InternalRel of RS implies P1[x,y] )assume that A57:
x in A
and A58:
y in A
and A59:
x <> y
and A60:
[x,y] in the
InternalRel of
RS
;
P1[x,y]A61:
y in f . y
by A35, A58;
set fIy =
f | ( the InternalRel of RS -Seg y);
x in the
InternalRel of
RS -Seg y
by A59, A60, WELLORD1:1;
then A62:
x in dom (f | ( the InternalRel of RS -Seg y))
by A56, RELAT_1:57;
then A63:
(f | ( the InternalRel of RS -Seg y)) . x in rng (f | ( the InternalRel of RS -Seg y))
by FUNCT_1:def 3;
A64:
(f | ( the InternalRel of RS -Seg y)) . x = f . x
by A62, FUNCT_1:47;
x in f . x
by A35, A57;
then
x in union (rng (f | ( the InternalRel of RS -Seg y)))
by A63, A64, TARSKI:def 4;
then
P1[
y,
x]
by A34, A61;
hence
P1[
x,
y]
by A1;
verum end;
let x,
y be
Element of
F1();
( x in A & y in A & x <> y implies P1[x,y] )
assume that A65:
x in A
and A66:
y in A
and A67:
x <> y
;
P1[x,y]
R2 well_orders F1()
by A3, PCOMPS_2:1;
then
R2 is_connected_in F1()
by WELLORD1:def 5;
then
(
[x,y] in the
InternalRel of
RS or
[y,x] in the
InternalRel of
RS )
by A67, RELAT_2:def 6;
then
(
P1[
x,
y] or
P1[
y,
x] )
by A55, A65, A66, A67;
hence
P1[
x,
y]
by A1;
verum
end;
let x be Element of F1(); ex y being Element of F1() st
( y in A & P1[x,y] )