defpred S1[ Nat] means for X being finite set st card X = $1 & X is Subset of F1() & ex x being Element of F1() st
( x in X & P1[x] ) holds
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) );
A2:
S1[ 0 ]
;
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
let X be
finite set ;
( card X = k + 1 & X is Subset of F1() & ex x being Element of F1() st
( x in X & P1[x] ) implies ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) ) )
assume that A5:
card X = k + 1
and A6:
X is
Subset of
F1()
;
( for x being Element of F1() holds
( not x in X or not P1[x] ) or ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) ) )
given x being
Element of
F1()
such that A7:
x in X
and A8:
P1[
x]
;
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )
set Xmx =
X \ {x};
reconsider Xmx =
X \ {x} as
Subset of
F1()
by A6, XBOOLE_1:1;
A9:
card Xmx =
(card X) - (card {x})
by A7, ZFMISC_1:31, CARD_2:44
.=
(card X) - 1
by CARD_1:30
.=
k
by A5
;
A10:
Xmx \/ {x} = X
by A7, ZFMISC_1:116;
per cases
( ex z being Element of F1() st
( z in Xmx & P1[z] ) or for z being Element of F1() st z in Xmx holds
not P1[z] )
;
suppose
ex
z being
Element of
F1() st
(
z in Xmx &
P1[
z] )
;
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )then consider z being
Element of
F1()
such that A11:
z in Xmx
and A12:
P1[
z]
and A13:
for
y being
Element of
F1() st
y in Xmx &
y <~ z holds
not
P1[
y]
by A4, A9;
per cases
( not x <~ z or x <~ z )
;
suppose A14:
not
x <~ z
;
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )take
z
;
( z in X & P1[z] & ( for y being Element of F1() st y in X & y <~ z holds
not P1[y] ) )thus
z in X
by A11;
( P1[z] & ( for y being Element of F1() st y in X & y <~ z holds
not P1[y] ) )thus
P1[
z]
by A12;
for y being Element of F1() st y in X & y <~ z holds
not P1[y]hereby verum
let y be
Element of
F1();
( y in X & y <~ z implies not P1[b1] )assume that A15:
y in X
and A16:
y <~ z
;
P1[b1]
end; end; suppose A17:
x <~ z
;
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )set Xmz =
X \ {z};
reconsider Xmz =
X \ {z} as
Subset of
F1()
by A6, XBOOLE_1:1;
A18:
Xmz \/ {z} = X
by A11, ZFMISC_1:116;
A19:
card Xmz =
(card X) - (card {z})
by A11, ZFMISC_1:31, CARD_2:44
.=
(card X) - 1
by CARD_1:30
.=
k
by A5
;
A20:
x in Xmz
by A7, A17, ZFMISC_1:56;
then consider v being
Element of
F1()
such that A21:
v in Xmz
and A22:
P1[
v]
and A23:
for
y being
Element of
F1() st
y in Xmz &
y <~ v holds
not
P1[
y]
by A19, A4, A8;
per cases
( v = x or v <> x )
;
suppose A24:
v = x
;
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )take
v
;
( v in X & P1[v] & ( for y being Element of F1() st y in X & y <~ v holds
not P1[y] ) )thus
v in X
by A21;
( P1[v] & ( for y being Element of F1() st y in X & y <~ v holds
not P1[y] ) )thus
P1[
v]
by A22;
for y being Element of F1() st y in X & y <~ v holds
not P1[y]hereby verum
let y be
Element of
F1();
( y in X & y <~ v implies not P1[b1] )assume that A25:
y in X
and A26:
y <~ v
;
P1[b1]
end; end; suppose A27:
v <> x
;
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )A28:
not
F1() is
empty
by A6, A7;
not
x <~ v
by A20, A8, A23;
per cases then
( v <~ x or v =~ x )
by A27, A28, Th27;
suppose A29:
v <~ x
;
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )take
v
;
( v in X & P1[v] & ( for y being Element of F1() st y in X & y <~ v holds
not P1[y] ) )thus
v in X
by A21;
( P1[v] & ( for y being Element of F1() st y in X & y <~ v holds
not P1[y] ) )thus
P1[
v]
by A22;
for y being Element of F1() st y in X & y <~ v holds
not P1[y]hereby verum
let y be
Element of
F1();
( y in X & y <~ v implies not P1[b1] )assume that A30:
y in X
and A31:
y <~ v
;
P1[b1]
end; end; suppose A32:
v =~ x
;
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )take
x
;
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )thus
x in X
by A7;
( P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )thus
P1[
x]
by A8;
for y being Element of F1() st y in X & y <~ x holds
not P1[y]hereby verum
let y be
Element of
F1();
( y in X & y <~ x implies not P1[b1] )assume that A33:
y in X
and A34:
y <~ x
;
P1[b1]
end; end; end; end; end; end; end; end; suppose A37:
for
z being
Element of
F1() st
z in Xmx holds
not
P1[
z]
;
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )take
x
;
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )thus
x in X
by A7;
( P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )thus
P1[
x]
by A8;
for y being Element of F1() st y in X & y <~ x holds
not P1[y]hereby verum
let y be
Element of
F1();
( y in X & y <~ x implies not P1[b1] )assume that A38:
y in X
and A39:
y <~ x
;
P1[b1]
end; end; end;
end;
A40:
for k being Nat holds S1[k]
from NAT_1:sch 2(A2, A3);
reconsider c = card F2() as Nat ;
S1[c]
by A40;
hence
ex x being Element of F1() st
( x in F2() & P1[x] & ( for y being Element of F1() st y in F2() & y <~ x holds
not P1[y] ) )
by A1; verum