defpred S₁[ object , object ] means ( ( $1 = VERUM implies $2 = F₁() ) & ( for n being Element of NAT st $1 = prop n holds
$2 = F₂(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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,a,b,c] ) ) ) } ;
A5: { (prop n) where n is Element of NAT : verum } c= HP-WFF

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (prop n) where n is Element of NAT : verum } or x in HP-WFF )
assume x in { (prop n) where n is Element of NAT : verum } ; :: thesis: x in HP-WFF
then ex n being Element of NAT st x = prop n ;
hence x in HP-WFF ; :: thesis: verum

end;

{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 S₁[x,y]

proof

let x be object ; :: thesis: ( x in Y0 implies ex y being object st S₁[x,y] )
assume A7: x in Y0 ; :: thesis: ex y being object st S₁[x,y]

per cases ( x in { (prop n) where n is Element of NAT : verum } or x in {VERUM} ) by A7, XBOOLE_0:def 3;

suppose x in { (prop n) where n is Element of NAT : verum } ; :: thesis: ex y being object st S₁[x,y]

then consider n being Element of NAT such that
A8: x = prop n ;
take F₂(n) ; :: thesis: S₁[x,F₂(n)]
thus ( x = VERUM implies F₂(n) = F₁() ) by A8, Th29; :: thesis: for n being Element of NAT st x = prop n holds
F₂(n) = F₂(n)
let k be Element of NAT ; :: thesis: ( x = prop k implies F₂(n) = F₂(k) )
assume x = prop k ; :: thesis: F₂(n) = F₂(k)
hence F₂(n) = F₂(k) by A8, Th21; :: thesis: verum

end;

suppose A9: x in {VERUM} ; :: thesis: ex y being object st S₁[x,y]

take F₁() ; :: thesis: S₁[x,F₁()]
x = VERUM by A9, TARSKI:def 1;
hence S₁[x,F₁()] by Th29; :: thesis: verum

end;

end;

end;

consider M0 being ManySortedSet of Y0 such that
A10: for x being object st x in Y0 holds
S₁[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 )

proof

let p, q be Element of HP-WFF ; :: thesis: ( not p '&' q in Y0 & not p => q in Y0 )
assume A12: ( p '&' q in Y0 or p => q in Y0 ) ; :: thesis: contradiction

per cases ( p '&' q in {VERUM} or p => q in {VERUM} or p '&' q in { (prop n) where n is Element of NAT : verum } or p => q in { (prop n) where n is Element of NAT : verum } ) by A12, XBOOLE_0:def 3;

suppose ( p '&' q in {VERUM} or p => q in {VERUM} ) ; :: thesis: contradiction

then ( p '&' q = VERUM or p => q = VERUM ) by TARSKI:def 1;
hence contradiction by Th23, Th25; :: thesis: verum

end;

suppose p '&' q in { (prop n) where n is Element of NAT : verum } ; :: thesis: contradiction

then ex n being Element of NAT st p '&' q = prop n ;
hence contradiction by Th24; :: thesis: verum

end;

suppose p => q in { (prop n) where n is Element of NAT : verum } ; :: thesis: contradiction

then ex n being Element of NAT st p => q = prop n ;
hence contradiction by Th26; :: thesis: verum

end;

end;

end;

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
P₁[p,q,x,y,z] ) ) ;
A14: for n being Element of NAT holds prop n in Y0

proof

let k be Element of NAT ; :: thesis: prop k in Y0
prop k in { (prop n) where n is Element of NAT : verum } ;
hence prop k in Y0 by XBOOLE_0:def 3; :: thesis: verum

end;

A15: for n being Element of NAT holds M0 . (prop n) = F₂(n)

proof

let n be Element of NAT ; :: thesis: M0 . (prop n) = F₂(n)
prop n in Y0 by A14;
hence M0 . (prop n) = F₂(n) by A10; :: thesis: verum

end;

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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,a,b,c] ) ) ) }

proof

defpred S₂[ object , object ] means ex D1 being set ex M being ManySortedSet of D1 st
( D1 = $1 & M = $2 & M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) );
let Z be set ; :: thesis: ( 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,a,b,c] ) ) ) } and
A20: Z is c=-linear ; :: thesis: 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,a,b,c] ) ) ) } c= bool HP-WFF

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,a,b,c] ) ) ) } ; :: thesis: 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) ) ) ;
hence x in bool HP-WFF ; :: thesis: 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 S₂[x,y]

proof

