let n be natural number ; :: thesis: for X, Y being set
for f being Function of X,Y
for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
the_subsets_of_card n,(f .: H) = (f ||^ n) .: (the_subsets_of_card n,H)
let X, Y be set ; :: thesis: for f being Function of X,Y
for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
the_subsets_of_card n,(f .: H) = (f ||^ n) .: (the_subsets_of_card n,H)
let f be Function of X,Y; :: thesis: for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
the_subsets_of_card n,(f .: H) = (f ||^ n) .: (the_subsets_of_card n,H)
let H be Subset of X; :: thesis: ( f is one-to-one & card n c= card X & not X is empty & not Y is empty implies the_subsets_of_card n,(f .: H) = (f ||^ n) .: (the_subsets_of_card n,H) )
assume A1:
( f is one-to-one & card n c= card X & not X is empty & not Y is empty )
; :: thesis: the_subsets_of_card n,(f .: H) = (f ||^ n) .: (the_subsets_of_card n,H)
then
f in Funcs X,Y
by FUNCT_2:11;
then consider f' being Function such that
A2:
( f = f' & dom f' = X & rng f' c= Y )
by FUNCT_2:def 2;
A3:
card X c= card Y
by A2, A1, CARD_1:26;
consider f1 being Function such that
A4:
n c= f1 .: X
by A1, CARD_2:2;
consider f2 being Function such that
A5:
X c= f2 .: Y
by A3, CARD_2:2;
f1 .: X c= f1 .: (f2 .: Y)
by A5, RELAT_1:156;
then
n c= f1 .: (f2 .: Y)
by A4, XBOOLE_1:1;
then
n c= (f1 * f2) .: Y
by RELAT_1:159;
then
card n c= card Y
by CARD_2:2;
then
not the_subsets_of_card n,Y is empty
by A1, GROUP_10:2;
then
f ||^ n in Funcs (the_subsets_of_card n,X),(the_subsets_of_card n,Y)
by FUNCT_2:11;
then consider fn being Function such that
A6:
( f ||^ n = fn & dom fn = the_subsets_of_card n,X & rng fn c= the_subsets_of_card n,Y )
by FUNCT_2:def 2;
for y being set holds
( y in the_subsets_of_card n,(f .: H) iff y in (f ||^ n) .: (the_subsets_of_card n,H) )
proof
let y be
set ;
:: thesis: ( y in the_subsets_of_card n,(f .: H) iff y in (f ||^ n) .: (the_subsets_of_card n,H) )
hereby :: thesis: ( y in (f ||^ n) .: (the_subsets_of_card n,H) implies y in the_subsets_of_card n,(f .: H) )
assume
y in the_subsets_of_card n,
(f .: H)
;
:: thesis: y in (f ||^ n) .: (the_subsets_of_card n,H)then consider X' being
Subset of
(f .: H) such that A7:
(
y = X' &
card X' = n )
;
A8:
f .: H c= rng f
by RELAT_1:144;
ex
x being
set st
(
x in dom (f ||^ n) &
x in the_subsets_of_card n,
H &
y = (f ||^ n) . x )
proof
set x =
f " y;
A9:
f .: (f " y) = y
by A8, A7, FUNCT_1:147, XBOOLE_1:1;
take
f " y
;
:: thesis: ( f " y in dom (f ||^ n) & f " y in the_subsets_of_card n,H & y = (f ||^ n) . (f " y) )
A10:
f " y c= dom f
by RELAT_1:167;
reconsider x' =
f " y as
Subset of
H by A9, A7, A10, A1, FUNCT_1:157;
f " y,
f .: (f " y) are_equipotent
by A10, A1, CARD_1:60;
then A11:
card x' = n
by A7, A9, CARD_1:21;
then A12:
f " y in the_subsets_of_card n,
H
;
A13:
the_subsets_of_card n,
H c= the_subsets_of_card n,
X
by Lm1;
thus
f " y in dom (f ||^ n)
by A6, A13, A12;
:: thesis: ( f " y in the_subsets_of_card n,H & y = (f ||^ n) . (f " y) )
thus
f " y in the_subsets_of_card n,
H
by A11;
:: thesis: y = (f ||^ n) . (f " y)
thus y =
f .: (f " y)
by A8, A7, FUNCT_1:147, XBOOLE_1:1
.=
(f ||^ n) . (f " y)
by A1, A13, A12, Def2
;
:: thesis: verum
end; hence
y in (f ||^ n) .: (the_subsets_of_card n,H)
by FUNCT_1:def 12;
:: thesis: verum
end;
assume
y in (f ||^ n) .: (the_subsets_of_card n,H)
;
:: thesis: y in the_subsets_of_card n,(f .: H)
then consider x being
set such that A14:
(
x in dom (f ||^ n) &
x in the_subsets_of_card n,
H &
y = (f ||^ n) . x )
by FUNCT_1:def 12;
reconsider x =
x as
Element of
the_subsets_of_card n,
X by A14;
A15:
y = f .: x
by A14, A1, Def2;
consider x' being
Subset of
H such that A16:
(
x' = x &
card x' = n )
by A14;
reconsider X' =
y as
Subset of
(f .: H) by A15, A16, RELAT_1:156;
x,
f .: x are_equipotent
by A1, A2, A16, CARD_1:60, XBOOLE_1:1;
then
card X' = n
by A16, A15, CARD_1:21;
hence
y in the_subsets_of_card n,
(f .: H)
;
:: thesis: verum
end;
hence
the_subsets_of_card n,(f .: H) = (f ||^ n) .: (the_subsets_of_card n,H)
by TARSKI:2; :: thesis: verum