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