let x be object ; :: thesis: ( x in Z implies ex y being object st S₂[x,y] )
assume x in Z ; :: thesis: ex y being object st S₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) ) ;
consider M being ManySortedSet of Y such that
A26: ( M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) ) by A25;
take M ; :: thesis: S₂[x,M]
thus S₂[x,M] by A24, A26; :: thesis: verum

end;

consider MM being ManySortedSet of Z such that
A27: for x being object st x in Z holds
S₂[x,MM . x] from PBOOLE:sch 3(A23);
rng MM is functional

proof

let y be object ; :: according to FUNCT_1:def 13 :: thesis: ( not y in rng MM or y is set )
assume y in rng MM ; :: thesis: y is set
then consider x being object such that
A28: x in dom MM and
A29: y = MM . x by FUNCT_1:def 3;
x in Z by A28, PARTFUN1:def 2;
then S₂[x,y] by A27, A29;
hence y is set ; :: thesis: verum

end;

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; :: thesis: ( f in rr & g in rr & dom f c= dom g implies f tolerates g )
assume f in rr ; :: thesis: ( 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 S₂[x1,MM . x1] by A27;
then A34: ex M being ManySortedSet of x1 st
( M = f & M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) ) by A32;
then A35: x1 = dom f by PARTFUN1:def 2;
assume g in rr ; :: thesis: ( 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 S₃[ Element of HP-WFF ] means ( $1 in x1 implies f . $1 = g . $1 );
assume A38: dom f c= dom g ; :: thesis: f tolerates g
x2 in Z by A36, PARTFUN1:def 2;
then S₂[x2,MM . x2] by A27;
then A39: ex M being ManySortedSet of x2 st
( M = g & M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) ) by A37;
A40: for n being Element of NAT holds S₃[ prop n]

proof

let n be Element of NAT ; :: thesis: S₃[ prop n]
assume prop n in x1 ; :: thesis: f . (prop n) = g . (prop n)
thus f . (prop n) = F₂(n) by A34
.= g . (prop n) by A39 ; :: thesis: verum

end;

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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,a,b,c] ) ) ) } by A19, A33;
A42: for r, s being Element of HP-WFF st S₃[r] & S₃[s] holds
( S₃[r '&' s] & S₃[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) ) ) & x1 c= x2 ) by A39, A38, A35, A41, PARTFUN1:def 2;
let r, s be Element of HP-WFF ; :: thesis: ( S₃[r] & S₃[s] implies ( S₃[r '&' s] & S₃[r => s] ) )
assume A44: ( ( r in x1 implies f . r = g . r ) & ( s in x1 implies f . s = g . s ) ) ; :: thesis: ( S₃[r '&' s] & S₃[r => s] )
thus ( r '&' s in x1 implies f . (r '&' s) = g . (r '&' s) ) :: thesis: S₃[r => s]

proof

assume r '&' s in x1 ; :: thesis: f . (r '&' s) = g . (r '&' s)
then ( P₁[r,s,g . r,g . s,f . (r '&' s)] & P₁[r,s,g . r,g . s,g . (r '&' s)] ) by A34, A39, A44, A43;
hence f . (r '&' s) = g . (r '&' s) by A3; :: thesis: verum

end;

thus ( r => s in x1 implies f . (r => s) = g . (r => s) ) :: thesis: verum

proof

assume r => s in x1 ; :: thesis: f . (r => s) = g . (r => s)
then ( P₂[r,s,g . r,g . s,f . (r => s)] & P₂[r,s,g . r,g . s,g . (r => s)] ) by A34, A39, A44, A43;
hence f . (r => s) = g . (r => s) by A4; :: thesis: verum

end;

end;

let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom f) /\ (dom g) or f . x = g . x )
assume x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then A45: x in x1 by A38, A35, XBOOLE_1:28;
A46: S₃[ VERUM ] by A34, A39;
for p being Element of HP-WFF holds S₃[p] from HILBERT2:sch 2(A46, A40, A42);
hence f . x = g . x by A21, A45, A41; :: thesis: verum

end;

for f, g being Function st f in rr & g in rr holds
f tolerates g

proof

