begin
deffunc H1( set ) -> set = $1 `1 ;
Lm1:
for A, B being Ordinal
for x1, x2 being set st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
deffunc H2( set , set ) -> set = [:$1,{0}:] \/ [:$2,{1}:];
Lm2:
for X, Y being set holds
( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] )
theorem Th5:
for
X,
Y,
Z being
set holds
(
[:[:X,Y:],Z:],
[:X,[:Y,Z:]:] are_equipotent &
card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] )
Lm3:
for X, Y being set holds [:X,Y:],[:(card X),Y:] are_equipotent
theorem Th7:
for
X,
Y being
set holds
(
[:X,Y:],
[:(card X),Y:] are_equipotent &
[:X,Y:],
[:X,(card Y):] are_equipotent &
[:X,Y:],
[:(card X),(card Y):] are_equipotent &
card [:X,Y:] = card [:(card X),Y:] &
card [:X,Y:] = card [:X,(card Y):] &
card [:X,Y:] = card [:(card X),(card Y):] )
theorem Th8:
for
X1,
Y1,
X2,
Y2 being
set st
X1,
Y1 are_equipotent &
X2,
Y2 are_equipotent holds
(
[:X1,X2:],
[:Y1,Y2:] are_equipotent &
card [:X1,X2:] = card [:Y1,Y2:] )
deffunc H3( set , set ) -> set = [:$1,{0}:] \/ [:$2,{1}:];
deffunc H4( set , set , set , set ) -> set = [:$1,{$3}:] \/ [:$2,{$4}:];
theorem Th12:
for
X1,
Y1,
X2,
Y2,
x1,
x2,
y1,
y2 being
set st
X1,
Y1 are_equipotent &
X2,
Y2 are_equipotent &
x1 <> x2 &
y1 <> y2 holds
(
[:X1,{x1}:] \/ [:X2,{x2}:],
[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent &
card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) )
theorem
for
X,
Y being
set holds
(
[:X,{0}:] \/ [:Y,{1}:],
[:Y,{0}:] \/ [:X,{1}:] are_equipotent &
card ([:X,{0}:] \/ [:Y,{1}:]) = card ([:Y,{0}:] \/ [:X,{1}:]) )
by Th12;
theorem Th16:
for
X1,
X2,
Y1,
Y2 being
set holds
(
[:X1,X2:] \/ [:Y1,Y2:],
[:X2,X1:] \/ [:Y2,Y1:] are_equipotent &
card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) )
Lm4:
for x, y, X, Y being set st x <> y holds
[:X,{x}:] misses [:Y,{y}:]
theorem Th52:
for
x1,
x2,
x3,
x4 being
set holds
card {x1,x2,x3,x4} <= 4
theorem Th53:
for
x1,
x2,
x3,
x4,
x5 being
set holds
card {x1,x2,x3,x4,x5} <= 5
theorem Th54:
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
card {x1,x2,x3,x4,x5,x6} <= 6
theorem Th55:
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
card {x1,x2,x3,x4,x5,x6,x7} <= 7
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8
theorem Th58:
for
x1,
x2,
x3 being
set st
x1 <> x2 &
x1 <> x3 &
x2 <> x3 holds
card {x1,x2,x3} = 3
theorem Th59:
for
x1,
x2,
x3,
x4 being
set st
x1 <> x2 &
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 &
x3 <> x4 holds
card {x1,x2,x3,x4} = 4
begin
Lm5:
now for n being Element of NAT st ( for Z being finite set st card Z = n & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z ) holds
for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z
let n be
Element of
NAT ;
( ( for Z being finite set st card Z = n & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z ) implies for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union b3 in b3 )assume A1:
for
Z being
finite set st
card Z = n &
Z <> {} & ( for
X,
Y being
set st
X in Z &
Y in Z & not
X c= Y holds
Y c= X ) holds
union Z in Z
;
for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union b3 in b3let Z be
finite set ;
( card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) implies union b2 in b2 )assume that A2:
card Z = n + 1
and A3:
Z <> {}
and A4:
for
X,
Y being
set st
X in Z &
Y in Z & not
X c= Y holds
Y c= X
;
union b2 in b2set y = the
Element of
Z;
per cases
( n = 0 or n <> 0 )
;
suppose A6:
n <> 0
;
union b2 in b2
set Y =
Z \ { the Element of Z};
reconsider Y =
Z \ { the Element of Z} as
finite set ;
{ the Element of Z} c= Z
by A3, ZFMISC_1:31;
then A7:
card Y =
(n + 1) - (card { the Element of Z})
by A2, Th44
.=
(n + 1) - 1
by CARD_1:30
.=
n
;
for
a,
b being
set st
a in Y &
b in Y & not
a c= b holds
b c= a
by A4;
then A8:
union Y in Y
by A1, A6, A7, CARD_1:27;
then A9:
union Y in Z
;
Z = (Z \ { the Element of Z}) \/ { the Element of Z}
then A11:
union Z =
(union Y) \/ (union { the Element of Z})
by ZFMISC_1:78
.=
(union Y) \/ the
Element of
Z
by ZFMISC_1:25
;
A12:
the
Element of
Z in Z
by A3;
( the
Element of
Z c= union Y or
union Y c= the
Element of
Z )
by A4, A8;
hence
union Z in Z
by A9, A12, A11, XBOOLE_1:12;
verum
end;
end;
end;
Lm6:
for Z being finite set st Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z
theorem
for
x1,
x2,
x3,
x4,
x5 being
set st
x1,
x2,
x3,
x4,
x5 are_mutually_different holds
card {x1,x2,x3,x4,x5} = 5
begin
scheme
FinRegularity{
F1()
-> finite set ,
P1[
set ,
set ] } :
ex
x being
set st
(
x in F1() & ( for
y being
set st
y in F1() &
y <> x holds
not
P1[
y,
x] ) )
provided
A1:
F1()
<> {}
and A2:
for
x,
y being
set st
P1[
x,
y] &
P1[
y,
x] holds
x = y
and A3:
for
x,
y,
z being
set st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
scheme
MaxFinSetElem{
F1()
-> finite set ,
P1[
set ,
set ] } :
ex
x being
set st
(
x in F1() & ( for
y being
set st
y in F1() holds
P1[
x,
y] ) )
provided
A1:
F1()
<> {}
and A2:
for
x,
y being
set holds
(
P1[
x,
y] or
P1[
y,
x] )
and A3:
for
x,
y,
z being
set st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
Lm7:
for n being Nat st Rank n is finite holds
Rank (n + 1) is finite
Lm8:
1 = card 1
by CARD_1:def 2;
Lm9:
2 = card 2
by CARD_1:def 2;
Lm10:
omega is limit_ordinal
by ORDINAL1:def 11;
theorem Th92:
for
K,
L,
M,
N being
Cardinal holds
( ( not (
K in L &
M in N ) & not (
K c= L &
M in N ) & not (
K in L &
M c= N ) & not (
K c= L &
M c= N ) ) or
K = 0 or
exp (
K,
M)
c= exp (
L,
N) )