set bX = bool F1();
consider R being Relation such that
A3:
R well_orders F1()
by WELLORD2:26;
( R /\ [:F1(),F1():] c= [:F1(),F1():] & R /\ [:F1(),F1():] = R |_2 F1() )
by WELLORD1:def 6, XBOOLE_1:17;
then reconsider R2 = R |_2 F1() as Relation of F1() ;
reconsider RS = RelStr(# F1(),R2 #) as non empty RelStr ;
A4:
( R2 well_orders F1() & field R2 = F1() )
by A3, PCOMPS_2:5;
then A5:
( R2 is_well_founded_in F1() & R2 is well-ordering )
by WELLORD1:8, WELLORD1:def 5;
then A6:
RS is well_founded
by WELLFND1:def 2;
set cRS = the carrier of RS;
set IRS = the InternalRel of RS;
defpred S1[ set , set , set ] 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) ) );
A7:
for x, y being set st x in the carrier of RS & y in PFuncs the carrier of RS,(bool F1()) holds
ex z being set 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
A11:
for x, y being set 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(A7);
consider f being Function of the carrier of RS,(bool F1()) such that
A12:
f is_recursively_expressed_by h
by A6, WELLFND1:12;
reconsider rngf = rng f as Subset of (bool F1()) ;
take A = union rngf; :: thesis: ( ( 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] ) ) )
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] ) ) );
A13:
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;
:: thesis: ( ( for y being Element of RS st y <> x & [y,x] in the InternalRel of RS holds
S2[y] ) implies S2[x] )
assume A14:
for
y being
Element of
RS st
y <> x &
[y,x] in the
InternalRel of
RS holds
S2[
y]
;
:: thesis: S2[x]
set fIx =
f | (the InternalRel of RS -Seg x);
A15:
union (rng (f | (the InternalRel of RS -Seg x))) c= the
InternalRel of
RS -Seg x
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in union (rng (f | (the InternalRel of RS -Seg x))) or y in the InternalRel of RS -Seg x )
assume A16:
y in union (rng (f | (the InternalRel of RS -Seg x)))
;
:: thesis: y in the InternalRel of RS -Seg x
consider z being
set such that A17:
(
y in z &
z in rng (f | (the InternalRel of RS -Seg x)) )
by A16, TARSKI:def 4;
consider t being
set such that A18:
(
t in dom (f | (the InternalRel of RS -Seg x)) &
(f | (the InternalRel of RS -Seg x)) . t = z )
by A17, FUNCT_1:def 5;
A19:
(
t in the
InternalRel of
RS -Seg x & the
InternalRel of
RS -Seg x c= the
carrier of
RS )
by A18, RELAT_1:86, WELLFND1:4;
reconsider t =
t as
Element of
RS by A18;
(
t <> x &
[t,x] in the
InternalRel of
RS )
by A19, WELLORD1:def 1;
then
(
f . t c= (the InternalRel of RS -Seg t) \/ {t} &
(f | (the InternalRel of RS -Seg x)) . t = f . t & the
InternalRel of
RS -Seg t c= the
InternalRel of
RS -Seg x &
{t} c= the
InternalRel of
RS -Seg x )
by A4, A5, A14, A18, A19, FUNCT_1:70, WELLORD1:37, ZFMISC_1:37;
then
(
y in (the InternalRel of RS -Seg t) \/ {t} &
(the InternalRel of RS -Seg t) \/ {t} c= the
InternalRel of
RS -Seg x )
by A17, A18, XBOOLE_1:8;
hence
y in the
InternalRel of
RS -Seg x
;
:: thesis: verum
end;
A20:
(
f . x = h . x,
(f | (the InternalRel of RS -Seg x)) &
f | (the InternalRel of RS -Seg x) in PFuncs the
carrier of
RS,
(bool F1()) )
by A12, PARTFUN1:119, 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 A21:
for
q being
Element of
F1() st
q in union (rng (f | (the InternalRel of RS -Seg x))) holds
P1[
x,
q]
;
:: thesis: S2[x]then A22:
f . x = (union (rng (f | (the InternalRel of RS -Seg x)))) \/ {x}
by A11, A20;
hence
f . x c= (the InternalRel of RS -Seg x) \/ {x}
by A15, XBOOLE_1:9;
:: thesis: ( ( 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 A21;
:: thesis: ( 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] ) )assume A23:
not
x in f . x
;
:: thesis: ex r being Element of F1() st
( r in union (rng (f | (the InternalRel of RS -Seg x))) & P1[x,r] )
x in {x}
by TARSKI:def 1;
hence
ex
r being
Element of
F1() st
(
r in union (rng (f | (the InternalRel of RS -Seg x))) &
P1[
x,
r] )
by A22, A23, XBOOLE_0:def 3;
:: thesis: verum end;
end;
A26:
for x being Element of RS holds S2[x]
from WELLFND1:sch 3(A13, A6);
thus
for x, y being Element of F1() st x in A & y in A & x <> y holds
P1[x,y]
:: thesis: for x being Element of F1() ex y being Element of F1() st
( y in A & P1[x,y] )proof
A38:
now let x,
y be
Element of
F1();
:: thesis: ( x in A & y in A & x <> y & [x,y] in the InternalRel of RS implies P1[x,y] )assume A39:
(
x in A &
y in A &
x <> y &
[x,y] in the
InternalRel of
RS )
;
:: thesis: P1[x,y]set fIy =
f | (the InternalRel of RS -Seg y);
(
dom f = the
carrier of
RS &
x in the
InternalRel of
RS -Seg y )
by A39, FUNCT_2:def 1, WELLORD1:def 1;
then
x in dom (f | (the InternalRel of RS -Seg y))
by RELAT_1:86;
then
(
x in f . x &
(f | (the InternalRel of RS -Seg y)) . x in rng (f | (the InternalRel of RS -Seg y)) &
(f | (the InternalRel of RS -Seg y)) . x = f . x )
by A27, A39, FUNCT_1:70, FUNCT_1:def 5;
then
(
y in f . y &
x in union (rng (f | (the InternalRel of RS -Seg y))) )
by A27, A39, TARSKI:def 4;
then
P1[
y,
x]
by A26;
hence
P1[
x,
y]
by A1;
:: thesis: verum end;
let x,
y be
Element of
F1();
:: thesis: ( x in A & y in A & x <> y implies P1[x,y] )
assume A40:
(
x in A &
y in A &
x <> y )
;
:: thesis: P1[x,y]
R2 well_orders F1()
by A3, PCOMPS_2:5;
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 A40, RELAT_2:def 6;
then
(
P1[
x,
y] or
P1[
y,
x] )
by A38, A40;
hence
P1[
x,
y]
by A1;
:: thesis: verum
end;
let x be Element of F1(); :: thesis: ex y being Element of F1() st
( y in A & P1[x,y] )