let f, g be Function; :: thesis: ( f in rr & g in rr implies f tolerates g )
assume A47: f in rr ; :: thesis: ( 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 S₂[x1,MM . x1] by A27;
then ex M being ManySortedSet of x1 st
( M = f & M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) ) by A49;
then A51: x1 = dom f by PARTFUN1:def 2;
assume A52: g in rr ; :: thesis: 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;
S₂[x2,MM . x2] by A27, A55;
then ex M being ManySortedSet of x2 st
( M = g & M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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; :: thesis: 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

proof

let x be set ; :: thesis: ( x in Z implies MM . x is ManySortedSet of x )
assume x in Z ; :: thesis: MM . x is ManySortedSet of x
then S₂[x,MM . x] by A27;
hence MM . x is ManySortedSet of x ; :: thesis: verum

end;

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
P₁[p,q,x,y,z]

proof

let p, q be Element of HP-WFF ; :: thesis: ( p '&' q in uZ implies for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P₁[p,q,x,y,z] )
assume p '&' q in uZ ; :: thesis: for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P₁[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 ; :: thesis: ( x = M . p & y = M . q & z = M . (p '&' q) implies P₁[p,q,x,y,z] )
assume that
A62: x = M . p and
A63: y = M . q and
A64: z = M . (p '&' q) ; :: thesis: P₁[p,q,x,y,z]
S₂[Z1,MM . Z1] by A27, A60;
then consider MZ1 being ManySortedSet of Z1 such that
A65: MZ1 = MM . Z1 and
MZ1 . VERUM = F₁() and
for n being Element of NAT holds MZ1 . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 P₁[p,q,x,y,z] by A59, A66, A69, A67; :: thesis: 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;
S₂[Z0,MM . Z0] by A27, A22;
then consider MZ0 being ManySortedSet of Z0 such that
A71: MZ0 = MM . Z0 and
A72: MZ0 . VERUM = F₁() and
A73: for n being Element of NAT holds MZ0 . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ;
A74: Y0 c= Z0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) ) ) ;
assume A76: x in Y0 ; :: thesis: x in Z0

per cases ( x in {VERUM} or x in { (prop n) where n is Element of NAT : verum } ) by A76, XBOOLE_0:def 3;

suppose x in {VERUM} ; :: thesis: x in Z0

hence x in Z0 by A75, TARSKI:def 1; :: thesis: verum

end;

suppose x in { (prop n) where n is Element of NAT : verum } ; :: thesis: x in Z0

then ex n being Element of NAT st x = prop n ;
hence x in Z0 by A75; :: thesis: verum

end;

end;

end;

then A77: Y0 c= dom MZ0 by PARTFUN1:def 2;
A78: for n being Element of NAT holds M . (prop n) = F₂(n)

proof

let n be Element of NAT ; :: thesis: M . (prop n) = F₂(n)
prop n in Y0 by A14;
hence M . (prop n) = MZ0 . (prop n) by A70, A71, A77, GRFUNC_1:2
.= F₂(n) by A73 ;
:: thesis: verum

end;

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
P₂[p,q,x,y,z]

proof

let p, q be Element of HP-WFF ; :: thesis: ( p => q in uZ implies for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P₂[p,q,x,y,z] )
assume p => q in uZ ; :: thesis: for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P₂[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 ; :: thesis: ( x = M . p & y = M . q & z = M . (p => q) implies P₂[p,q,x,y,z] )
assume that
A83: x = M . p and
A84: y = M . q and
A85: z = M . (p => q) ; :: thesis: P₂[p,q,x,y,z]
S₂[Z1,MM . Z1] by A27, A81;
then consider MZ1 being ManySortedSet of Z1 such that
A86: MZ1 = MM . Z1 and
MZ1 . VERUM = F₁() and
for n being Element of NAT holds MZ1 . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 P₂[p,q,x,y,z] by A80, A87, A90, A88; :: thesis: 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 ; :: thesis: ( ( 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 ) ; :: thesis: ( p in uZ & q in uZ )

per cases ( p '&' q in uZ or p => q in uZ ) by A92;

suppose p '&' q in uZ ; :: thesis: ( 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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; :: thesis: verum

end;

suppose p => q in uZ ; :: thesis: ( 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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; :: thesis: 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 = F₁() 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,a,b,c] ) ) ) } by A16, A97, A98, A91, A78, A58, A79; :: thesis: 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
P₂[p,q,x,y,z] by A11;
M0 . VERUM = F₁() 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] ) ) by A100;
consider M being ManySortedSet of Y such that
A107: M . VERUM = F₁() and
A108: for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,x,y,z] by A106;
A111: Y = HP-WFF

proof

defpred S₂[ Element of HP-WFF ] means $1 in Y;
A112: for n being Element of NAT holds S₂[ prop n] by A104;
A113: for r, s being Element of HP-WFF st S₂[r] & S₂[s] holds
( S₂[r '&' s] & S₂[r => s] )

proof

let r, s be Element of HP-WFF ; :: thesis: ( S₂[r] & S₂[s] implies ( S₂[r '&' s] & S₂[r => s] ) )
assume A114: ( r in Y & s in Y ) ; :: thesis: ( S₂[r '&' s] & S₂[r => s] )
assume A115: ( not S₂[r '&' s] or not S₂[r => s] ) ; :: thesis: contradiction

