environ
vocabularies HIDDEN, FINSET_1, CARD_1, XBOOLE_0, SUBSET_1, CARD_5, SETFAM_1, TARSKI, ZFMISC_1, ORDINAL1, CARD_2, FUNCT_1, RELAT_1, ORDINAL2, FUNCT_2, CARD_3, FUNCOP_1, FUNCT_5, CARD_FIL;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, BINOP_1, FUNCT_5, SETFAM_1, FINSET_1, ORDINAL1, CARD_1, RELSET_1, FUNCT_2, ORDINAL2, CARD_2, CARD_3, CARD_5;
definitions TARSKI, FUNCT_1, CARD_1, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, WELLORD2, CARD_1, CARD_2, CARD_5, SETFAM_1, ZFMISC_1, FUNCT_5, RELAT_1, SUBSET_1, FUNCOP_1, SETWISEO, RELSET_1, FRAENKEL, ORDERS_1, XBOOLE_0, XBOOLE_1, ORDINAL3, CARD_3;
schemes FUNCT_1, FUNCT_2, DOMAIN_1, FRAENKEL, TREES_2, BINOP_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, CARD_1, CARD_5, CARD_2;
constructors HIDDEN, SETFAM_1, WELLORD2, BINOP_1, FUNCOP_1, ORDINAL2, FUNCT_5, CARD_2, CARD_5, NUMBERS, RELSET_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities BINOP_1, SUBSET_1, ORDINAL1;
expansions TARSKI, FUNCT_1, CARD_1, XBOOLE_0, ORDINAL1;
::
deftheorem defines
is_Ulam_Matrix_of CARD_FIL:def 18 :
for M being non limit_cardinal Aleph
for T being Inf_Matrix of (predecessor M),M,(bool M) holds
( T is_Ulam_Matrix_of M iff ( ( for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty ) & ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ) & ( for N1 being Element of predecessor M holds card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ) ) );