let F be finite set ; :: thesis: for A being FinSequence of bool F st ex X being set st X is_a_system_of_different_representatives_of A holds
A is Hall
let A be FinSequence of bool F; :: thesis: ( ex X being set st X is_a_system_of_different_representatives_of A implies A is Hall )
given X being set such that A1:
X is_a_system_of_different_representatives_of A
; :: thesis: A is Hall
consider f being FinSequence of F such that
f = X
and
A2:
dom A = dom f
and
A3:
for i being Element of NAT st i in dom f holds
f . i in A . i
and
A4:
f is one-to-one
by A1, Def3;
for J being finite set st J c= dom A holds
card J <= card (union A,J)
proof
let J be
finite set ;
:: thesis: ( J c= dom A implies card J <= card (union A,J) )
assume A5:
J c= dom A
;
:: thesis: card J <= card (union A,J)
set X =
J;
set Y =
union A,
J;
set g =
f | J;
A6:
f | J is
one-to-one
by A4, FUNCT_1:84;
A7:
dom (f | J) = J
by A2, A5, RELAT_1:91;
A8:
(
dom (f | J) c= dom f &
rng (f | J) c= rng f )
by RELAT_1:89, RELAT_1:99;
rng (f | J) c= union A,
J
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng (f | J) or x in union A,J )
assume
x in rng (f | J)
;
:: thesis: x in union A,J
then consider a being
set such that A9:
(
a in dom (f | J) &
x = (f | J) . a )
by FUNCT_1:def 5;
a in dom f
by A8, A9;
then reconsider a =
a as
Element of
NAT ;
f . a in A . a
by A2, A3, A5, A7, A9;
then
(f | J) . a in A . a
by A9, FUNCT_1:70;
hence
x in union A,
J
by A5, A7, A9, Def1;
:: thesis: verum
end;
then
card J c= card (union A,J)
by A6, A7, CARD_1:26;
hence
card J <= card (union A,J)
by NAT_1:40;
:: thesis: verum
end;
hence
A is Hall
by Def4; :: thesis: verum