per cases ( not r '&' s in Y or not r => s in Y ) by A115;

suppose A116: not r '&' s in Y ; :: thesis: 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: P₁[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
P₂[p,q,x,y,z]

proof

let p, q be Element of HP-WFF ; :: thesis: ( p => q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P₂[p,q,x,y,z] )
assume A121: p => q in Y9 ; :: thesis: for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P₂[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 ; :: thesis: ( x = N . p & y = N . q & z = N . (p => q) implies P₂[p,q,x,y,z] )
assume ( x = N . p & y = N . q & z = N . (p => q) ) ; :: thesis: P₂[p,q,x,y,z]
hence P₂[p,q,x,y,z] by A110, A123, A124, A125, A126; :: thesis: verum

end;

A127: for n being Element of NAT holds N . (prop n) = F₂(n)

proof

let n be Element of NAT ; :: thesis: N . (prop n) = F₂(n)
prop n <> r '&' s by Th24;
then not prop n in {(r '&' s)} by TARSKI:def 1;
hence N . (prop n) = M . (prop n) by A118, FUNCT_4:11
.= F₂(n) by A108 ;
:: thesis: verum

end;

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
P₁[p,q,x,y,z]

proof

let p, q be Element of HP-WFF ; :: thesis: ( p '&' q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P₁[p,q,x,y,z] )
assume A129: p '&' q in Y9 ; :: thesis: for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P₁[p,q,x,y,z]
let x, y, z be set ; :: thesis: ( x = N . p & y = N . q & z = N . (p '&' q) implies P₁[p,q,x,y,z] )
assume A130: ( x = N . p & y = N . q & z = N . (p '&' q) ) ; :: thesis: P₁[p,q,x,y,z]

per cases ( p '&' q = r '&' s or p '&' q <> r '&' s ) ;

suppose A131: p '&' q = r '&' s ; :: thesis: P₁[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 P₁[p,q,x,y,z] by A117, A130, A133, A132, A134, FUNCOP_1:72; :: thesis: verum

end;

suppose p '&' q <> r '&' s ; :: thesis: P₁[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 P₁[p,q,x,y,z] by A109, A130, A136, A137, A138; :: thesis: 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 )

proof

let p, q be Element of HP-WFF ; :: thesis: ( ( p '&' q in Y9 or p => q in Y9 ) implies ( p in Y9 & q in Y9 ) )
assume A142: ( p '&' q in Y9 or p => q in Y9 ) ; :: thesis: ( p in Y9 & q in Y9 )

per cases ( p '&' q = r '&' s or ( p '&' q in Y9 & p '&' q <> r '&' s ) or p => q in Y9 ) by A142;

suppose p '&' q = r '&' s ; :: thesis: ( p in Y9 & q in Y9 )

then ( p = r & q = s ) by Th19;
hence ( p in Y9 & q in Y9 ) by A114, A139; :: thesis: verum

end;

suppose that A143: p '&' q in Y9 and
A144: p '&' q <> r '&' s ; :: thesis: ( p in Y9 & q in Y9 )

not p '&' q in {(r '&' s)} by A144, TARSKI:def 1;
then p '&' q in Y by A143, XBOOLE_0:def 3;
then ( p in Y & q in Y ) by A105;
hence ( p in Y9 & q in Y9 ) by A139; :: thesis: verum

end;

suppose A145: p => q in Y9 ; :: thesis: ( p in Y9 & q in Y9 )

p => q <> r '&' s by Th22;
then not p => q in {(r '&' s)} by TARSKI:def 1;
then p => q in Y by A145, XBOOLE_0:def 3;
then ( p in Y & q in Y ) by A105;
hence ( p in Y9 & q in Y9 ) by A139; :: thesis: verum

end;

end;

end;

VERUM <> r '&' s by Th23;
then not VERUM in {(r '&' s)} by TARSKI:def 1;
then N . VERUM = F₁() 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,a,b,c] ) ) ) } by A103, A139, A140, A141, A127, A128, A120;
hence contradiction by A101, A102, A116, A119, XBOOLE_1:7; :: thesis: verum

end;

