let A be Element of PL-WFF ; for F being Subset of PL-WFF st F |- A holds
F |= A
let F be Subset of PL-WFF; ( F |- A implies F |= A )
assume
F |- A
; F |= A
then consider f being FinSequence of PL-WFF such that
A1:
f . (len f) = A
and
A2:
1 <= len f
and
A3:
for i being Nat st 1 <= i & i <= len f holds
prc f,F,i
;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies F |= f /. $1 );
A4:
for i being Nat st ( for j being Nat st j < i holds
S1[j] ) holds
S1[i]
proof
let i be
Nat;
( ( for j being Nat st j < i holds
S1[j] ) implies S1[i] )
assume A5:
for
j being
Nat st
j < i holds
S1[
j]
;
S1[i]
per cases
( i = 0 or not i < 1 )
by NAT_1:14;
suppose
not
i < 1
;
S1[i]assume that A6:
1
<= i
and A7:
i <= len f
;
F |= f /. iper cases
( f . i in PL_axioms or f . i in F or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) )
by A3, A6, A7, defprc;
suppose
ex
j,
k being
Nat st
( 1
<= j &
j < i & 1
<= k &
k < i &
f /. j,
f /. k MP_rule f /. i )
;
F |= f /. ithen consider j,
k being
Nat such that A10:
1
<= j
and A11:
j < i
and A12:
1
<= k
and A13:
k < i
and A14:
f /. j,
f /. k MP_rule f /. i
;
U1:
k <= len f
by A7, A13, XXREAL_0:2;
A16:
j <= len f
by A7, A11, XXREAL_0:2;
F |= (f /. j) => (f /. i)
by A5, A12, A13, A14, U1;
hence
F |= f /. i
by A5, A10, A11, A16, th24;
verum end; end; end; end;
end;
A22:
for i being Nat holds S1[i]
from NAT_1:sch 4(A4);
f /. (len f) = A
by A1, A2, LTLAXIO5:1;
hence
F |= A
by A2, A22; verum