let p be RelStr-yielding ManySortedSet of {} ; :: thesis: ( not product p is empty & product p is quasi_ordered & product p is Dickson & product p is antisymmetric )
A1: product p = RelStr(# {{}},(id {{}}) #) by YELLOW_1:26;
set pp = product p;
set cpp = the carrier of (product p);
set ipp = the InternalRel of (product p);
A2: the InternalRel of (product p) = id {{}} by YELLOW_1:26;
thus not product p is empty by YELLOW_1:26; :: thesis: ( product p is quasi_ordered & product p is Dickson & product p is antisymmetric )
thus product p is quasi_ordered :: thesis: ( product p is Dickson & product p is antisymmetric )
proof
thus product p is reflexive by YELLOW_1:26; :: according to DICKSON:def 3 :: thesis: product p is transitive
let x, y, z be set ; :: according to RELAT_2:def 8,ORDERS_2:def 3 :: thesis: ( not x in the carrier of (product p) or not y in the carrier of (product p) or not z in the carrier of (product p) or not [x,y] in the InternalRel of (product p) or not [y,z] in the InternalRel of (product p) or [x,z] in the InternalRel of (product p) )
assume that
x in the carrier of (product p) and
y in the carrier of (product p) and
z in the carrier of (product p) and
A3: [x,y] in the InternalRel of (product p) and
A4: [y,z] in the InternalRel of (product p) ; :: thesis: [x,z] in the InternalRel of (product p)
thus [x,z] in the InternalRel of (product p) by A2, A3, A4, RELAT_1:def 10; :: thesis: verum
end;
thus product p is Dickson :: thesis: product p is antisymmetric
proof
let N be Subset of the carrier of (product p); :: according to DICKSON:def 10 :: thesis: ex B being set st
( B is_Dickson-basis_of N, product p & B is finite )
per cases ( N = {} or N = {{}} ) by A1, ZFMISC_1:33;
suppose A6: N = {{}} ; :: thesis: ex B being set st
( B is_Dickson-basis_of N, product p & B is finite )
take B = {{}}; :: thesis: ( B is_Dickson-basis_of N, product p & B is finite )
thus B is_Dickson-basis_of N, product p :: thesis: B is finite
proof
thus B c= N by A6; :: according to DICKSON:def 9 :: thesis: for a being Element of (product p) st a in N holds
ex b being Element of (product p) st
( b in B & b <= a )
let a be Element of (product p); :: thesis: ( a in N implies ex b being Element of (product p) st
( b in B & b <= a ) )
assume A7: a in N ; :: thesis: ex b being Element of (product p) st
( b in B & b <= a )
take b = a; :: thesis: ( b in B & b <= a )
thus b in B by A6, A7; :: thesis: b <= a
[b,a] in id {{}} by A6, A7, RELAT_1:def 10;
hence b <= a by A2, ORDERS_2:def 5; :: thesis: verum
end;
thus B is finite ; :: thesis: verum
end;
end;
end;
thus product p is antisymmetric by YELLOW_1:26; :: thesis: verum