suppose A146: not r => s in Y ; :: thesis: 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: P₂[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
P₁[p,q,x,y,z]

proof

let p, q be Element of HP-WFF ; :: thesis: ( p '&' q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P₁[p,q,x,y,z] )
assume A151: p '&' q in Y9 ; :: thesis: for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P₁[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 ; :: thesis: ( x = N . p & y = N . q & z = N . (p '&' q) implies P₁[p,q,x,y,z] )
assume ( x = N . p & y = N . q & z = N . (p '&' q) ) ; :: thesis: P₁[p,q,x,y,z]
hence P₁[p,q,x,y,z] by A109, A153, A154, A155, A156; :: thesis: verum

end;

A157: for n being Element of NAT holds N . (prop n) = F₂(n)

proof

let n be Element of NAT ; :: thesis: N . (prop n) = F₂(n)
prop n <> r => s by Th26;
then not prop n in {(r => s)} by TARSKI:def 1;
hence N . (prop n) = M . (prop n) by A148, FUNCT_4:11
.= F₂(n) by A108 ;
:: thesis: verum

end;

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
P₂[p,q,x,y,z]

proof

let p, q be Element of HP-WFF ; :: thesis: ( p => q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P₂[p,q,x,y,z] )
assume A159: p => q in Y9 ; :: thesis: for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P₂[p,q,x,y,z]
let x, y, z be set ; :: thesis: ( x = N . p & y = N . q & z = N . (p => q) implies P₂[p,q,x,y,z] )
assume A160: ( x = N . p & y = N . q & z = N . (p => q) ) ; :: thesis: P₂[p,q,x,y,z]

per cases ( p => q = r => s or p => q <> r => s ) ;

suppose A161: p => q = r => s ; :: thesis: P₂[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 P₂[p,q,x,y,z] by A147, A160, A163, A162, A164, FUNCOP_1:72; :: thesis: verum

end;

suppose p => q <> r => s ; :: thesis: P₂[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 P₂[p,q,x,y,z] by A110, A160, A166, A167, A168; :: thesis: 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 )

proof

let p, q be Element of HP-WFF ; :: thesis: ( ( p '&' q in Y9 or p => q in Y9 ) implies ( p in Y9 & q in Y9 ) )
assume A172: ( p '&' q in Y9 or p => q in Y9 ) ; :: thesis: ( p in Y9 & q in Y9 )

per cases ( p => q = r => s or ( p => q in Y9 & p => q <> r => s ) or p '&' q in Y9 ) by A172;

suppose p => q = r => s ; :: thesis: ( p in Y9 & q in Y9 )

then ( p = r & q = s ) by Th20;
hence ( p in Y9 & q in Y9 ) by A114, A169; :: thesis: verum

end;

suppose that A173: p => q in Y9 and
A174: p => q <> r => s ; :: thesis: ( p in Y9 & q in Y9 )

not p => q in {(r => s)} by A174, TARSKI:def 1;
then p => q in Y by A173, XBOOLE_0:def 3;
then ( p in Y & q in Y ) by A105;
hence ( p in Y9 & q in Y9 ) by A169; :: thesis: verum

end;

suppose A175: p '&' q in Y9 ; :: thesis: ( p in Y9 & q in Y9 )

p '&' q <> r => s by Th22;
then not p '&' q in {(r => s)} by TARSKI:def 1;
then p '&' q in Y by A175, XBOOLE_0:def 3;
then ( p in Y & q in Y ) by A105;
hence ( p in Y9 & q in Y9 ) by A169; :: thesis: verum

end;

end;

end;

VERUM <> r => s by Th25;
then not VERUM in {(r => s)} by TARSKI:def 1;
then N . VERUM = F₁() 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 = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(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
P₁[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
P₂[p,q,a,b,c] ) ) ) } by A103, A169, A170, A171, A157, A158, A150;
hence contradiction by A101, A102, A146, A149, XBOOLE_1:7; :: thesis: verum

end;

end;

end;

A176: S₂[ VERUM ] by A103;
for s being Element of HP-WFF holds S₂[s] from HILBERT2:sch 2(A176, A112, A113);
hence Y = HP-WFF by SUBSET_1:28; :: thesis: verum

end;

then reconsider M = M as ManySortedSet of HP-WFF ;
take M ; :: thesis: ( M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(n) ) & ( for p, q being Element of HP-WFF holds
( P₁[p,q,M . p,M . q,M . (p '&' q)] & P₂[p,q,M . p,M . q,M . (p => q)] ) ) )
thus ( M . VERUM = F₁() & ( for n being Element of NAT holds M . (prop n) = F₂(n) ) & ( for p, q being Element of HP-WFF holds
( P₁[p,q,M . p,M . q,M . (p '&' q)] & P₂[p,q,M . p,M . q,M . (p => q)] ) ) ) by A107, A108, A109, A110, A111; :: thesis: verum