let l be Element of NAT ; :: thesis: for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X & 1 <= l & l <= len f holds
(f . l) `1 in Cn X
let X be Subset of CQC-WFF ; :: thesis: for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X & 1 <= l & l <= len f holds
(f . l) `1 in Cn X
let f be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :]; :: thesis: ( f is_a_proof_wrt X & 1 <= l & l <= len f implies (f . l) `1 in Cn X )
assume that
A1: f is_a_proof_wrt X and
A2: ( 1 <= l & l <= len f ) ; :: thesis: (f . l) `1 in Cn X
A3: for n being Element of NAT st 1 <= n & n <= len f holds
(f . n) `1 in Cn X
proof
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies (f . $1) `1 in Cn X );
A4: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A5: for k being Nat st k < n holds
S1[k] ; :: thesis: S1[n]
A6: n in NAT by ORDINAL1:def 13;
assume that
A7: 1 <= n and
A8: n <= len f ; :: thesis: (f . n) `1 in Cn X
A9: f,n is_a_correct_step_wrt X by A1, A6, A7, A8, Def5;
A10: now
per cases ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) by A7, A8, Th45;
suppose A11: (f . n) `2 = 0 ; :: thesis: (f . n) `1 in Cn X
A12: (f . n) `1 in X by A9, A11, Def4;
A13: X c= Cn X by Th38;
thus (f . n) `1 in Cn X by A12, A13; :: thesis: verum
end;
suppose A14: (f . n) `2 = 1 ; :: thesis: (f . n) `1 in Cn X
A15: (f . n) `1 = VERUM by A9, A14, Def4;
thus (f . n) `1 in Cn X by A15, Th27; :: thesis: verum
end;
suppose A16: (f . n) `2 = 2 ; :: thesis: (f . n) `1 in Cn X
A17: ex p being Element of CQC-WFF st (f . n) `1 = (('not' p) => p) => p by A9, A16, Def4;
thus (f . n) `1 in Cn X by A17, Th28; :: thesis: verum
end;
suppose A18: (f . n) `2 = 3 ; :: thesis: (f . n) `1 in Cn X
A19: ex p, q being Element of CQC-WFF st (f . n) `1 = p => (('not' p) => q) by A9, A18, Def4;
thus (f . n) `1 in Cn X by A19, Th29; :: thesis: verum
end;
suppose A20: (f . n) `2 = 4 ; :: thesis: (f . n) `1 in Cn X
A21: ex p, q, r being Element of CQC-WFF st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A9, A20, Def4;
thus (f . n) `1 in Cn X by A21, Th30; :: thesis: verum
end;
suppose A22: (f . n) `2 = 5 ; :: thesis: (f . n) `1 in Cn X
A23: ex p, q being Element of CQC-WFF st (f . n) `1 = (p '&' q) => (q '&' p) by A9, A22, Def4;
thus (f . n) `1 in Cn X by A23, Th31; :: thesis: verum
end;
suppose A24: (f . n) `2 = 6 ; :: thesis: (f . n) `1 in Cn X
A25: ex p being Element of CQC-WFF ex x being bound_QC-variable st (f . n) `1 = (All x,p) => p by A9, A24, Def4;
thus (f . n) `1 in Cn X by A25, Th33; :: thesis: verum
end;
suppose A26: (f . n) `2 = 7 ; :: thesis: (f . n) `1 in Cn X
consider i, j being Element of NAT , p, q being Element of CQC-WFF such that
A27: 1 <= i and
A28: i < n and
A29: 1 <= j and
A30: j < i and
A31: ( p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A9, A26, Def4;
A32: j < n by A28, A30, XXREAL_0:2;
A33: i <= len f by A8, A28, XXREAL_0:2;
A34: j <= len f by A30, A33, XXREAL_0:2;
A35: (f . j) `1 in Cn X by A5, A29, A32, A34;
A36: (f . i) `1 in Cn X by A5, A27, A28, A33;
thus (f . n) `1 in Cn X by A31, A35, A36, Th32; :: thesis: verum
end;
suppose A37: (f . n) `2 = 8 ; :: thesis: (f . n) `1 in Cn X
consider i being Element of NAT , p, q being Element of CQC-WFF , x being bound_QC-variable such that
A38: 1 <= i and
A39: i < n and
A40: ( (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All x,q) ) by A9, A37, Def4;
A41: i <= len f by A8, A39, XXREAL_0:2;
thus (f . n) `1 in Cn X by A5, A38, A39, A40, A41, Th34; :: thesis: verum
end;
suppose A42: (f . n) `2 = 9 ; :: thesis: (f . n) `1 in Cn X
consider i being Element of NAT , x, y being bound_QC-variable, s being QC-formula such that
A43: 1 <= i and
A44: i < n and
A45: ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . n) `1 = s . y ) by A9, A42, Def4;
A46: i <= len f by A8, A44, XXREAL_0:2;
thus (f . n) `1 in Cn X by A5, A43, A44, A45, A46, Th35; :: thesis: verum
end;
end;
end;
thus (f . n) `1 in Cn X by A10; :: thesis: verum
end;
A47: for n being Nat holds S1[n] from NAT_1:sch 4(A4);
 thus for n being Element of NAT st 1 <= n & n <= len f holds
(f . n) `1 in Cn X by A47; :: thesis: verum
end;
thus (f . l) `1 in Cn X by A2, A3; :: thesis: verum