defpred S1[ Element of NAT , Element of BOOLEAN ] means ( $2 = 1 iff Prop $1 in M );
A16: for x being Element of NAT ex y being Element of BOOLEAN st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of BOOLEAN st S1[x,y]
defpred S2[ Element of BOOLEAN ] means ( $1 = 1 iff Prop x in M );
per cases ( prop x in M or not prop x in M ) ;
suppose prop x in M ; :: thesis: ex y being Element of BOOLEAN st S1[x,y]
then S2[ TRUE ] ;
hence ex y being Element of BOOLEAN st S1[x,y] ; :: thesis: verum
end;
suppose not prop x in M ; :: thesis: ex y being Element of BOOLEAN st S1[x,y]
then S2[ FALSE ] ;
hence ex y being Element of BOOLEAN st S1[x,y] ; :: thesis: verum
end;
end;
end;
consider f1 being sequence of BOOLEAN such that
A19: for k being Element of NAT holds S1[k,f1 . k] from FUNCT_2:sch 3(A16);
 deffunc H1( Element of NAT ) -> Element of BOOLEAN = f1 . $1;
defpred S2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ex s5 being Element of BOOLEAN st $5 = FALSE ;
defpred S3[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is Element of BOOLEAN & $4 is Element of BOOLEAN implies ex s3, s4, s5 being Element of BOOLEAN st
( s3 = $3 & s4 = $4 & s5 = $5 & s5 = s3 => s4 ) ) & ( ( not $3 is Element of BOOLEAN or not $4 is Element of BOOLEAN ) implies $5 = FALSE ) );
A1: for p, q being Element of HP-WFF
for a, b being set ex c being set st S2[p,q,a,b,c] ;
A2: for p, q being Element of HP-WFF
for a, b being set ex d being set st S3[p,q,a,b,d]
proof
let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex d being set st S3[p,q,a,b,d]
let a, b be set ; :: thesis: ex d being set st S3[p,q,a,b,d]
per cases ( ( a is Element of BOOLEAN & b is Element of BOOLEAN ) or not a is Element of BOOLEAN or not b is Element of BOOLEAN ) ;
suppose ( a is Element of BOOLEAN & b is Element of BOOLEAN ) ; :: thesis: ex d being set st S3[p,q,a,b,d]
then reconsider a1 = a, b1 = b as Element of BOOLEAN ;
reconsider ab = a1 => b1 as Element of BOOLEAN by MARGREL1:def 12;
ab = a1 => b1 ;
hence ex d being set st S3[p,q,a,b,d] ; :: thesis: verum
end;
suppose ( not a is Element of BOOLEAN or not b is Element of BOOLEAN ) ; :: thesis: ex d being set st S3[p,q,a,b,d]
hence ex d being set st S3[p,q,a,b,d] ; :: thesis: verum
end;
end;
end;
A3: for p, q being Element of HP-WFF
for a, b, c, d being set st S2[p,q,a,b,c] & S2[p,q,a,b,d] holds
c = d ;
A4: for p, q being Element of HP-WFF
for a, b, c, d being set st S3[p,q,a,b,c] & S3[p,q,a,b,d] holds
c = d ;
consider sat being ManySortedSet of HP-WFF such that
A34: ( sat . VERUM = 0 & ( for n being Element of NAT holds sat . (prop n) = H1(n) ) & ( for p, q being Element of HP-WFF holds
( S2[p,q,sat . p,sat . q,sat . (p '&' q)] & S3[p,q,sat . p,sat . q,sat . (p => q)] ) ) ) from HILBERT2:sch 3(A1, A2, A3, A4);
 A35: for x being object st x in HP-WFF holds
sat . x in BOOLEAN
proof
let x be object ; :: thesis: ( x in HP-WFF implies sat . x in BOOLEAN )
assume x in HP-WFF ; :: thesis: sat . x in BOOLEAN
then reconsider x1 = x as Element of HP-WFF ;
A42: now :: thesis: for n being Element of NAT holds sat . (prop n) in BOOLEAN
let n be Element of NAT ; :: thesis: sat . (prop n) in BOOLEAN
sat . (prop n) = f1 . n by A34;
hence sat . (prop n) in BOOLEAN ; :: thesis: verum
end;
per cases ( x1 = VERUM or x1 is simple or x1 is conjunctive or x1 is conditional ) by HILBERT2:9;
suppose x1 is conjunctive ; :: thesis: sat . x in BOOLEAN
then consider A, B being Element of HP-WFF such that
E2: x1 = A '&' B by HILBERT2:def 6;
consider s5 being Element of BOOLEAN such that
E3: sat . (A '&' B) = FALSE by A34;
thus sat . x in BOOLEAN by E3, E2; :: thesis: verum
end;
suppose x1 is conditional ; :: thesis: sat . x in BOOLEAN
then consider A, B being Element of HP-WFF such that
E1: x1 = A => B by HILBERT2:def 7;
A37: S3[A,B,sat . A,sat . B,sat . (A => B)] by A34;
thus sat . x in BOOLEAN by A37, E1; :: thesis: verum
end;
end;
end;
dom sat = HP-WFF by PARTFUN1:def 2;
then reconsider sat = sat as Function of HP-WFF,BOOLEAN by A35, FUNCT_2:3;
set satc = sat | PL-WFF;
reconsider satc = sat | PL-WFF as Function of PL-WFF,BOOLEAN by FUNCT_2:32, plhp;
B1: satc . FaLSUM = 0 by A34, FUNCT_1:49;
B2: for k being Element of NAT holds
( satc . (Prop k) = 1 iff Prop k in M )
proof
let k be Element of NAT ; :: thesis: ( satc . (Prop k) = 1 iff Prop k in M )
hereby :: thesis: ( Prop k in M implies satc . (Prop k) = 1 )
assume satc . (Prop k) = 1 ; :: thesis: Prop k in M
then D2: sat . (Prop k) = 1 by FUNCT_1:49;
sat . (prop k) = f1 . k by A34;
hence Prop k in M by A19, D2; :: thesis: verum
end;
assume Prop k in M ; :: thesis: satc . (Prop k) = 1
then D1: f1 . k = 1 by A19;
sat . (prop k) = f1 . k by A34;
hence satc . (Prop k) = 1 by D1, FUNCT_1:49; :: thesis: verum
end;
for p, q being Element of PL-WFF holds satc . (p => q) = (satc . p) => (satc . q)
proof
let p, q be Element of PL-WFF ; :: thesis: satc . (p => q) = (satc . p) => (satc . q)
reconsider p1 = p, q1 = q as Element of HP-WFF by plhp;
consider s3, s4, s5 being Element of BOOLEAN such that
D4: ( s3 = sat . p1 & s4 = sat . q1 & s5 = sat . (p1 => q1) & s5 = s3 => s4 ) by A34;
thus satc . (p => q) = sat . (p => q) by FUNCT_1:49
.= (satc . p) => (sat . q) by FUNCT_1:49, D4
.= (satc . p) => (satc . q) by FUNCT_1:49 ; :: thesis: verum
end;
hence ex b1 being Function of PL-WFF,BOOLEAN st
( b1 . FaLSUM = 0 & ( for k being Element of NAT holds
( b1 . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b1 . (p => q) = (b1 . p) => (b1 . q) ) ) by B1, B2; :: thesis: verum