let A be partial non-empty UAStr ; :: thesis: for P being a_partition of A holds P is_finer_than Class (LimDomRel A)
let P be a_partition of A; :: thesis: 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 ; :: according to SETFAM_1:def 2 :: thesis: ( not a in P or ex b1 being set st
( b1 in Class (LimDomRel A) & a c= b1 ) )
assume a in P ; :: thesis: 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) ; :: thesis: ( 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; :: thesis: a c= Class ((LimDomRel A), the Element of aa)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in a or y in Class ((LimDomRel A), the Element of aa) )
assume y in a ; :: thesis: 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 ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in EP or [x,y] in (DomRel A) |^ (A,0) )
assume A3: [x,y] in EP ; :: thesis: [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 )
proof
let f be operation of A; :: thesis: for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f )
let p, q be FinSequence; :: thesis: ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f )
A6: f is_exactly_partitable_wrt P by Def10;
now :: thesis: for p, q being FinSequence
for x, y being Element of a st (p ^ <*x*>) ^ q in dom f holds
(p ^ <*y*>) ^ q in dom f
let p, q be FinSequence; :: thesis: for x, y being Element of a st (p ^ <*x*>) ^ q in dom f holds
(p ^ <*y*>) ^ q in dom f
let x, y be Element of a; :: thesis: ( (p ^ <*x*>) ^ q in dom f implies (p ^ <*y*>) ^ q in dom f )
assume A7: (p ^ <*x*>) ^ q in dom f ; :: thesis: (p ^ <*y*>) ^ q in dom f
then (p ^ <*x*>) ^ q is FinSequence of the carrier of A by FINSEQ_1:def 11;
then consider pp being FinSequence of P such that
A8: (p ^ <*x*>) ^ q in product pp by Th6;
product pp meets dom f by A7, A8, XBOOLE_0:3;
then A9: product pp c= dom f by A6;
(p ^ <*y*>) ^ q in product pp by A8, Th25;
hence (p ^ <*y*>) ^ q in dom f by A9; :: thesis: verum
end;
hence ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) by A4, A5; :: thesis: verum
end;
then [x,y] in DomRel A by Def4;
hence [x,y] in (DomRel A) |^ (A,0) by Th15; :: thesis: verum
end;
A10: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A11: EP c= (DomRel A) |^ (A,i) ; :: thesis: S1[i + 1]
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in EP or [x,y] in (DomRel A) |^ (A,(i + 1)) )
assume A12: [x,y] in EP ; :: thesis: [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 :: thesis: 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; :: thesis: 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; :: thesis: ( (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 ; :: thesis: [(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; :: thesis: 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; :: thesis: verum
end;
A21: for i being Nat holds S1[i] from NAT_1:sch 2(A2, A10);
now :: thesis: for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i)
let i be Element of NAT ; :: thesis: [x,y] in (DomRel A) |^ (A,i)
ex x being object st
( x in the carrier of A & aa = Class (EP,x) ) by A1, EQREL_1:def 3;
then A22: [x,y] in EP by EQREL_1:22;
EP c= (DomRel A) |^ (A,i) by A21;
hence [x,y] in (DomRel A) |^ (A,i) by A22; :: thesis: verum
end;
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; :: thesis: verum