let n be Nat; 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 ; 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; 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; ( 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 that
A1:
f is one-to-one
and
A2:
card n c= card X
and
A3:
not X is empty
and
A4:
not Y is empty
; the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H))
consider f1 being Function such that
A5:
n c= f1 .: X
by A2, CARD_1:66;
f in Funcs (X,Y)
by A4, FUNCT_2:8;
then A6:
ex f9 being Function st
( f = f9 & dom f9 = X & rng f9 c= Y )
by FUNCT_2:def 2;
then
card X c= card Y
by A1, CARD_1:10;
then consider f2 being Function such that
A7:
X c= f2 .: Y
by CARD_1:66;
f1 .: X c= f1 .: (f2 .: Y)
by A7, RELAT_1:123;
then
n c= f1 .: (f2 .: Y)
by A5;
then
n c= (f1 * f2) .: Y
by RELAT_1:126;
then
card n c= card Y
by CARD_1:66;
then
not the_subsets_of_card (n,Y) is empty
by A4, GROUP_10:1;
then
f ||^ n in Funcs ((the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)))
by FUNCT_2:8;
then A8:
ex fn being Function st
( 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 object 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
object ;
( y in the_subsets_of_card (n,(f .: H)) iff y in (f ||^ n) .: (the_subsets_of_card (n,H)) )
hereby ( y in (f ||^ n) .: (the_subsets_of_card (n,H)) implies y in the_subsets_of_card (n,(f .: H)) )
A9:
f .: H c= rng f
by RELAT_1:111;
assume A10:
y in the_subsets_of_card (
n,
(f .: H))
;
y in (f ||^ n) .: (the_subsets_of_card (n,H))then A11:
ex
X9 being
Subset of
(f .: H) st
(
y = X9 &
card X9 = n )
;
ex
x being
set st
(
x in dom (f ||^ n) &
x in the_subsets_of_card (
n,
H) &
y = (f ||^ n) . x )
proof
reconsider yy =
y as
set by TARSKI:1;
set x =
f " yy;
take
f " yy
;
( f " yy in dom (f ||^ n) & f " yy in the_subsets_of_card (n,H) & y = (f ||^ n) . (f " yy) )
A12:
f " yy c= dom f
by RELAT_1:132;
A13:
f .: (f " yy) = y
by A10, A9, FUNCT_1:77, XBOOLE_1:1;
then reconsider x9 =
f " yy as
Subset of
H by A1, A10, A12, FUNCT_1:87;
A14:
card x9 = n
by A11, A13, CARD_1:5, A1, A12, CARD_1:33;
then A15:
f " yy in the_subsets_of_card (
n,
H)
;
A16:
the_subsets_of_card (
n,
H)
c= the_subsets_of_card (
n,
X)
by Lm1;
hence
f " yy in dom (f ||^ n)
by A8, A15;
( f " yy in the_subsets_of_card (n,H) & y = (f ||^ n) . (f " yy) )
thus
f " yy in the_subsets_of_card (
n,
H)
by A14;
y = (f ||^ n) . (f " yy)
thus y =
f .: (f " yy)
by A10, A9, FUNCT_1:77, XBOOLE_1:1
.=
(f ||^ n) . (f " yy)
by A1, A2, A3, A4, A15, A16, Def2A
;
verum
end; hence
y in (f ||^ n) .: (the_subsets_of_card (n,H))
by FUNCT_1:def 6;
verum
end;
assume
y in (f ||^ n) .: (the_subsets_of_card (n,H))
;
y in the_subsets_of_card (n,(f .: H))
then consider x being
object such that A17:
x in dom (f ||^ n)
and A18:
x in the_subsets_of_card (
n,
H)
and A19:
y = (f ||^ n) . x
by FUNCT_1:def 6;
reconsider x =
x as
Element of
the_subsets_of_card (
n,
X)
by A17;
A20:
y = f .: x
by A1, A2, A3, A4, A19, Def2A;
then reconsider X9 =
y as
Subset of
(f .: H) by A18, RELAT_1:123;
( ex
x9 being
Subset of
H st
(
x9 = x &
card x9 = n ) &
x,
f .: x are_equipotent )
by A1, A6, A18, CARD_1:33, XBOOLE_1:1;
then
card X9 = n
by A20, CARD_1:5;
hence
y in the_subsets_of_card (
n,
(f .: H))
;
verum
end;
hence
the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H))
by TARSKI:2; verum