let i be Nat; :: thesis: for X, Y being finite natural-membered set st X <N< Y & i in card X holds
(Sgm0 (X \/ Y)) . i in X
let X, Y be finite natural-membered set ; :: thesis: ( X <N< Y & i in card X implies (Sgm0 (X \/ Y)) . i in X )
assume that
A1: X <N< Y and
A2: i in card X ; :: thesis: (Sgm0 (X \/ Y)) . i in X
set f = (Sgm0 (X \/ Y)) | (card X);
set f0 = Sgm0 (X \/ Y);
set Z = { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ;
A3: rng (Sgm0 (X \/ Y)) = X \/ Y by Def4;
len (Sgm0 (X \/ Y)) = card (X \/ Y) by Th20;
then A4: card X <= len (Sgm0 (X \/ Y)) by NAT_1:43, XBOOLE_1:7;
then A5: len ((Sgm0 (X \/ Y)) | (card X)) = card X by AFINSQ_1:54;
A6: { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } c= rng ((Sgm0 (X \/ Y)) | (card X))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } or y in rng ((Sgm0 (X \/ Y)) | (card X)) )
assume y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ; :: thesis: y in rng ((Sgm0 (X \/ Y)) | (card X))
then ex v0 being Element of X \/ Y st
( y = v0 & ex k2 being Nat st
( v0 = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) ) ;
hence y in rng ((Sgm0 (X \/ Y)) | (card X)) by A5, FUNCT_1:def 3; :: thesis: verum
end;
then reconsider Z0 = { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } as finite set ;
rng ((Sgm0 (X \/ Y)) | (card X)) c= { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Sgm0 (X \/ Y)) | (card X)) or y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } )
assume A7: y in rng ((Sgm0 (X \/ Y)) | (card X)) ; :: thesis: y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) }
then consider x being object such that
A8: x in dom ((Sgm0 (X \/ Y)) | (card X)) and
A9: y = ((Sgm0 (X \/ Y)) | (card X)) . x by FUNCT_1:def 3;
reconsider y0 = y as Element of X \/ Y by A7, Def4;
ex k2 being Nat st
( y0 = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) by A8, A9;
hence y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ; :: thesis: verum
end;
then A10: rng ((Sgm0 (X \/ Y)) | (card X)) = { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } by A6;
A11: X \/ Y <> {} by A2, CARD_1:27, XBOOLE_1:15;
A12: now :: thesis: ( not { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } c= X implies X c= { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } )
assume that
A13: not { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } c= X and
A14: not X c= { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ; :: thesis: contradiction
consider v1 being object such that
A15: v1 in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } and
A16: not v1 in X by A13;
consider v10 being Element of X \/ Y such that
A17: v1 = v10 and
A18: ex k2 being Nat st
( v10 = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) by A15;
A19: v10 in Y by A11, A16, A17, XBOOLE_0:def 3;
reconsider nv10 = v10 as Nat ;
consider v2 being object such that
A20: v2 in X and
A21: not v2 in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } by A14;
X c= X \/ Y by XBOOLE_1:7;
then consider x2 being object such that
A22: x2 in dom (Sgm0 (X \/ Y)) and
A23: v2 = (Sgm0 (X \/ Y)) . x2 by A3, A20, FUNCT_1:def 3;
reconsider x20 = x2 as Nat by A22;
now :: thesis: not x20 < card X
assume x20 < card X ; :: thesis: contradiction
then A24: x20 in Segm (card X) by NAT_1:44;
card X <= card (X \/ Y) by NAT_1:43, XBOOLE_1:7;
then card X <= len (Sgm0 (X \/ Y)) by Th20;
then ((Sgm0 (X \/ Y)) | (card X)) . x20 = (Sgm0 (X \/ Y)) . x20 by A24, AFINSQ_1:53;
hence contradiction by A5, A10, A21, A23, A24, FUNCT_1:def 3; :: thesis: verum
end;
then A25: len ((Sgm0 (X \/ Y)) | (card X)) <= x20 by A4, AFINSQ_1:54;
consider k20 being Nat such that
A26: v10 = ((Sgm0 (X \/ Y)) | (card X)) . k20 and
A27: k20 in card X by A18;
A28: ((Sgm0 (X \/ Y)) | (card X)) . k20 = (Sgm0 (X \/ Y)) . k20 by A4, A27, AFINSQ_1:53;
reconsider nv2 = v2 as Nat by A23;
k20 < len ((Sgm0 (X \/ Y)) | (card X)) by A5, A27, AFINSQ_1:86;
then A29: k20 < x20 by A25, XXREAL_0:2;
x20 < len (Sgm0 (X \/ Y)) by A22, AFINSQ_1:86;
then nv10 < nv2 by A26, A23, A29, A28, Def4;
hence contradiction by A1, A20, A19; :: thesis: verum
end;
(Sgm0 (X \/ Y)) | (card X) is one-to-one by FUNCT_1:52;
then A30: dom ((Sgm0 (X \/ Y)) | (card X)),((Sgm0 (X \/ Y)) | (card X)) .: (dom ((Sgm0 (X \/ Y)) | (card X))) are_equipotent by CARD_1:33;
((Sgm0 (X \/ Y)) | (card X)) .: (dom ((Sgm0 (X \/ Y)) | (card X))) = rng ((Sgm0 (X \/ Y)) | (card X)) by RELAT_1:113;
then A31: card { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } = card (len ((Sgm0 (X \/ Y)) | (card X))) by A10, A30, CARD_1:5;
then A32: card { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } = card X by A4, AFINSQ_1:54;
A33: now :: thesis: ( ( Z0 c= X & Z0 = X ) or ( X c= Z0 & Z0 = X ) )
per cases ( Z0 c= X or X c= Z0 ) by A12;
case X c= Z0 ; :: thesis: Z0 = X
hence Z0 = X by A32, CARD_2:102; :: thesis: verum
end;
end;
end;
((Sgm0 (X \/ Y)) | (card X)) . i = (Sgm0 (X \/ Y)) . i by A2, A4, AFINSQ_1:53;
hence (Sgm0 (X \/ Y)) . i in X by A2, A5, A10, A33, FUNCT_1:def 3; :: thesis: verum