reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set SS = AllSymbolsOf S;
set Phim = S -formulasOfMaxDepth m;
defpred S1[ set ] means for U being non empty set
for I being Element of U -InterpretersOf S holds $1 = dom ((I,m) -TruthEval);
let x be Subset of (((AllSymbolsOf S) *) \ {{}}); :: thesis: ( x = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval) )
thus ( x = S -formulasOfMaxDepth m implies S1[x] ) :: thesis: ( ( for U being non empty set
for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval) ) implies x = S -formulasOfMaxDepth m )
proof
assume A1: x = S -formulasOfMaxDepth m ; :: thesis: S1[x]
thus for U being non empty set
for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval) :: thesis: verum
proof
let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval)
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: x = dom ((I,m) -TruthEval)
S -formulasOfMaxDepth m = dom ((I,mm) -TruthEval) by Def22;
hence x = dom ((I,m) -TruthEval) by A1; :: thesis: verum
end;
end;
assume A2: S1[x] ; :: thesis: x = S -formulasOfMaxDepth m
for U being non empty set
for I being Element of U -InterpretersOf S
for nn being Element of NAT st m = nn holds
x = dom ((I,nn) -TruthEval) by A2;
hence x = S -formulasOfMaxDepth m by Def22; :: thesis: verum