let X be Subset of MC-wff; :: thesis: for p being Element of MC-wff st p in CnIPC X holds
ex Y being Subset of MC-wff st
( Y c= X & Y is finite & p in CnIPC Y )
let p be Element of MC-wff ; :: thesis: ( p in CnIPC X implies ex Y being Subset of MC-wff st
( Y c= X & Y is finite & p in CnIPC Y ) )
assume p in CnIPC X ; :: thesis: ex Y being Subset of MC-wff st
( Y c= X & Y is finite & p in CnIPC Y )
then consider f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] such that
A1: f is_a_proof_wrt_IPC X and
A2: Effect_IPC f = p by Th16;
A3: f <> {} by A1;
consider A being set such that
A4: A is finite and
A5: A c= MC-wff and
A6: rng f c= [:A,Proof_Step_Kinds_IPC:] by FINSEQ_1:def 4, FINSET_1:14;
reconsider Z = A as Subset of MC-wff by A5;
take Y = Z /\ X; :: thesis: ( Y c= X & Y is finite & p in CnIPC Y )
thus Y c= X by XBOOLE_1:17; :: thesis: ( Y is finite & p in CnIPC Y )
thus Y is finite by A4; :: thesis: p in CnIPC Y
for n being Nat st 1 <= n & n <= len f holds
f,n is_a_correct_step_wrt_IPC Y
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len f implies f,n is_a_correct_step_wrt_IPC Y )
assume A7: ( 1 <= n & n <= len f ) ; :: thesis: f,n is_a_correct_step_wrt_IPC Y
then A8: f,n is_a_correct_step_wrt_IPC X by A1;
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10 by A7, Th3;
per cases then ( (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 or (f . n) `2 = 10 ) ;
:: according to INTPRO_2:def 3
case (f . n) `2 = 1 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = p => (q => p)
hence ex p, q being Element of MC-wff st (f . n) `1 = p => (q => p) by A8, Def3; :: thesis: verum
end;
case (f . n) `2 = 2 ; :: thesis: ex p, q, r being Element of MC-wff st (f . n) `1 = (p => (q => r)) => ((p => q) => (p => r))
hence ex p, q, r being Element of MC-wff st (f . n) `1 = (p => (q => r)) => ((p => q) => (p => r)) by A8, Def3; :: thesis: verum
end;
case (f . n) `2 = 3 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => p
hence ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => p by A8, Def3; :: thesis: verum
end;
case (f . n) `2 = 4 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => q
hence ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => q by A8, Def3; :: thesis: verum
end;
case (f . n) `2 = 5 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = p => (q => (p '&' q))
hence ex p, q being Element of MC-wff st (f . n) `1 = p => (q => (p '&' q)) by A8, Def3; :: thesis: verum
end;
case (f . n) `2 = 6 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = p => (p 'or' q)
hence ex p, q being Element of MC-wff st (f . n) `1 = p => (p 'or' q) by A8, Def3; :: thesis: verum
end;
case (f . n) `2 = 7 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = q => (p 'or' q)
hence ex p, q being Element of MC-wff st (f . n) `1 = q => (p 'or' q) by A8, Def3; :: thesis: verum
end;
case (f . n) `2 = 8 ; :: thesis: ex p, q, r being Element of MC-wff st (f . n) `1 = (p => r) => ((q => r) => ((p 'or' q) => r))
hence ex p, q, r being Element of MC-wff st (f . n) `1 = (p => r) => ((q => r) => ((p 'or' q) => r)) by A8, Def3; :: thesis: verum
end;
case (f . n) `2 = 9 ; :: thesis: ex p being Element of MC-wff st (f . n) `1 = FALSUM => p
hence ex p being Element of MC-wff st (f . n) `1 = FALSUM => p by A8, Def3; :: thesis: verum
end;
case (f . n) `2 = 10 ; :: thesis: ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q )
hence ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A8, Def3; :: thesis: verum
end;
end;
end;
then f is_a_proof_wrt_IPC Y by A3;
then p in { q where q is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC Y & Effect_IPC f = q ) } by A2;
hence p in CnIPC Y by Th15; :: thesis: verum