let A be partial non-empty UAStr ; for P being a_partition of A holds P is_finer_than Class (LimDomRel A)
let P be a_partition of A; P is_finer_than Class (LimDomRel A)
consider EP being Equivalence_Relation of the carrier of A such that
A1:
P = Class EP
by EQREL_1:34;
let a be set ; SETFAM_1:def 2 ( not a in P or ex b1 being set st
( b1 in Class (LimDomRel A) & a c= b1 ) )
assume
a in P
; ex b1 being set st
( b1 in Class (LimDomRel A) & a c= b1 )
then reconsider aa = a as Element of P ;
set x = the Element of aa;
take
Class ((LimDomRel A), the Element of aa)
; ( Class ((LimDomRel A), the Element of aa) in Class (LimDomRel A) & a c= Class ((LimDomRel A), the Element of aa) )
thus
Class ((LimDomRel A), the Element of aa) in Class (LimDomRel A)
by EQREL_1:def 3; a c= Class ((LimDomRel A), the Element of aa)
let y be object ; TARSKI:def 3 ( not y in a or y in Class ((LimDomRel A), the Element of aa) )
assume
y in a
; y in Class ((LimDomRel A), the Element of aa)
then reconsider y = y as Element of aa ;
reconsider x = the Element of aa, y = y as Element of A ;
defpred S1[ Nat] means EP c= (DomRel A) |^ (A,$1);
A2:
S1[ 0 ]
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in EP or [x,y] in (DomRel A) |^ (A,0) )
assume A3:
[x,y] in EP
;
[x,y] in (DomRel A) |^ (A,0)
then reconsider x =
x,
y =
y as
Element of
A by ZFMISC_1:87;
reconsider a =
Class (
EP,
y) as
Element of
P by A1, EQREL_1:def 3;
A4:
x in a
by A3, EQREL_1:19;
A5:
y in a
by EQREL_1:20;
for
f being
operation of
A for
p,
q being
FinSequence holds
(
(p ^ <*x*>) ^ q in dom f iff
(p ^ <*y*>) ^ q in dom f )
then
[x,y] in DomRel A
by Def4;
hence
[x,y] in (DomRel A) |^ (
A,
0)
by Th15;
verum
end;
A10:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A11:
EP c= (DomRel A) |^ (
A,
i)
;
S1[i + 1]
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in EP or [x,y] in (DomRel A) |^ (A,(i + 1)) )
assume A12:
[x,y] in EP
;
[x,y] in (DomRel A) |^ (A,(i + 1))
then reconsider x =
x,
y =
y as
Element of
A by ZFMISC_1:87;
reconsider a =
Class (
EP,
y) as
Element of
P by A1, EQREL_1:def 3;
now for f being operation of A
for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ (A,i)let f be
operation of
A;
for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ (A,i)let p,
q be
FinSequence;
( (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f implies [(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ (A,i) )assume that A13:
(p ^ <*x*>) ^ q in dom f
and A14:
(p ^ <*y*>) ^ q in dom f
;
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ (A,i)
(p ^ <*x*>) ^ q is
FinSequence of the
carrier of
A
by A13, FINSEQ_1:def 11;
then consider pp being
FinSequence of
P such that A15:
(p ^ <*x*>) ^ q in product pp
by Th6;
f is_exactly_partitable_wrt P
by Def10;
then
f is_partitable_wrt P
;
then consider c being
Element of
P such that A16:
f .: (product pp) c= c
;
A17:
x in a
by A12, EQREL_1:19;
y in a
by EQREL_1:20;
then A18:
(p ^ <*y*>) ^ q in product pp
by A15, A17, Th25;
A19:
f . ((p ^ <*x*>) ^ q) in f .: (product pp)
by A13, A15, FUNCT_1:def 6;
A20:
f . ((p ^ <*y*>) ^ q) in f .: (product pp)
by A14, A18, FUNCT_1:def 6;
ex
x being
object st
(
x in the
carrier of
A &
c = Class (
EP,
x) )
by A1, EQREL_1:def 3;
then
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in EP
by A16, A19, A20, EQREL_1:22;
hence
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ (
A,
i)
by A11;
verum end;
then
[x,y] in ((DomRel A) |^ (A,i)) |^ A
by A11, A12, Def5;
hence
[x,y] in (DomRel A) |^ (
A,
(i + 1))
by Th16;
verum
end;
A21:
for i being Nat holds S1[i]
from NAT_1:sch 2(A2, A10);
then
[x,y] in LimDomRel A
by Def7;
then
[y,x] in LimDomRel A
by EQREL_1:6;
hence
y in Class ((LimDomRel A), the Element of aa)
by EQREL_1:19; verum