let m be Element of NAT ; :: thesis: not SubstPoset NAT ,{m} is complete
reconsider Cos = {(PFArt 1,m)} as Element of (SubstPoset NAT ,{m}) by Th31;
assume SubstPoset NAT ,{m} is complete ; :: thesis: contradiction
then consider a being Element of (SubstPoset NAT ,{m}) such that
A1: PFDrt m is_>=_than a and
A2: for b being Element of (SubstPoset NAT ,{m}) st PFDrt m is_>=_than b holds
a >= b by LATTICE5:def 2;
SubstitutionSet NAT ,{m} = the carrier of (SubstPoset NAT ,{m}) by SUBSTLAT:def 4;
then a in SubstitutionSet NAT ,{m} ;
then reconsider a9 = a as Element of Fin (PFuncs NAT ,{m}) ;
set Mi = Involved a9;
PFDrt m is_>=_than Cos
proof
let u be Element of (SubstPoset NAT ,{m}); :: according to LATTICE3:def 8 :: thesis: ( not u in PFDrt m or Cos <= u )
assume u in PFDrt m ; :: thesis: Cos <= u
then consider n1 being non empty Element of NAT such that
A3: u = PFBrt n1,m by Def5;
now
let d be set ; :: thesis: ( d in Cos implies ex e being set st
( e in u & e c= d ) )
assume d in Cos ; :: thesis: ex e being set st
( e in u & e c= d )
then A4: d = PFArt 1,m by TARSKI:def 1;
1 <= n1 by NAT_1:14;
then d in PFBrt n1,m by A4, Def4;
hence ex e being set st
( e in u & e c= d ) by A3; :: thesis: verum
end;
hence Cos <= u by Th15; :: thesis: verum
end;
then a <> {} by A2, Th42;
then reconsider Mi = Involved a9 as non empty finite Subset of NAT by A1, Th37, Th43;
reconsider mX = (max Mi) + 1 as non empty Element of NAT ;
reconsider Sum = {(PFArt mX,m)} as Element of (SubstPoset NAT ,{m}) by Th31;
set b = a "\/" Sum;
Sum is_<=_than PFDrt m
proof
let t be Element of (SubstPoset NAT ,{m}); :: according to LATTICE3:def 8 :: thesis: ( not t in PFDrt m or Sum <= t )
assume t in PFDrt m ; :: thesis: Sum <= t
then consider n being non empty Element of NAT such that
A5: t = PFBrt n,m by Def5;
for x being set st x in Sum holds
ex y being set st
( y in t & y c= x )
proof
let x be set ; :: thesis: ( x in Sum implies ex y being set st
( y in t & y c= x ) )
assume A6: x in Sum ; :: thesis: ex y being set st
( y in t & y c= x )
then A7: x = PFArt mX,m by TARSKI:def 1;
per cases ( n < mX or n >= mX ) ;
suppose A8: n < mX ; :: thesis: ex y being set st
( y in t & y c= x )
take y = PFCrt n,m; :: thesis: ( y in t & y c= x )
thus y in t by A5, Def4; :: thesis: y c= x
thus y c= x by A7, A8, Lm7; :: thesis: verum
end;
suppose A9: n >= mX ; :: thesis: ex y being set st
( y in t & y c= x )
take y = PFArt mX,m; :: thesis: ( y in t & y c= x )
thus y in t by A5, A9, Def4; :: thesis: y c= x
thus y c= x by A6, TARSKI:def 1; :: thesis: verum
end;
end;
end;
hence Sum <= t by Th15; :: thesis: verum
end;
then A10: PFDrt m is_>=_than a "\/" Sum by A1, Th34;
A11: a <> a "\/" Sum
proof
A12: PFArt mX,m in Sum by TARSKI:def 1;
assume A13: a = a "\/" Sum ; :: thesis: contradiction
then Sum <= a by YELLOW_0:24;
then consider g being set such that
A14: g in a and
A15: g c= PFArt mX,m by A12, Th15;
per cases ( not g is empty or g is empty ) ;
suppose not g is empty ; :: thesis: contradiction
then consider n being Element of NAT such that
A16: [n,m] in g and
A17: n is even by A1, A14, Th33;
now
per cases ( ex m9 being odd Element of NAT st
( m9 <= 2 * mX & [m9,m] = [n,m] ) or [(2 * mX),m] = [n,m] ) by A15, A16, Def2;
suppose ex m9 being odd Element of NAT st
( m9 <= 2 * mX & [m9,m] = [n,m] ) ; :: thesis: contradiction
hence contradiction by A17, ZFMISC_1:33; :: thesis: verum
end;
suppose [(2 * mX),m] = [n,m] ; :: thesis: contradiction
hence contradiction by A14, A16, Th38, XREAL_1:157; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
a <= a "\/" Sum by YELLOW_0:22;
then a < a "\/" Sum by A11, ORDERS_2:def 10;
hence contradiction by A2, A10, ORDERS_2:30; :: thesis: verum