defpred S1[ object , object ] means ( ( $1 = VERUM implies $2 = F1() ) & ( for n being Element of NAT st $1 = prop n holds
$2 = F2(n) ) );
set Pn = { (prop n) where n is Element of NAT : verum } ;
set X = { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } ;
A5:
{ (prop n) where n is Element of NAT : verum } c= HP-WFF
{VERUM} c= HP-WFF
by ZFMISC_1:31;
then reconsider Y0 = { (prop n) where n is Element of NAT : verum } \/ {VERUM} as Subset of HP-WFF by A5, XBOOLE_1:8;
A6:
for x being object st x in Y0 holds
ex y being object st S1[x,y]
consider M0 being ManySortedSet of Y0 such that
A10:
for x being object st x in Y0 holds
S1[x,M0 . x]
from PBOOLE:sch 3(A6);
A11:
for p, q being Element of HP-WFF holds
( not p '&' q in Y0 & not p => q in Y0 )
then A13:
( ( for p, q being Element of HP-WFF st ( p '&' q in Y0 or p => q in Y0 ) holds
( p in Y0 & q in Y0 ) ) & ( for p, q being Element of HP-WFF st p '&' q in Y0 holds
for x, y, z being set st x = M0 . p & y = M0 . q & z = M0 . (p '&' q) holds
P1[p,q,x,y,z] ) )
;
A14:
for n being Element of NAT holds prop n in Y0
A15:
for n being Element of NAT holds M0 . (prop n) = F2(n)
VERUM in {VERUM}
by TARSKI:def 1;
then A16:
VERUM in Y0
by XBOOLE_0:def 3;
A17:
for Z being set st Z <> {} & Z c= { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } & Z is c=-linear holds
union Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
proof
defpred S2[
object ,
object ]
means ex
D1 being
set ex
M being
ManySortedSet of
D1 st
(
D1 = $1 &
M = $2 &
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in D1 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in D1 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) );
let Z be
set ;
( Z <> {} & Z c= { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } & Z is c=-linear implies union Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } )
assume that A18:
Z <> {}
and A19:
Z c= { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
and A20:
Z is
c=-linear
;
union Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
A21:
{ Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } c= bool HP-WFF
proof
let x be
object ;
TARSKI:def 3 ( not x in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } or x in bool HP-WFF )
assume
x in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
;
x in bool HP-WFF
then
ex
Y being
Subset of
HP-WFF st
(
x = Y &
VERUM in Y & ( for
n being
Element of
NAT holds
prop n in Y ) & ( for
p,
q being
Element of
HP-WFF st (
p '&' q in Y or
p => q in Y ) holds
(
p in Y &
q in Y ) ) & ex
M being
ManySortedSet of
Y st
(
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) ) )
;
hence
x in bool HP-WFF
;
verum
end;
then reconsider uZ =
union Z as
Subset of
HP-WFF by A19, EQREL_1:61;
consider Z0 being
object such that A22:
Z0 in Z
by A18, XBOOLE_0:def 1;
reconsider Z0 =
Z0 as
set by TARSKI:1;
A23:
for
x being
object st
x in Z holds
ex
y being
object st
S2[
x,
y]
proof
let x be
object ;
( x in Z implies ex y being object st S2[x,y] )
assume
x in Z
;
ex y being object st S2[x,y]
then
x in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A19;
then consider Y being
Subset of
HP-WFF such that A24:
Y = x
and
VERUM in Y
and
for
n being
Element of
NAT holds
prop n in Y
and
for
p,
q being
Element of
HP-WFF st (
p '&' q in Y or
p => q in Y ) holds
(
p in Y &
q in Y )
and A25:
ex
M being
ManySortedSet of
Y st
(
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) )
;
consider M being
ManySortedSet of
Y such that A26:
(
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) )
by A25;
take
M
;
S2[x,M]
thus
S2[
x,
M]
by A24, A26;
verum
end;
consider MM being
ManySortedSet of
Z such that A27:
for
x being
object st
x in Z holds
S2[
x,
MM . x]
from PBOOLE:sch 3(A23);
rng MM is
functional
then reconsider rr =
rng MM as
functional set ;
A30:
for
f,
g being
Function st
f in rr &
g in rr &
dom f c= dom g holds
f tolerates g
proof
let f,
g be
Function;
( f in rr & g in rr & dom f c= dom g implies f tolerates g )
assume
f in rr
;
( not g in rr or not dom f c= dom g or f tolerates g )
then consider x1 being
object such that A31:
x1 in dom MM
and A32:
f = MM . x1
by FUNCT_1:def 3;
reconsider x1 =
x1 as
set by TARSKI:1;
A33:
x1 in Z
by A31, PARTFUN1:def 2;
then
S2[
x1,
MM . x1]
by A27;
then A34:
ex
M being
ManySortedSet of
x1 st
(
M = f &
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in x1 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in x1 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) )
by A32;
then A35:
x1 = dom f
by PARTFUN1:def 2;
assume
g in rr
;
( not dom f c= dom g or f tolerates g )
then consider x2 being
object such that A36:
x2 in dom MM
and A37:
g = MM . x2
by FUNCT_1:def 3;
reconsider x2 =
x2 as
set by TARSKI:1;
defpred S3[
Element of
HP-WFF ]
means ( $1
in x1 implies
f . $1
= g . $1 );
assume A38:
dom f c= dom g
;
f tolerates g
x2 in Z
by A36, PARTFUN1:def 2;
then
S2[
x2,
MM . x2]
by A27;
then A39:
ex
M being
ManySortedSet of
x2 st
(
M = g &
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in x2 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in x2 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) )
by A37;
A40:
for
n being
Element of
NAT holds
S3[
prop n]
A41:
x1 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A19, A33;
A42:
for
r,
s being
Element of
HP-WFF st
S3[
r] &
S3[
s] holds
(
S3[
r '&' s] &
S3[
r => s] )
proof
A43:
( ex
Y being
Subset of
HP-WFF st
(
Y = x1 &
VERUM in Y & ( for
n being
Element of
NAT holds
prop n in Y ) & ( for
p,
q being
Element of
HP-WFF st (
p '&' q in Y or
p => q in Y ) holds
(
p in Y &
q in Y ) ) & ex
M being
ManySortedSet of
Y st
(
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) ) ) &
x1 c= x2 )
by A39, A38, A35, A41, PARTFUN1:def 2;
let r,
s be
Element of
HP-WFF ;
( S3[r] & S3[s] implies ( S3[r '&' s] & S3[r => s] ) )
assume A44:
( (
r in x1 implies
f . r = g . r ) & (
s in x1 implies
f . s = g . s ) )
;
( S3[r '&' s] & S3[r => s] )
thus
(
r '&' s in x1 implies
f . (r '&' s) = g . (r '&' s) )
S3[r => s]proof
assume
r '&' s in x1
;
f . (r '&' s) = g . (r '&' s)
then
(
P1[
r,
s,
g . r,
g . s,
f . (r '&' s)] &
P1[
r,
s,
g . r,
g . s,
g . (r '&' s)] )
by A34, A39, A44, A43;
hence
f . (r '&' s) = g . (r '&' s)
by A3;
verum
end;
thus
(
r => s in x1 implies
f . (r => s) = g . (r => s) )
verumproof
assume
r => s in x1
;
f . (r => s) = g . (r => s)
then
(
P2[
r,
s,
g . r,
g . s,
f . (r => s)] &
P2[
r,
s,
g . r,
g . s,
g . (r => s)] )
by A34, A39, A44, A43;
hence
f . (r => s) = g . (r => s)
by A4;
verum
end;
end;
let x be
object ;
PARTFUN1:def 4 ( not x in (dom f) /\ (dom g) or f . x = g . x )
assume
x in (dom f) /\ (dom g)
;
f . x = g . x
then A45:
x in x1
by A38, A35, XBOOLE_1:28;
A46:
S3[
VERUM ]
by A34, A39;
for
p being
Element of
HP-WFF holds
S3[
p]
from HILBERT2:sch 2(A46, A40, A42);
hence
f . x = g . x
by A21, A45, A41;
verum
end;
for
f,
g being
Function st
f in rr &
g in rr holds
f tolerates g
proof
let f,
g be
Function;
( f in rr & g in rr implies f tolerates g )
assume A47:
f in rr
;
( not g in rr or f tolerates g )
then consider x1 being
object such that A48:
x1 in dom MM
and A49:
f = MM . x1
by FUNCT_1:def 3;
reconsider x1 =
x1 as
set by TARSKI:1;
A50:
x1 in Z
by A48, PARTFUN1:def 2;
then
S2[
x1,
MM . x1]
by A27;
then
ex
M being
ManySortedSet of
x1 st
(
M = f &
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in x1 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in x1 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) )
by A49;
then A51:
x1 = dom f
by PARTFUN1:def 2;
assume A52:
g in rr
;
f tolerates g
then consider x2 being
object such that A53:
x2 in dom MM
and A54:
g = MM . x2
by FUNCT_1:def 3;
reconsider x2 =
x2 as
set by TARSKI:1;
A55:
x2 in Z
by A53, PARTFUN1:def 2;
then
x1,
x2 are_c=-comparable
by A20, A50, ORDINAL1:def 8;
then A56:
(
x1 c= x2 or
x2 c= x1 )
by XBOOLE_0:def 9;
S2[
x2,
MM . x2]
by A27, A55;
then
ex
M being
ManySortedSet of
x2 st
(
M = g &
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in x2 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in x2 holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) )
by A54;
then
x2 = dom g
by PARTFUN1:def 2;
hence
f tolerates g
by A30, A47, A52, A51, A56;
verum
end;
then
union rr is
Function
by WELLFND1:1;
then reconsider M =
Union MM as
Function by CARD_3:def 4;
for
x being
set st
x in Z holds
MM . x is
ManySortedSet of
x
then
dom M = uZ
by Th1;
then reconsider M =
M as
ManySortedSet of
uZ by PARTFUN1:def 2, RELAT_1:def 18;
A57:
M = union rr
by CARD_3:def 4;
A58:
for
p,
q being
Element of
HP-WFF st
p '&' q in uZ holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z]
proof
let p,
q be
Element of
HP-WFF ;
( p '&' q in uZ implies for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] )
assume
p '&' q in uZ
;
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z]
then consider Z1 being
set such that A59:
p '&' q in Z1
and A60:
Z1 in Z
by TARSKI:def 4;
Z1 in dom MM
by A60, PARTFUN1:def 2;
then
MM . Z1 in rr
by FUNCT_1:def 3;
then A61:
MM . Z1 c= M
by A57, ZFMISC_1:74;
let x,
y,
z be
set ;
( x = M . p & y = M . q & z = M . (p '&' q) implies P1[p,q,x,y,z] )
assume that A62:
x = M . p
and A63:
y = M . q
and A64:
z = M . (p '&' q)
;
P1[p,q,x,y,z]
S2[
Z1,
MM . Z1]
by A27, A60;
then consider MZ1 being
ManySortedSet of
Z1 such that A65:
MZ1 = MM . Z1
and
MZ1 . VERUM = F1()
and
for
n being
Element of
NAT holds
MZ1 . (prop n) = F2(
n)
and A66:
for
p,
q being
Element of
HP-WFF st
p '&' q in Z1 holds
for
x,
y,
z being
set st
x = MZ1 . p &
y = MZ1 . q &
z = MZ1 . (p '&' q) holds
P1[
p,
q,
x,
y,
z]
and
for
p,
q being
Element of
HP-WFF st
p => q in Z1 holds
for
x,
y,
z being
set st
x = MZ1 . p &
y = MZ1 . q &
z = MZ1 . (p => q) holds
P2[
p,
q,
x,
y,
z]
;
p '&' q in dom MZ1
by A59, PARTFUN1:def 2;
then A67:
z = MZ1 . (p '&' q)
by A65, A61, A64, GRFUNC_1:2;
Z1 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A19, A60;
then A68:
ex
Y being
Subset of
HP-WFF st
(
Z1 = Y &
VERUM in Y & ( for
n being
Element of
NAT holds
prop n in Y ) & ( for
p,
q being
Element of
HP-WFF st (
p '&' q in Y or
p => q in Y ) holds
(
p in Y &
q in Y ) ) & ex
M being
ManySortedSet of
Y st
(
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) ) )
;
then
q in Z1
by A59;
then
q in dom MZ1
by PARTFUN1:def 2;
then A69:
y = MZ1 . q
by A65, A61, A63, GRFUNC_1:2;
p in Z1
by A59, A68;
then
p in dom MZ1
by PARTFUN1:def 2;
then
x = MZ1 . p
by A65, A61, A62, GRFUNC_1:2;
hence
P1[
p,
q,
x,
y,
z]
by A59, A66, A69, A67;
verum
end;
Z0 in dom MM
by A22, PARTFUN1:def 2;
then
MM . Z0 in rr
by FUNCT_1:def 3;
then A70:
MM . Z0 c= M
by A57, ZFMISC_1:74;
S2[
Z0,
MM . Z0]
by A27, A22;
then consider MZ0 being
ManySortedSet of
Z0 such that A71:
MZ0 = MM . Z0
and A72:
MZ0 . VERUM = F1()
and A73:
for
n being
Element of
NAT holds
MZ0 . (prop n) = F2(
n)
and
for
p,
q being
Element of
HP-WFF st
p '&' q in Z0 holds
for
x,
y,
z being
set st
x = MZ0 . p &
y = MZ0 . q &
z = MZ0 . (p '&' q) holds
P1[
p,
q,
x,
y,
z]
and
for
p,
q being
Element of
HP-WFF st
p => q in Z0 holds
for
x,
y,
z being
set st
x = MZ0 . p &
y = MZ0 . q &
z = MZ0 . (p => q) holds
P2[
p,
q,
x,
y,
z]
;
A74:
Y0 c= Z0
proof
let x be
object ;
TARSKI:def 3 ( not x in Y0 or x in Z0 )
Z0 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A19, A22;
then A75:
ex
Y being
Subset of
HP-WFF st
(
Y = Z0 &
VERUM in Y & ( for
n being
Element of
NAT holds
prop n in Y ) & ( for
p,
q being
Element of
HP-WFF st (
p '&' q in Y or
p => q in Y ) holds
(
p in Y &
q in Y ) ) & ex
M being
ManySortedSet of
Y st
(
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) ) )
;
assume A76:
x in Y0
;
x in Z0
end;
then A77:
Y0 c= dom MZ0
by PARTFUN1:def 2;
A78:
for
n being
Element of
NAT holds
M . (prop n) = F2(
n)
A79:
for
p,
q being
Element of
HP-WFF st
p => q in uZ holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z]
proof
let p,
q be
Element of
HP-WFF ;
( p => q in uZ implies for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] )
assume
p => q in uZ
;
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z]
then consider Z1 being
set such that A80:
p => q in Z1
and A81:
Z1 in Z
by TARSKI:def 4;
Z1 in dom MM
by A81, PARTFUN1:def 2;
then
MM . Z1 in rr
by FUNCT_1:def 3;
then A82:
MM . Z1 c= M
by A57, ZFMISC_1:74;
let x,
y,
z be
set ;
( x = M . p & y = M . q & z = M . (p => q) implies P2[p,q,x,y,z] )
assume that A83:
x = M . p
and A84:
y = M . q
and A85:
z = M . (p => q)
;
P2[p,q,x,y,z]
S2[
Z1,
MM . Z1]
by A27, A81;
then consider MZ1 being
ManySortedSet of
Z1 such that A86:
MZ1 = MM . Z1
and
MZ1 . VERUM = F1()
and
for
n being
Element of
NAT holds
MZ1 . (prop n) = F2(
n)
and
for
p,
q being
Element of
HP-WFF st
p '&' q in Z1 holds
for
x,
y,
z being
set st
x = MZ1 . p &
y = MZ1 . q &
z = MZ1 . (p '&' q) holds
P1[
p,
q,
x,
y,
z]
and A87:
for
p,
q being
Element of
HP-WFF st
p => q in Z1 holds
for
x,
y,
z being
set st
x = MZ1 . p &
y = MZ1 . q &
z = MZ1 . (p => q) holds
P2[
p,
q,
x,
y,
z]
;
p => q in dom MZ1
by A80, PARTFUN1:def 2;
then A88:
z = MZ1 . (p => q)
by A86, A82, A85, GRFUNC_1:2;
Z1 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A19, A81;
then A89:
ex
Y being
Subset of
HP-WFF st
(
Z1 = Y &
VERUM in Y & ( for
n being
Element of
NAT holds
prop n in Y ) & ( for
p,
q being
Element of
HP-WFF st (
p '&' q in Y or
p => q in Y ) holds
(
p in Y &
q in Y ) ) & ex
M being
ManySortedSet of
Y st
(
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) ) )
;
then
q in Z1
by A80;
then
q in dom MZ1
by PARTFUN1:def 2;
then A90:
y = MZ1 . q
by A86, A82, A84, GRFUNC_1:2;
p in Z1
by A80, A89;
then
p in dom MZ1
by PARTFUN1:def 2;
then
x = MZ1 . p
by A86, A82, A83, GRFUNC_1:2;
hence
P2[
p,
q,
x,
y,
z]
by A80, A87, A90, A88;
verum
end;
A91:
for
p,
q being
Element of
HP-WFF st (
p '&' q in uZ or
p => q in uZ ) holds
(
p in uZ &
q in uZ )
proof
let p,
q be
Element of
HP-WFF ;
( ( p '&' q in uZ or p => q in uZ ) implies ( p in uZ & q in uZ ) )
assume A92:
(
p '&' q in uZ or
p => q in uZ )
;
( p in uZ & q in uZ )
per cases
( p '&' q in uZ or p => q in uZ )
by A92;
suppose
p '&' q in uZ
;
( p in uZ & q in uZ )then consider Z0 being
set such that A93:
p '&' q in Z0
and A94:
Z0 in Z
by TARSKI:def 4;
Z0 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A19, A94;
then
ex
Y being
Subset of
HP-WFF st
(
Z0 = Y &
VERUM in Y & ( for
n being
Element of
NAT holds
prop n in Y ) & ( for
p,
q being
Element of
HP-WFF st (
p '&' q in Y or
p => q in Y ) holds
(
p in Y &
q in Y ) ) & ex
M being
ManySortedSet of
Y st
(
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) ) )
;
then
(
p in Z0 &
q in Z0 )
by A93;
hence
(
p in uZ &
q in uZ )
by A94, TARSKI:def 4;
verum end; suppose
p => q in uZ
;
( p in uZ & q in uZ )then consider Z0 being
set such that A95:
p => q in Z0
and A96:
Z0 in Z
by TARSKI:def 4;
Z0 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A19, A96;
then
ex
Y being
Subset of
HP-WFF st
(
Z0 = Y &
VERUM in Y & ( for
n being
Element of
NAT holds
prop n in Y ) & ( for
p,
q being
Element of
HP-WFF st (
p '&' q in Y or
p => q in Y ) holds
(
p in Y &
q in Y ) ) & ex
M being
ManySortedSet of
Y st
(
M . VERUM = F1() & ( for
n being
Element of
NAT holds
M . (prop n) = F2(
n) ) & ( for
p,
q being
Element of
HP-WFF st
p '&' q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p '&' q) holds
P1[
p,
q,
x,
y,
z] ) & ( for
p,
q being
Element of
HP-WFF st
p => q in Y holds
for
x,
y,
z being
set st
x = M . p &
y = M . q &
z = M . (p => q) holds
P2[
p,
q,
x,
y,
z] ) ) )
;
then
(
p in Z0 &
q in Z0 )
by A95;
hence
(
p in uZ &
q in uZ )
by A96, TARSKI:def 4;
verum end; end;
end;
Z0 c= uZ
by A22, ZFMISC_1:74;
then A97:
Y0 c= uZ
by A74;
A98:
for
n being
Element of
NAT holds
prop n in uZ
by A14, A97;
M . VERUM = F1()
by A16, A70, A71, A72, A77, GRFUNC_1:2;
hence
union Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A16, A97, A98, A91, A78, A58, A79;
verum
end;
A99:
for p, q being Element of HP-WFF st p => q in Y0 holds
for x, y, z being set st x = M0 . p & y = M0 . q & z = M0 . (p => q) holds
P2[p,q,x,y,z]
by A11;
M0 . VERUM = F1()
by A10, A16;
then
Y0 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A16, A14, A15, A13, A99;
then consider H being set such that
A100:
H in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
and
A101:
for Z being set st Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } & Z <> H holds
not H c= Z
by A17, ORDERS_1:67;
consider Y being Subset of HP-WFF such that
A102:
Y = H
and
A103:
VERUM in Y
and
A104:
for n being Element of NAT holds prop n in Y
and
A105:
for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y )
and
A106:
ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) )
by A100;
consider M being ManySortedSet of Y such that
A107:
M . VERUM = F1()
and
A108:
for n being Element of NAT holds M . (prop n) = F2(n)
and
A109:
for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z]
and
A110:
for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z]
by A106;
A111:
Y = HP-WFF
proof
defpred S2[
Element of
HP-WFF ]
means $1
in Y;
A112:
for
n being
Element of
NAT holds
S2[
prop n]
by A104;
A113:
for
r,
s being
Element of
HP-WFF st
S2[
r] &
S2[
s] holds
(
S2[
r '&' s] &
S2[
r => s] )
proof
let r,
s be
Element of
HP-WFF ;
( S2[r] & S2[s] implies ( S2[r '&' s] & S2[r => s] ) )
assume A114:
(
r in Y &
s in Y )
;
( S2[r '&' s] & S2[r => s] )
assume A115:
( not
S2[
r '&' s] or not
S2[
r => s] )
;
contradiction
per cases
( not r '&' s in Y or not r => s in Y )
by A115;
suppose A116:
not
r '&' s in Y
;
contradiction
{(r '&' s)} c= HP-WFF
by ZFMISC_1:31;
then reconsider Y9 =
Y \/ {(r '&' s)} as
Subset of
HP-WFF by XBOOLE_1:8;
consider CMrMs being
set such that A117:
P1[
r,
s,
M . r,
M . s,
CMrMs]
by A1;
set N =
M +* ((r '&' s) .--> CMrMs);
A118:
dom ((r '&' s) .--> CMrMs) = {(r '&' s)}
;
dom M = Y
by PARTFUN1:def 2;
then
dom (M +* ((r '&' s) .--> CMrMs)) = Y9
by A118, FUNCT_4:def 1;
then reconsider N =
M +* ((r '&' s) .--> CMrMs) as
ManySortedSet of
Y9 by PARTFUN1:def 2, RELAT_1:def 18;
r '&' s in {(r '&' s)}
by TARSKI:def 1;
then A119:
r '&' s in Y9
by XBOOLE_0:def 3;
A120:
for
p,
q being
Element of
HP-WFF st
p => q in Y9 holds
for
x,
y,
z being
set st
x = N . p &
y = N . q &
z = N . (p => q) holds
P2[
p,
q,
x,
y,
z]
proof
let p,
q be
Element of
HP-WFF ;
( p => q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z] )
assume A121:
p => q in Y9
;
for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z]
p => q <> r '&' s
by Th22;
then A122:
not
p => q in {(r '&' s)}
by TARSKI:def 1;
then A123:
p => q in Y
by A121, XBOOLE_0:def 3;
then
p in Y
by A105;
then
not
p in {(r '&' s)}
by A116, TARSKI:def 1;
then A124:
N . p = M . p
by A118, FUNCT_4:11;
q in Y
by A105, A123;
then
not
q in {(r '&' s)}
by A116, TARSKI:def 1;
then A125:
N . q = M . q
by A118, FUNCT_4:11;
A126:
N . (p => q) = M . (p => q)
by A118, A122, FUNCT_4:11;
let x,
y,
z be
set ;
( x = N . p & y = N . q & z = N . (p => q) implies P2[p,q,x,y,z] )
assume
(
x = N . p &
y = N . q &
z = N . (p => q) )
;
P2[p,q,x,y,z]
hence
P2[
p,
q,
x,
y,
z]
by A110, A123, A124, A125, A126;
verum
end; A127:
for
n being
Element of
NAT holds
N . (prop n) = F2(
n)
A128:
for
p,
q being
Element of
HP-WFF st
p '&' q in Y9 holds
for
x,
y,
z being
set st
x = N . p &
y = N . q &
z = N . (p '&' q) holds
P1[
p,
q,
x,
y,
z]
proof
let p,
q be
Element of
HP-WFF ;
( p '&' q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z] )
assume A129:
p '&' q in Y9
;
for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z]
let x,
y,
z be
set ;
( x = N . p & y = N . q & z = N . (p '&' q) implies P1[p,q,x,y,z] )
assume A130:
(
x = N . p &
y = N . q &
z = N . (p '&' q) )
;
P1[p,q,x,y,z]
per cases
( p '&' q = r '&' s or p '&' q <> r '&' s )
;
suppose A131:
p '&' q = r '&' s
;
P1[p,q,x,y,z]
q <> p '&' q
by Th27;
then
not
q in {(r '&' s)}
by A131, TARSKI:def 1;
then A132:
N . q = M . q
by A118, FUNCT_4:11;
p <> p '&' q
by Th27;
then
not
p in {(r '&' s)}
by A131, TARSKI:def 1;
then A133:
N . p = M . p
by A118, FUNCT_4:11;
p '&' q in {(r '&' s)}
by A131, TARSKI:def 1;
then A134:
N . (p '&' q) = ((r '&' s) .--> CMrMs) . (p '&' q)
by A118, FUNCT_4:13;
(
p = r &
q = s )
by A131, Th19;
hence
P1[
p,
q,
x,
y,
z]
by A117, A130, A133, A132, A134, FUNCOP_1:72;
verum end; suppose
p '&' q <> r '&' s
;
P1[p,q,x,y,z]then A135:
not
p '&' q in {(r '&' s)}
by TARSKI:def 1;
then A136:
p '&' q in Y
by A129, XBOOLE_0:def 3;
then
p in Y
by A105;
then
not
p in {(r '&' s)}
by A116, TARSKI:def 1;
then A137:
N . p = M . p
by A118, FUNCT_4:11;
q in Y
by A105, A136;
then
not
q in {(r '&' s)}
by A116, TARSKI:def 1;
then A138:
N . q = M . q
by A118, FUNCT_4:11;
N . (p '&' q) = M . (p '&' q)
by A118, A135, FUNCT_4:11;
hence
P1[
p,
q,
x,
y,
z]
by A109, A130, A136, A137, A138;
verum end; end;
end; A139:
Y c= Y9
by XBOOLE_1:7;
then A140:
for
n being
Element of
NAT holds
prop n in Y9
by A104;
A141:
for
p,
q being
Element of
HP-WFF st (
p '&' q in Y9 or
p => q in Y9 ) holds
(
p in Y9 &
q in Y9 )
VERUM <> r '&' s
by Th23;
then
not
VERUM in {(r '&' s)}
by TARSKI:def 1;
then
N . VERUM = F1()
by A107, A118, FUNCT_4:11;
then
Y9 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A103, A139, A140, A141, A127, A128, A120;
hence
contradiction
by A101, A102, A116, A119, XBOOLE_1:7;
verum end; suppose A146:
not
r => s in Y
;
contradiction
{(r => s)} c= HP-WFF
by ZFMISC_1:31;
then reconsider Y9 =
Y \/ {(r => s)} as
Subset of
HP-WFF by XBOOLE_1:8;
consider IMrMs being
set such that A147:
P2[
r,
s,
M . r,
M . s,
IMrMs]
by A2;
set N =
M +* ((r => s) .--> IMrMs);
A148:
dom ((r => s) .--> IMrMs) = {(r => s)}
;
dom M = Y
by PARTFUN1:def 2;
then
dom (M +* ((r => s) .--> IMrMs)) = Y9
by A148, FUNCT_4:def 1;
then reconsider N =
M +* ((r => s) .--> IMrMs) as
ManySortedSet of
Y9 by PARTFUN1:def 2, RELAT_1:def 18;
r => s in {(r => s)}
by TARSKI:def 1;
then A149:
r => s in Y9
by XBOOLE_0:def 3;
A150:
for
p,
q being
Element of
HP-WFF st
p '&' q in Y9 holds
for
x,
y,
z being
set st
x = N . p &
y = N . q &
z = N . (p '&' q) holds
P1[
p,
q,
x,
y,
z]
proof
let p,
q be
Element of
HP-WFF ;
( p '&' q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z] )
assume A151:
p '&' q in Y9
;
for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z]
p '&' q <> r => s
by Th22;
then A152:
not
p '&' q in {(r => s)}
by TARSKI:def 1;
then A153:
p '&' q in Y
by A151, XBOOLE_0:def 3;
then
p in Y
by A105;
then
not
p in {(r => s)}
by A146, TARSKI:def 1;
then A154:
N . p = M . p
by A148, FUNCT_4:11;
q in Y
by A105, A153;
then
not
q in {(r => s)}
by A146, TARSKI:def 1;
then A155:
N . q = M . q
by A148, FUNCT_4:11;
A156:
N . (p '&' q) = M . (p '&' q)
by A148, A152, FUNCT_4:11;
let x,
y,
z be
set ;
( x = N . p & y = N . q & z = N . (p '&' q) implies P1[p,q,x,y,z] )
assume
(
x = N . p &
y = N . q &
z = N . (p '&' q) )
;
P1[p,q,x,y,z]
hence
P1[
p,
q,
x,
y,
z]
by A109, A153, A154, A155, A156;
verum
end; A157:
for
n being
Element of
NAT holds
N . (prop n) = F2(
n)
A158:
for
p,
q being
Element of
HP-WFF st
p => q in Y9 holds
for
x,
y,
z being
set st
x = N . p &
y = N . q &
z = N . (p => q) holds
P2[
p,
q,
x,
y,
z]
proof
let p,
q be
Element of
HP-WFF ;
( p => q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z] )
assume A159:
p => q in Y9
;
for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z]
let x,
y,
z be
set ;
( x = N . p & y = N . q & z = N . (p => q) implies P2[p,q,x,y,z] )
assume A160:
(
x = N . p &
y = N . q &
z = N . (p => q) )
;
P2[p,q,x,y,z]
per cases
( p => q = r => s or p => q <> r => s )
;
suppose A161:
p => q = r => s
;
P2[p,q,x,y,z]
q <> p => q
by Th28;
then
not
q in {(r => s)}
by A161, TARSKI:def 1;
then A162:
N . q = M . q
by A148, FUNCT_4:11;
p <> p => q
by Th28;
then
not
p in {(r => s)}
by A161, TARSKI:def 1;
then A163:
N . p = M . p
by A148, FUNCT_4:11;
p => q in {(r => s)}
by A161, TARSKI:def 1;
then A164:
N . (p => q) = ((r => s) .--> IMrMs) . (p => q)
by A148, FUNCT_4:13;
(
p = r &
q = s )
by A161, Th20;
hence
P2[
p,
q,
x,
y,
z]
by A147, A160, A163, A162, A164, FUNCOP_1:72;
verum end; suppose
p => q <> r => s
;
P2[p,q,x,y,z]then A165:
not
p => q in {(r => s)}
by TARSKI:def 1;
then A166:
p => q in Y
by A159, XBOOLE_0:def 3;
then
p in Y
by A105;
then
not
p in {(r => s)}
by A146, TARSKI:def 1;
then A167:
N . p = M . p
by A148, FUNCT_4:11;
q in Y
by A105, A166;
then
not
q in {(r => s)}
by A146, TARSKI:def 1;
then A168:
N . q = M . q
by A148, FUNCT_4:11;
N . (p => q) = M . (p => q)
by A148, A165, FUNCT_4:11;
hence
P2[
p,
q,
x,
y,
z]
by A110, A160, A166, A167, A168;
verum end; end;
end; A169:
Y c= Y9
by XBOOLE_1:7;
then A170:
for
n being
Element of
NAT holds
prop n in Y9
by A104;
A171:
for
p,
q being
Element of
HP-WFF st (
p '&' q in Y9 or
p => q in Y9 ) holds
(
p in Y9 &
q in Y9 )
VERUM <> r => s
by Th25;
then
not
VERUM in {(r => s)}
by TARSKI:def 1;
then
N . VERUM = F1()
by A107, A148, FUNCT_4:11;
then
Y9 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
by A103, A169, A170, A171, A157, A158, A150;
hence
contradiction
by A101, A102, A146, A149, XBOOLE_1:7;
verum end; end;
end;
A176:
S2[
VERUM ]
by A103;
for
s being
Element of
HP-WFF holds
S2[
s]
from HILBERT2:sch 2(A176, A112, A113);
hence
Y = HP-WFF
by SUBSET_1:28;
verum
end;
then reconsider M = M as ManySortedSet of HP-WFF ;
take
M
; ( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( P1[p,q,M . p,M . q,M . (p '&' q)] & P2[p,q,M . p,M . q,M . (p => q)] ) ) )
thus
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( P1[p,q,M . p,M . q,M . (p '&' q)] & P2[p,q,M . p,M . q,M . (p => q)] ) ) )
by A107, A108, A109, A110, A111; verum