defpred S1[ Nat] means for X being finite set st card X = $1 & X <> {} holds
ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) );
A4:
S1[ 0 ]
;
A5:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A6:
for
X being
finite set st
card X = n &
X <> {} holds
ex
x being
object st
(
x in X & ( for
y being
object st
y in X holds
P1[
x,
y] ) )
;
S1[n + 1]
let X be
finite set ;
( card X = n + 1 & X <> {} implies ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) ) )
assume that A7:
card X = n + 1
and A8:
X <> {}
;
ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) )
set x = the
Element of
X;
now ( X \ { the Element of X} <> {} implies ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) ) )assume A11:
X \ { the Element of X} <> {}
;
ex x being object st
( x in X & ( for y being object st y in X holds
P1[x,y] ) )
{ the Element of X} c= X
by A8, ZFMISC_1:31;
then A12:
card (X \ { the Element of X}) = (n + 1) - (card { the Element of X})
by A7, Th43;
card { the Element of X} = 1
by CARD_1:30;
then consider y being
object such that A13:
y in X \ { the Element of X}
and A14:
for
z being
object st
z in X \ { the Element of X} holds
P1[
y,
z]
by A6, A11, A12;
A15:
(
P1[ the
Element of
X,
y] or
P1[
y, the
Element of
X] )
by A2;
A16:
P1[ the
Element of
X, the
Element of
X]
by A2;
P1[
y,
y]
by A2;
then consider z being
object such that A17:
(
z = the
Element of
X or
z = y )
and A18:
P1[
z, the
Element of
X]
and A19:
P1[
z,
y]
by A15, A16;
thus
ex
x being
object st
(
x in X & ( for
y being
object st
y in X holds
P1[
x,
y] ) )
verumproof
take
z
;
( z in X & ( for y being object st y in X holds
P1[z,y] ) )
thus
z in X
by A13, A17;
for y being object st y in X holds
P1[z,y]
let u be
object ;
( u in X implies P1[z,u] )
A20:
(
u in { the Element of X} or not
u in { the Element of X} )
;
assume
u in X
;
P1[z,u]
then
(
u = the
Element of
X or
u in X \ { the Element of X} )
by A20, TARSKI:def 1, XBOOLE_0:def 5;
then
(
P1[
z,
u] or
P1[
y,
u] )
by A14, A18;
hence
P1[
z,
u]
by A3, A19;
verum
end; end;
hence
ex
x being
object st
(
x in X & ( for
y being
object st
y in X holds
P1[
x,
y] ) )
by A9;
verum
end;
A21:
for n being Nat holds S1[n]
from NAT_1:sch 2(A4, A5);
card F1() = card F1()
;
hence
ex x being object st
( x in F1() & ( for y being object st y in F1() holds
P1[x,y] ) )
by A1, A21; verum