let R be non empty RelStr ; :: thesis: ( R is well_founded iff for V being non empty set
for H being Function of [:the carrier of R,(PFuncs the carrier of R,V):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H )
set c = the carrier of R;
set r = the InternalRel of R;
defpred S1[] means for V being non empty set
for H being Function of [:the carrier of R,(PFuncs the carrier of R,V):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H;
thus
( R is well_founded implies S1[] )
:: thesis: ( ( for V being non empty set
for H being Function of [:the carrier of R,(PFuncs the carrier of R,V):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H ) implies R is well_founded )proof
assume A1:
R is
well_founded
;
:: thesis: S1[]
let V be non
empty set ;
:: thesis: for H being Function of [:the carrier of R,(PFuncs the carrier of R,V):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by Hlet H be
Function of
[:the carrier of R,(PFuncs the carrier of R,V):],
V;
:: thesis: ex F being Function of the carrier of R,V st F is_recursively_expressed_by H
defpred S2[
PartFunc of the
carrier of
R,
V]
means (
dom $1 is
lower & ( for
x being
set st
x in dom $1 holds
$1
. x = H . [x,($1 | (the InternalRel of R -Seg x))] ) );
consider fs being
Subset of
(PFuncs the carrier of R,V) such that A2:
for
f being
PartFunc of the
carrier of
R,
V holds
(
f in fs iff
S2[
f] )
from WELLFND1:sch 1();
now let f,
g be
Function;
:: thesis: ( f in fs & g in fs implies f tolerates g )assume A3:
(
f in fs &
g in fs )
;
:: thesis: f tolerates gthen reconsider ff =
f,
gg =
g as
PartFunc of the
carrier of
R,
V by PARTFUN1:120;
assume
not
f tolerates g
;
:: thesis: contradictionthen consider x being
set such that A4:
(
x in (dom ff) /\ (dom gg) &
ff . x <> gg . x )
by PARTFUN1:def 6;
reconsider x =
x as
Element of
R by A4;
defpred S3[
set ]
means ( $1
in dom ff & $1
in dom gg &
ff . $1
<> gg . $1 );
A5:
S3[
x]
by A4, XBOOLE_0:def 4;
consider x0 being
Element of
R such that A6:
S3[
x0]
and A7:
for
y being
Element of
R holds
( not
x0 <> y or not
S3[
y] or not
[y,x0] in the
InternalRel of
R )
from WELLFND1:sch 2(A5, A1);
ff | (the InternalRel of R -Seg x0) = gg | (the InternalRel of R -Seg x0)
proof
set fr =
ff | (the InternalRel of R -Seg x0);
set gr =
gg | (the InternalRel of R -Seg x0);
assume A8:
not
ff | (the InternalRel of R -Seg x0) = gg | (the InternalRel of R -Seg x0)
;
:: thesis: contradiction
A9:
dom ff is
lower
by A2, A3;
then A10:
dom (ff | (the InternalRel of R -Seg x0)) = the
InternalRel of
R -Seg x0
by A6, Th5, RELAT_1:91;
A11:
dom gg is
lower
by A2, A3;
then
dom (ff | (the InternalRel of R -Seg x0)) = dom (gg | (the InternalRel of R -Seg x0))
by A6, A10, Th5, RELAT_1:91;
then consider x1 being
set such that A12:
(
x1 in dom (ff | (the InternalRel of R -Seg x0)) &
(ff | (the InternalRel of R -Seg x0)) . x1 <> (gg | (the InternalRel of R -Seg x0)) . x1 )
by A8, FUNCT_1:9;
A13:
[x1,x0] in the
InternalRel of
R
by A10, A12, WELLORD1:def 1;
reconsider x1 =
x1 as
Element of
R by A12;
A14:
(
(ff | (the InternalRel of R -Seg x0)) . x1 = ff . x1 &
(gg | (the InternalRel of R -Seg x0)) . x1 = gg . x1 )
by A10, A12, FUNCT_1:72;
A15:
x1 <> x0
by A10, A12, WELLORD1:def 1;
(
x1 in dom ff &
x1 in dom gg )
by A6, A9, A11, A13, Def1;
hence
contradiction
by A7, A12, A13, A14, A15;
:: thesis: verum
end; then ff . x0 =
H . [x0,(gg | (the InternalRel of R -Seg x0))]
by A2, A3, A6
.=
gg . x0
by A2, A3, A6
;
hence
contradiction
by A6;
:: thesis: verum end;
then reconsider ufs =
union fs as
Function by Th2;
A16:
dom ufs c= the
carrier of
R
A19:
rng ufs c= V
A23:
now let x be
set ;
:: thesis: ( x in dom ufs implies ufs . x = H . [x,(ufs | (the InternalRel of R -Seg x))] )assume
x in dom ufs
;
:: thesis: ufs . x = H . [x,(ufs | (the InternalRel of R -Seg x))]then
[x,(ufs . x)] in ufs
by FUNCT_1:8;
then consider fx being
set such that A24:
(
[x,(ufs . x)] in fx &
fx in fs )
by TARSKI:def 4;
reconsider ff =
fx as
PartFunc of the
carrier of
R,
V by A24, PARTFUN1:120;
A25:
x in dom ff
by A24, FUNCT_1:8;
A26:
dom ff is
lower
by A2, A24;
A27:
ff c= ufs
by A24, ZFMISC_1:92;
thus ufs . x =
ff . x
by A24, FUNCT_1:8
.=
H . [x,(ff | (the InternalRel of R -Seg x))]
by A2, A24, A25
.=
H . [x,(ufs | (the InternalRel of R -Seg x))]
by A25, A26, A27, Th5, GRFUNC_1:95
;
:: thesis: verum end;
A28:
now let x,
y be
set ;
:: thesis: ( x in dom ufs & [y,x] in the InternalRel of R implies y in dom ufs )assume A29:
(
x in dom ufs &
[y,x] in the
InternalRel of
R )
;
:: thesis: y in dom ufsthen
[x,(ufs . x)] in ufs
by FUNCT_1:8;
then consider fx being
set such that A30:
(
[x,(ufs . x)] in fx &
fx in fs )
by TARSKI:def 4;
reconsider ff =
fx as
PartFunc of the
carrier of
R,
V by A30, PARTFUN1:120;
A31:
dom ff is
lower
by A2, A30;
x in dom ff
by A30, FUNCT_1:8;
then A32:
y in dom ff
by A29, A31, Def1;
ff c= ufs
by A30, ZFMISC_1:92;
then
dom ff c= dom ufs
by GRFUNC_1:8;
hence
y in dom ufs
by A32;
:: thesis: verum end;
A33:
dom ufs = the
carrier of
R
proof
assume
dom ufs <> the
carrier of
R
;
:: thesis: contradiction
then consider x being
set such that A34:
( (
x in dom ufs & not
x in the
carrier of
R ) or (
x in the
carrier of
R & not
x in dom ufs ) )
by TARSKI:2;
reconsider x =
x as
Element of
R by A16, A34;
defpred S3[
set ]
means ( $1
in the
carrier of
R & not $1
in dom ufs );
A35:
S3[
x]
by A34;
consider x0 being
Element of
R such that A36:
S3[
x0]
and A37:
for
y being
Element of
R holds
( not
x0 <> y or not
S3[
y] or not
[y,x0] in the
InternalRel of
R )
from WELLFND1:sch 2(A35, A1);
set nv =
x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]);
set nf =
ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]));
A38:
dom (ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))) = (dom ufs) \/ (dom (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))])))
by FUNCT_4:def 1;
A39:
dom (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))])) = {x0}
by FUNCOP_1:19;
then
x0 in dom (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))
by TARSKI:def 1;
then
x0 in dom (ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))])))
by A38, XBOOLE_0:def 3;
then A40:
[x0,((ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))) . x0)] in ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))
by FUNCT_1:8;
A41:
dom (ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))) c= the
carrier of
R
rng (ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))) c= V
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng (ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))) or x in V )
assume A43:
x in rng (ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))])))
;
:: thesis: x in V
A44:
rng (ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))) c= (rng ufs) \/ (rng (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))])))
by FUNCT_4:18;
assume A45:
not
x in V
;
:: thesis: contradiction
then
not
x in rng ufs
by A19;
then A46:
x in rng (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))
by A43, A44, XBOOLE_0:def 3;
rng (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))])) = {(H . [x0,(ufs | (the InternalRel of R -Seg x0))])}
by FUNCOP_1:14;
then A47:
x = H . x0,
(ufs | (the InternalRel of R -Seg x0))
by A46, TARSKI:def 1;
ufs in PFuncs the
carrier of
R,
V
by A16, A19, PARTFUN1:def 5;
then
ufs is
PartFunc of the
carrier of
R,
V
by PARTFUN1:120;
then
ufs | (the InternalRel of R -Seg x0) is
PartFunc of the
carrier of
R,
V
by PARTFUN1:44;
then
ufs | (the InternalRel of R -Seg x0) in PFuncs the
carrier of
R,
V
by PARTFUN1:119;
hence
contradiction
by A45, A47, BINOP_1:29;
:: thesis: verum
end;
then
ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))])) in PFuncs the
carrier of
R,
V
by A41, PARTFUN1:def 5;
then reconsider nf =
ufs +* (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))])) as
PartFunc of the
carrier of
R,
V by PARTFUN1:120;
A48:
dom nf is
lower
proof
let x,
y be
set ;
:: according to WELLFND1:def 1 :: thesis: ( x in dom nf & [y,x] in the InternalRel of R implies y in dom nf )
assume A49:
(
x in dom nf &
[y,x] in the
InternalRel of
R )
;
:: thesis: y in dom nf
assume A50:
not
y in dom nf
;
:: thesis: contradiction
then A51:
not
y in dom ufs
by A38, XBOOLE_0:def 3;
then
not
x in dom ufs
by A28, A49;
then
x in dom (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))
by A38, A49, XBOOLE_0:def 3;
then A52:
x = x0
by A39, TARSKI:def 1;
reconsider y =
y as
Element of
R by A49, ZFMISC_1:106;
not
y in dom (x0 .--> (H . [x0,(ufs | (the InternalRel of R -Seg x0))]))
by A38, A50, XBOOLE_0:def 3;
then
y <> x0
by A39, TARSKI:def 1;
hence
contradiction
by A37, A49, A51, A52;
:: thesis: verum
end;
then
nf in fs
by A2, A48;
then
[x0,(nf . x0)] in ufs
by A40, TARSKI:def 4;
hence
contradiction
by A36, FUNCT_1:8;
:: thesis: verum
end;
then reconsider ufs =
ufs as
Function of the
carrier of
R,
V by A19, FUNCT_2:def 1, RELSET_1:11;
take
ufs
;
:: thesis: ufs is_recursively_expressed_by H
let x be
Element of the
carrier of
R;
:: according to WELLFND1:def 5 :: thesis: ufs . x = H . x,(ufs | (the InternalRel of R -Seg x))
thus
ufs . x = H . x,
(ufs | (the InternalRel of R -Seg x))
by A23, A33;
:: thesis: verum
end;
assume A62:
S1[]
; :: thesis: R is well_founded
reconsider ac = omega +` (card the carrier of R) as infinite Cardinal ;
set V = nextcard ac;
deffunc H1( Element of the carrier of R, Element of PFuncs the carrier of R,(nextcard ac)) -> set = sup (rng $2);
A63:
for x being Element of the carrier of R
for p being Element of PFuncs the carrier of R,(nextcard ac) holds H1(x,p) in nextcard ac
consider H being Function of [:the carrier of R,(PFuncs the carrier of R,(nextcard ac)):], nextcard ac such that
A66:
for x being Element of the carrier of R
for p being Element of PFuncs the carrier of R,(nextcard ac) holds H . x,p = H1(x,p)
from FUNCT_7:sch 1(A63);
consider rk being Function of the carrier of R, nextcard ac such that
A67:
rk is_recursively_expressed_by H
by A62;
A68:
dom rk = the carrier of R
by FUNCT_2:def 1;
let Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 2 :: thesis: ( not Y c= the carrier of R or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )
assume A69:
( Y c= the carrier of R & Y <> {} )
; :: thesis: ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )
then consider b being set such that
A70:
b in Y
by XBOOLE_0:def 1;
set m = inf (rk .: Y);
rk . b in nextcard ac
by A69, A70, FUNCT_2:7;
then
( rk . b in rk .: Y & rk . b is Ordinal )
by A68, A69, A70, FUNCT_1:def 12;
then
inf (rk .: Y) in rk .: Y
by ORDINAL2:25;
then consider a being set such that
A71:
( a in dom rk & a in Y & rk . a = inf (rk .: Y) )
by FUNCT_1:def 12;
take
a
; :: thesis: ( a in Y & the InternalRel of R -Seg a misses Y )
thus
a in Y
by A71; :: thesis: the InternalRel of R -Seg a misses Y
assume
(the InternalRel of R -Seg a) /\ Y <> {}
; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider e being set such that
A72:
e in (the InternalRel of R -Seg a) /\ Y
by XBOOLE_0:def 1;
A73:
( e in the InternalRel of R -Seg a & e in Y )
by A72, XBOOLE_0:def 4;
then reconsider rke = rk . e as Ordinal by A69, FUNCT_2:7, ORDINAL1:23;
rke in rk .: Y
by A68, A69, A73, FUNCT_1:def 12;
then A74:
inf (rk .: Y) c= rk . e
by ORDINAL2:22;
reconsider a = a as Element of the carrier of R by A71;
reconsider rkra = rk | (the InternalRel of R -Seg a) as Element of PFuncs the carrier of R,(nextcard ac) by PARTFUN1:119;
A75: rk . a =
H . a,rkra
by A67, Def5
.=
sup (rng rkra)
by A66
;
rke in rng rkra
by A68, A69, A73, FUNCT_1:73;
hence
contradiction
by A71, A74, A75, ORDINAL1:7, ORDINAL2:27; :: thesis: verum