let S be Language; R#3e S is Correct
now for X being set st X is S -correct holds
(R#3e S) . X is S -correct set f =
R#3e S;
set R =
P#3e S;
set Q =
S -sequents ;
set E =
TheEqSymbOf S;
set N =
TheNorSymbOf S;
set FF =
AllFormulasOf S;
set TT =
AllTermsOf S;
set SS =
AllSymbolsOf S;
set F =
S -firstChar ;
set C =
S -multiCat ;
let X be
set ;
( X is S -correct implies (R#3e S) . X is S -correct )assume A1:
X is
S -correct
;
(R#3e S) . X is S -correct now for U being non empty set
for I being Element of U -InterpretersOf S
for x being b2 -satisfied set
for psi being wff string of S st [x,psi] in (R#3e S) . X holds
I -TruthEval psi = 1let U be non
empty set ;
for I being Element of U -InterpretersOf S
for x being b1 -satisfied set
for psi being wff string of S st [x,psi] in (R#3e S) . X holds
b5 -TruthEval b7 = 1set II =
U -InterpretersOf S;
let I be
Element of
U -InterpretersOf S;
for x being I -satisfied set
for psi being wff string of S st [x,psi] in (R#3e S) . X holds
b4 -TruthEval b6 = 1let x be
I -satisfied set ;
for psi being wff string of S st [x,psi] in (R#3e S) . X holds
b3 -TruthEval b5 = 1let psi be
wff string of
S;
( [x,psi] in (R#3e S) . X implies b2 -TruthEval b4 = 1 )set s =
[x,psi];
set TE =
I -TermEval ;
set d =
U -deltaInterpreter ;
assume A3:
[x,psi] in (R#3e S) . X
;
b2 -TruthEval b4 = 1then A4:
(
[x,psi] in S -sequents &
[X,[x,psi]] in P#3e S )
by Lm30;
then
X in dom (P#3e S)
by XTUPLE_0:def 12;
then reconsider Seqts =
X as
S -correct Subset of
(S -sequents) by A1;
reconsider seqt =
[x,psi] as
Element of
S -sequents by A3, Lm30;
seqt Rule3e Seqts
by A4, Def40;
then consider r being
relational Element of
S,
T1,
T2 being
|.(ar r).| -element Element of
(AllTermsOf S) * such that A5:
(
seqt `1 = {(r -compound T1)} \/ { ((<*(TheEqSymbOf S)*> ^ (TT1 . j)) ^ (TT2 . j)) where j is Element of Seg |.(ar r).|, TT1, TT2 is Function of (Seg |.(ar r).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT1 = T1 & TT2 = T2 ) } &
seqt `2 = r -compound T2 )
;
reconsider psi0 =
psi as
0wff string of
S by A5;
reconsider phi1 =
r -compound T1 as
0wff string of
S ;
reconsider rr =
(S -firstChar) . psi0 as
relational Element of
S ;
reconsider Fam =
{ ((<*(TheEqSymbOf S)*> ^ (TT1 . j)) ^ (TT2 . j)) where j is Element of Seg |.(ar r).|, TT1, TT2 is Function of (Seg |.(ar r).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT1 = T1 & TT2 = T2 ) } null {phi1} as
Subset of
x by A5;
(
((<*r*> ^ ((S -multiCat) . T1)) . 1) \+\ r = {} &
((<*r*> ^ ((S -multiCat) . T2)) . 1) \+\ r = {} )
;
then
(
(<*r*> ^ ((S -multiCat) . T1)) . 1
= r &
(<*r*> ^ ((S -multiCat) . T2)) . 1
= r &
psi0 = <*r*> ^ ((S -multiCat) . T2) )
by A5, FOMODEL0:29;
then A6:
(
(S -firstChar) . phi1 = r &
rr = r &
psi0 = <*r*> ^ ((S -multiCat) . T2) )
by FOMODEL0:6;
then A7:
(
T1 = SubTerms phi1 &
T2 = SubTerms psi0 )
by FOMODEL1:def 38;
reconsider y =
{phi1} null Fam as
Subset of
x by A5;
A8:
{phi1} = y
;
end; hence
(R#3e S) . X is
S -correct
;
verum end;
hence
R#3e S is Correct
; verum