environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, FUNCT_1, SUBSET_1, EQREL_1, GROUP_10, TARSKI, FINSET_1, XBOOLE_0, CARD_1, RELAT_1, FUNCT_2, ARYTM_1, ARYTM_3, XXREAL_0, NAT_1, FINSEQ_1, CARD_3, RAMSEY_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XXREAL_0, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, CARD_1, ORDINAL1, NAT_1, NUMBERS, PARTFUN1, EQREL_1, FINSET_1, FUNCT_2, GROUP_10, NEWTON, NAT_D;
definitions TARSKI;
theorems TARSKI, XBOOLE_0, XBOOLE_1, EQREL_1, CARD_1, WELLORD2, FUNCT_1, FUNCT_2, RELAT_1, GROUP_10, ZFMISC_1, CARD_2, NAT_1, XREAL_1, ORDINAL1, XXREAL_0, STIRL2_1, WAYBEL12, CARD_FIL, FINSEQ_1, NEWTON, ENUMSET1, NAT_D, XREAL_0, CARD_3;
schemes NAT_1, FUNCT_1, FUNCT_2, RECDEF_2;
registrations XBOOLE_0, SUBSET_1, XXREAL_0, XREAL_0, FINSEQ_1, RELAT_1, ORDINAL1, EQREL_1, CARD_3, NAT_1, CARD_1, MEMBERED, FINSET_1, FUNCT_1, FUNCT_2, RELSET_1;
constructors HIDDEN, WELLORD2, GROUP_10, NEWTON, NAT_D, REAL_1, RVSUM_1, CARD_5, RELSET_1, NUMBERS, EQREL_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities GROUP_10, ORDINAL1, CARD_1;
expansions TARSKI;
definition
let n be
Nat;
let X,
Y be
set ;
let f be
Function of
X,
Y;
assume that A1:
f is
one-to-one
and A2:
(
card n c= card X & not
X is
empty )
and A3:
not
Y is
empty
;
existence
ex b1 being Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) st
for x being Element of the_subsets_of_card (n,X) holds b1 . x = f .: x
uniqueness
for b1, b2 being Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) st ( for x being Element of the_subsets_of_card (n,X) holds b1 . x = f .: x ) & ( for x being Element of the_subsets_of_card (n,X) holds b2 . x = f .: x ) holds
b1 = b2
end;
Lm1:
for X, Y, Z being set st X c= Y holds
the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y)
Lm2:
for X being set holds the_subsets_of_card (0,X) = {0}
Lm3:
for X, Y being finite set st card Y = X holds
the_subsets_of_card (X,Y) = {Y}
Lm4:
for n, k being Nat
for X being set
for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds
ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card (n,H)) is constant )
scheme
BinInd2{
P1[
Nat,
Nat] } :
for
n,
m being
Nat holds
P1[
m,
n]
provided
A1:
for
n being
Nat holds
(
P1[
0 ,
n] &
P1[
n,
0 ] )
and A2:
for
n,
m being
Nat st
P1[
m + 1,
n] &
P1[
m,
n + 1] holds
P1[
m + 1,
n + 1]
::