:: CQC_THE2 semantic presentation
begin
theorem Th1: :: CQC_THE2:1
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
(p '&' q) => r is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
(p '&' q) => r is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid implies (p '&' q) => r is valid )
A1: (p => (q => r)) => ((p '&' q) => r) in TAUT A by PROCAL_1:32;
assume p => (q => r) in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: (p '&' q) => r is valid
hence (p '&' q) => r in TAUT A by A1, CQC_THE1:46; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
theorem Th2: :: CQC_THE2:2
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
(q '&' p) => r is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
(q '&' p) => r is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid implies (q '&' p) => r is valid )
assume p => (q => r) in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: (q '&' p) => r is valid
then p => (q => r) is valid by CQC_THE1:def_10;
then (p '&' q) => r is valid by Th1;
then A1: (p '&' q) => r in TAUT A by CQC_THE1:def_10;
(q '&' p) => (p '&' q) in TAUT A by CQC_THE1:45;
hence (q '&' p) => r in TAUT A by A1, LUKASI_1:3; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
theorem Th3: :: CQC_THE2:3
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds
p => (q => r) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds
p => (q => r) is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( (p '&' q) => r is valid implies p => (q => r) is valid )
A1: ((p '&' q) => r) => (p => (q => r)) in TAUT A by PROCAL_1:31;
assume (p '&' q) => r in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: p => (q => r) is valid
hence p => (q => r) in TAUT A by A1, CQC_THE1:46; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
theorem Th4: :: CQC_THE2:4
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds
q => (p => r) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds
q => (p => r) is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( (p '&' q) => r is valid implies q => (p => r) is valid )
A1: (q '&' p) => (p '&' q) in TAUT A by CQC_THE1:45;
assume (p '&' q) => r in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: q => (p => r) is valid
then (q '&' p) => r in TAUT A by A1, LUKASI_1:3;
then (q '&' p) => r is valid by CQC_THE1:def_10;
then q => (p => r) is valid by Th3;
hence q => (p => r) in TAUT A by CQC_THE1:def_10; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm1: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( (p '&' q) => p is valid & (p '&' q) => q is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( (p '&' q) => p is valid & (p '&' q) => q is valid )
let p, q be Element of CQC-WFF A; ::_thesis: ( (p '&' q) => p is valid & (p '&' q) => q is valid )
thus ( (p '&' q) => p in TAUT A & (p '&' q) => q in TAUT A ) by PROCAL_1:19, PROCAL_1:21; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm2: for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q is valid holds
( p is valid & q is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p '&' q is valid holds
( p is valid & q is valid )
let p, q be Element of CQC-WFF A; ::_thesis: ( p '&' q is valid implies ( p is valid & q is valid ) )
assume A1: p '&' q is valid ; ::_thesis: ( p is valid & q is valid )
( (p '&' q) => p is valid & (p '&' q) => q is valid ) by Lm1;
hence ( p is valid & q is valid ) by A1, CQC_THE1:65; ::_thesis: verum
end;
Lm3: for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & p => r is valid holds
p => (q '&' r) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid & p => r is valid holds
p => (q '&' r) is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid & p => r is valid implies p => (q '&' r) is valid )
assume ( p => q in TAUT A & p => r in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: p => (q '&' r) is valid
hence p => (q '&' r) in TAUT A by PROCAL_1:52; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm4: for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p 'or' r) => (q 'or' t) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p 'or' r) => (q 'or' t) is valid
let p, q, r, t be Element of CQC-WFF A; ::_thesis: ( p => q is valid & r => t is valid implies (p 'or' r) => (q 'or' t) is valid )
assume ( p => q in TAUT A & r => t in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: (p 'or' r) => (q 'or' t) is valid
hence (p 'or' r) => (q 'or' t) in TAUT A by PROCAL_1:57; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm5: for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p '&' r) => (q '&' t) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p '&' r) => (q '&' t) is valid
let p, q, r, t be Element of CQC-WFF A; ::_thesis: ( p => q is valid & r => t is valid implies (p '&' r) => (q '&' t) is valid )
assume ( p => q in TAUT A & r => t in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: (p '&' r) => (q '&' t) is valid
hence (p '&' r) => (q '&' t) in TAUT A by PROCAL_1:56; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm6: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => (p 'or' q) is valid & p => (q 'or' p) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( p => (p 'or' q) is valid & p => (q 'or' p) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: ( p => (p 'or' q) is valid & p => (q 'or' p) is valid )
thus ( p => (p 'or' q) in TAUT A & p => (q 'or' p) in TAUT A ) by PROCAL_1:3, PROCAL_1:4; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm7: for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & r => q is valid holds
(p 'or' r) => q is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid & r => q is valid holds
(p 'or' r) => q is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid & r => q is valid implies (p 'or' r) => q is valid )
assume ( p => q in TAUT A & r => q in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: (p 'or' r) => q is valid
hence (p 'or' r) => q in TAUT A by PROCAL_1:53; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm8: for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is valid & q is valid holds
p '&' q is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is valid & q is valid holds
p '&' q is valid
let p, q be Element of CQC-WFF A; ::_thesis: ( p is valid & q is valid implies p '&' q is valid )
assume ( p in TAUT A & q in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: p '&' q is valid
hence p '&' q in TAUT A by PROCAL_1:47; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm9: for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(r '&' p) => (r '&' q) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid holds
(r '&' p) => (r '&' q) is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid implies (r '&' p) => (r '&' q) is valid )
assume p => q in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: (r '&' p) => (r '&' q) is valid
hence (r '&' p) => (r '&' q) in TAUT A by PROCAL_1:50; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm10: for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(p 'or' r) => (q 'or' r) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid holds
(p 'or' r) => (q 'or' r) is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid implies (p 'or' r) => (q 'or' r) is valid )
assume p => q in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: (p 'or' r) => (q 'or' r) is valid
hence (p 'or' r) => (q 'or' r) in TAUT A by PROCAL_1:48; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm11: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) is valid
let p, q be Element of CQC-WFF A; ::_thesis: (p 'or' q) => (('not' p) => q) is valid
thus (p 'or' q) => (('not' p) => q) in TAUT A by PROCAL_1:5; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm12: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) => q) => (p 'or' q) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' p) => q) => (p 'or' q) is valid
let p, q be Element of CQC-WFF A; ::_thesis: (('not' p) => q) => (p 'or' q) is valid
('not' ('not' p)) => p in TAUT A by LUKASI_1:25;
then ( (('not' p) => q) => (('not' ('not' p)) 'or' q) in TAUT A & (('not' ('not' p)) 'or' q) => (p 'or' q) in TAUT A ) by PROCAL_1:14, PROCAL_1:48;
hence (('not' p) => q) => (p 'or' q) in TAUT A by LUKASI_1:3; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm13: for A being QC-alphabet
for p being Element of CQC-WFF A holds p <=> p is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p <=> p is valid
let p be Element of CQC-WFF A; ::_thesis: p <=> p is valid
(p => p) '&' (p => p) is valid by Lm8;
hence p <=> p is valid by QC_LANG2:def_4; ::_thesis: verum
end;
Lm14: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( ( p => q is valid & q => p is valid ) iff p <=> q is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( ( p => q is valid & q => p is valid ) iff p <=> q is valid )
let p, q be Element of CQC-WFF A; ::_thesis: ( ( p => q is valid & q => p is valid ) iff p <=> q is valid )
thus ( p => q is valid & q => p is valid implies p <=> q is valid ) ::_thesis: ( p <=> q is valid implies ( p => q is valid & q => p is valid ) )
proof
assume ( p => q is valid & q => p is valid ) ; ::_thesis: p <=> q is valid
then (p => q) '&' (q => p) is valid by Lm8;
hence p <=> q is valid by QC_LANG2:def_4; ::_thesis: verum
end;
assume p <=> q is valid ; ::_thesis: ( p => q is valid & q => p is valid )
then (p => q) '&' (q => p) is valid by QC_LANG2:def_4;
hence ( p => q is valid & q => p is valid ) by Lm2; ::_thesis: verum
end;
Lm15: for A being QC-alphabet
for p, q being Element of CQC-WFF A st p <=> q is valid holds
( p is valid iff q is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p <=> q is valid holds
( p is valid iff q is valid )
let p, q be Element of CQC-WFF A; ::_thesis: ( p <=> q is valid implies ( p is valid iff q is valid ) )
assume A1: p <=> q in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: ( p is valid iff q is valid )
(p <=> q) => (p => q) in TAUT A by PROCAL_1:23;
then A2: p => q in TAUT A by A1, CQC_THE1:46;
thus ( p is valid implies q is valid ) ::_thesis: ( q is valid implies p is valid )
proof
assume p in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: q is valid
hence q in TAUT A by A2, CQC_THE1:46; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
assume A3: q in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: p is valid
(p <=> q) => (q => p) in TAUT A by PROCAL_1:24;
then q => p in TAUT A by A1, CQC_THE1:46;
hence p in TAUT A by A3, CQC_THE1:46; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
Lm16: for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => (q => r) is valid & r => t is valid holds
p => (q => t) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, t being Element of CQC-WFF A st p => (q => r) is valid & r => t is valid holds
p => (q => t) is valid
let p, q, r, t be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid & r => t is valid implies p => (q => t) is valid )
assume that
A1: p => (q => r) is valid and
A2: r => t is valid ; ::_thesis: p => (q => t) is valid
(p '&' q) => r is valid by A1, Th1;
then (p '&' q) => t is valid by A2, LUKASI_1:42;
hence p => (q => t) is valid by Th3; ::_thesis: verum
end;
theorem Th5: :: CQC_THE2:5
for A being QC-alphabet
for s being QC-formula of A
for y, x being bound_QC-variable of A holds
( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
proof
let A be QC-alphabet ; ::_thesis: for s being QC-formula of A
for y, x being bound_QC-variable of A holds
( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
let s be QC-formula of A; ::_thesis: for y, x being bound_QC-variable of A holds
( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
let y, x be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
still_not-bound_in (All (x,s)) = (still_not-bound_in s) \ {x} by QC_LANG3:12;
hence ( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) by ZFMISC_1:56; ::_thesis: verum
end;
theorem Th6: :: CQC_THE2:6
for A being QC-alphabet
for s being QC-formula of A
for y, x being bound_QC-variable of A holds
( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
proof
let A be QC-alphabet ; ::_thesis: for s being QC-formula of A
for y, x being bound_QC-variable of A holds
( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
let s be QC-formula of A; ::_thesis: for y, x being bound_QC-variable of A holds
( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
let y, x be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
still_not-bound_in (Ex (x,s)) = (still_not-bound_in s) \ {x} by QC_LANG3:19;
hence ( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) by ZFMISC_1:56; ::_thesis: verum
end;
theorem Th7: :: CQC_THE2:7
for A being QC-alphabet
for s, h being QC-formula of A
for y being bound_QC-variable of A holds
( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
proof
let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A
for y being bound_QC-variable of A holds
( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
let s, h be QC-formula of A; ::_thesis: for y being bound_QC-variable of A holds
( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
let y be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
still_not-bound_in (s => h) = (still_not-bound_in s) \/ (still_not-bound_in h) by QC_LANG3:16;
hence ( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th8: :: CQC_THE2:8
for A being QC-alphabet
for s, h being QC-formula of A
for y being bound_QC-variable of A holds
( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
proof
let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A
for y being bound_QC-variable of A holds
( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
let s, h be QC-formula of A; ::_thesis: for y being bound_QC-variable of A holds
( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
let y be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
still_not-bound_in (s '&' h) = (still_not-bound_in s) \/ (still_not-bound_in h) by QC_LANG3:10;
hence ( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th9: :: CQC_THE2:9
for A being QC-alphabet
for s, h being QC-formula of A
for y being bound_QC-variable of A holds
( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
proof
let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A
for y being bound_QC-variable of A holds
( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
let s, h be QC-formula of A; ::_thesis: for y being bound_QC-variable of A holds
( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
let y be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
still_not-bound_in (s 'or' h) = (still_not-bound_in s) \/ (still_not-bound_in h) by QC_LANG3:14;
hence ( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: CQC_THE2:10
for A being QC-alphabet
for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) )
proof
let A be QC-alphabet ; ::_thesis: for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) )
let s be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) )
let x, y be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) )
not y in still_not-bound_in (All (y,s)) by Th5;
then A1: not y in still_not-bound_in (All (x,(All (y,s)))) by Th5;
not x in still_not-bound_in (All (x,(All (y,s)))) by Th5;
hence ( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) ) by A1, QC_LANG2:14; ::_thesis: verum
end;
theorem :: CQC_THE2:11
for A being QC-alphabet
for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) )
proof
let A be QC-alphabet ; ::_thesis: for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) )
let s be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) )
let x, y be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) )
not y in still_not-bound_in (Ex (y,s)) by Th6;
then A1: not y in still_not-bound_in (Ex (x,(Ex (y,s)))) by Th6;
not x in still_not-bound_in (Ex (x,(Ex (y,s)))) by Th6;
hence ( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) ) by A1, QC_LANG2:14; ::_thesis: verum
end;
theorem Th12: :: CQC_THE2:12
for A being QC-alphabet
for s, h being QC-formula of A
for x being bound_QC-variable of A holds (s => h) . x = (s . x) => (h . x)
proof
let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A
for x being bound_QC-variable of A holds (s => h) . x = (s . x) => (h . x)
let s, h be QC-formula of A; ::_thesis: for x being bound_QC-variable of A holds (s => h) . x = (s . x) => (h . x)
let x be bound_QC-variable of A; ::_thesis: (s => h) . x = (s . x) => (h . x)
s => h = 'not' (s '&' ('not' h)) by QC_LANG2:def_2;
hence (s => h) . x = 'not' ((s '&' ('not' h)) . x) by CQC_LANG:19
.= 'not' ((s . x) '&' (('not' h) . x)) by CQC_LANG:21
.= 'not' ((s . x) '&' ('not' (h . x))) by CQC_LANG:19
.= (s . x) => (h . x) by QC_LANG2:def_2 ;
::_thesis: verum
end;
theorem :: CQC_THE2:13
for A being QC-alphabet
for s, h being QC-formula of A
for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x)
proof
let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A
for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x)
let s, h be QC-formula of A; ::_thesis: for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x)
let x be bound_QC-variable of A; ::_thesis: (s 'or' h) . x = (s . x) 'or' (h . x)
thus (s 'or' h) . x = ('not' (('not' s) '&' ('not' h))) . x by QC_LANG2:def_3
.= 'not' ((('not' s) '&' ('not' h)) . x) by CQC_LANG:19
.= 'not' ((('not' s) . x) '&' (('not' h) . x)) by CQC_LANG:21
.= 'not' (('not' (s . x)) '&' (('not' h) . x)) by CQC_LANG:19
.= 'not' (('not' (s . x)) '&' ('not' (h . x))) by CQC_LANG:19
.= (s . x) 'or' (h . x) by QC_LANG2:def_3 ; ::_thesis: verum
end;
theorem :: CQC_THE2:14
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A st x <> y holds
(Ex (x,p)) . y = Ex (x,(p . y))
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A st x <> y holds
(Ex (x,p)) . y = Ex (x,(p . y))
let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A st x <> y holds
(Ex (x,p)) . y = Ex (x,(p . y))
let x, y be bound_QC-variable of A; ::_thesis: ( x <> y implies (Ex (x,p)) . y = Ex (x,(p . y)) )
assume A1: x <> y ; ::_thesis: (Ex (x,p)) . y = Ex (x,(p . y))
thus (Ex (x,p)) . y = ('not' (All (x,('not' p)))) . y by QC_LANG2:def_5
.= 'not' ((All (x,('not' p))) . y) by CQC_LANG:19
.= 'not' (All (x,(('not' p) . y))) by A1, CQC_LANG:25
.= 'not' (All (x,('not' (p . y)))) by CQC_LANG:19
.= Ex (x,(p . y)) by QC_LANG2:def_5 ; ::_thesis: verum
end;
theorem Th15: :: CQC_THE2:15
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds p => (Ex (x,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds p => (Ex (x,p)) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds p => (Ex (x,p)) is valid
let x be bound_QC-variable of A; ::_thesis: p => (Ex (x,p)) is valid
(All (x,('not' p))) => ('not' p) is valid by CQC_THE1:66;
then ('not' ('not' p)) => ('not' (All (x,('not' p)))) is valid by LUKASI_1:52;
then A1: ('not' ('not' p)) => (Ex (x,p)) is valid by QC_LANG2:def_5;
(('not' ('not' p)) => (Ex (x,p))) => (p => (Ex (x,p))) is valid ;
hence p => (Ex (x,p)) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
theorem Th16: :: CQC_THE2:16
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st p is valid holds
Ex (x,p) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A st p is valid holds
Ex (x,p) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p is valid holds
Ex (x,p) is valid
let x be bound_QC-variable of A; ::_thesis: ( p is valid implies Ex (x,p) is valid )
assume A1: p is valid ; ::_thesis: Ex (x,p) is valid
p => (Ex (x,p)) is valid by Th15;
hence Ex (x,p) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
theorem :: CQC_THE2:17
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,p)) => (Ex (x,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,p)) => (Ex (x,p)) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,p)) => (Ex (x,p)) is valid
let x be bound_QC-variable of A; ::_thesis: (All (x,p)) => (Ex (x,p)) is valid
( (All (x,p)) => p is valid & p => (Ex (x,p)) is valid ) by Th15, CQC_THE1:66;
hence (All (x,p)) => (Ex (x,p)) is valid by LUKASI_1:42; ::_thesis: verum
end;
theorem :: CQC_THE2:18
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds (All (x,p)) => (Ex (y,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds (All (x,p)) => (Ex (y,p)) is valid
let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A holds (All (x,p)) => (Ex (y,p)) is valid
let x, y be bound_QC-variable of A; ::_thesis: (All (x,p)) => (Ex (y,p)) is valid
( (All (x,p)) => p is valid & p => (Ex (y,p)) is valid ) by Th15, CQC_THE1:66;
hence (All (x,p)) => (Ex (y,p)) is valid by LUKASI_1:42; ::_thesis: verum
end;
theorem Th19: :: CQC_THE2:19
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p => q is valid & not x in still_not-bound_in q holds
(Ex (x,p)) => q is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p => q is valid & not x in still_not-bound_in q holds
(Ex (x,p)) => q is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p => q is valid & not x in still_not-bound_in q holds
(Ex (x,p)) => q is valid
let x be bound_QC-variable of A; ::_thesis: ( p => q is valid & not x in still_not-bound_in q implies (Ex (x,p)) => q is valid )
assume ( p => q is valid & not x in still_not-bound_in q ) ; ::_thesis: (Ex (x,p)) => q is valid
then ( ('not' q) => ('not' p) is valid & not x in still_not-bound_in ('not' q) ) by LUKASI_1:52, QC_LANG3:7;
then ('not' q) => (All (x,('not' p))) is valid by CQC_THE1:67;
then ('not' (All (x,('not' p)))) => ('not' ('not' q)) is valid by LUKASI_1:52;
then (Ex (x,p)) => ('not' ('not' q)) is valid by QC_LANG2:def_5;
hence (Ex (x,p)) => q is valid by LUKASI_1:55; ::_thesis: verum
end;
theorem Th20: :: CQC_THE2:20
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,p)) => p is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,p)) => p is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,p)) => p is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (Ex (x,p)) => p is valid )
A1: p => p is valid ;
assume not x in still_not-bound_in p ; ::_thesis: (Ex (x,p)) => p is valid
hence (Ex (x,p)) => p is valid by A1, Th19; ::_thesis: verum
end;
theorem :: CQC_THE2:21
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p & Ex (x,p) is valid holds
p is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p & Ex (x,p) is valid holds
p is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p & Ex (x,p) is valid holds
p is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p & Ex (x,p) is valid implies p is valid )
assume that
A1: not x in still_not-bound_in p and
A2: Ex (x,p) is valid ; ::_thesis: p is valid
(Ex (x,p)) => p is valid by A1, Th20;
hence p is valid by A2, CQC_THE1:65; ::_thesis: verum
end;
theorem Th22: :: CQC_THE2:22
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
p => (Ex (y,q)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
p => (Ex (y,q)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
p => (Ex (y,q)) is valid
let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
p => (Ex (y,q)) is valid
let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not y in still_not-bound_in h implies p => (Ex (y,q)) is valid )
assume that
A1: p = h . x and
A2: q = h . y and
A3: not y in still_not-bound_in h ; ::_thesis: p => (Ex (y,q)) is valid
A4: (h => (Ex (y,q))) . x = (h . x) => ((Ex (y,q)) . x) by Th12
.= p => (Ex (y,q)) by A1, CQC_LANG:27 ;
not y in still_not-bound_in (Ex (y,q)) by Th6;
then A5: not y in still_not-bound_in (h => (Ex (y,q))) by A3, Th7;
A6: q => (Ex (y,q)) is valid by Th15;
(h => (Ex (y,q))) . y = (h . y) => ((Ex (y,q)) . y) by Th12
.= q => (Ex (y,q)) by A2, CQC_LANG:27 ;
hence p => (Ex (y,q)) is valid by A6, A4, A5, CQC_THE1:68; ::_thesis: verum
end;
theorem Th23: :: CQC_THE2:23
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st p is valid holds
All (x,p) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A st p is valid holds
All (x,p) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p is valid holds
All (x,p) is valid
let x be bound_QC-variable of A; ::_thesis: ( p is valid implies All (x,p) is valid )
A1: p => (((All (x,p)) => (All (x,p))) => p) is valid ;
not x in still_not-bound_in (All (x,p)) by Th5;
then A2: not x in still_not-bound_in ((All (x,p)) => (All (x,p))) by Th7;
assume p is valid ; ::_thesis: All (x,p) is valid
then ((All (x,p)) => (All (x,p))) => p is valid by A1, CQC_THE1:65;
then ((All (x,p)) => (All (x,p))) => (All (x,p)) is valid by A2, CQC_THE1:67;
hence All (x,p) is valid by CQC_THE1:65; ::_thesis: verum
end;
theorem Th24: :: CQC_THE2:24
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
p => (All (x,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
p => (All (x,p)) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
p => (All (x,p)) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies p => (All (x,p)) is valid )
A1: p => p is valid ;
assume not x in still_not-bound_in p ; ::_thesis: p => (All (x,p)) is valid
hence p => (All (x,p)) is valid by A1, CQC_THE1:67; ::_thesis: verum
end;
theorem Th25: :: CQC_THE2:25
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h holds
(All (x,p)) => q is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h holds
(All (x,p)) => q is valid
let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h holds
(All (x,p)) => q is valid
let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h holds
(All (x,p)) => q is valid
let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not x in still_not-bound_in h implies (All (x,p)) => q is valid )
assume that
A1: p = h . x and
A2: q = h . y and
A3: not x in still_not-bound_in h ; ::_thesis: (All (x,p)) => q is valid
A4: ((All (x,p)) => h) . y = ((All (x,p)) . y) => q by A2, Th12
.= (All (x,p)) => q by CQC_LANG:27 ;
not x in still_not-bound_in (All (x,p)) by Th5;
then A5: ( (All (x,p)) => p is valid & not x in still_not-bound_in ((All (x,p)) => h) ) by A3, Th7, CQC_THE1:66;
((All (x,p)) => h) . x = ((All (x,p)) . x) => p by A1, Th12
.= (All (x,p)) => p by CQC_LANG:27 ;
hence (All (x,p)) => q is valid by A4, A5, CQC_THE1:68; ::_thesis: verum
end;
theorem :: CQC_THE2:26
for A being QC-alphabet
for p being Element of CQC-WFF A
for y, x being bound_QC-variable of A st not y in still_not-bound_in p holds
(All (x,p)) => (All (y,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for y, x being bound_QC-variable of A st not y in still_not-bound_in p holds
(All (x,p)) => (All (y,p)) is valid
let p be Element of CQC-WFF A; ::_thesis: for y, x being bound_QC-variable of A st not y in still_not-bound_in p holds
(All (x,p)) => (All (y,p)) is valid
let y, x be bound_QC-variable of A; ::_thesis: ( not y in still_not-bound_in p implies (All (x,p)) => (All (y,p)) is valid )
assume not y in still_not-bound_in p ; ::_thesis: (All (x,p)) => (All (y,p)) is valid
then ( (All (x,p)) => p is valid & not y in still_not-bound_in (All (x,p)) ) by Th5, CQC_THE1:66;
hence (All (x,p)) => (All (y,p)) is valid by CQC_THE1:67; ::_thesis: verum
end;
theorem :: CQC_THE2:27
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p holds
(All (x,p)) => (All (y,q)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p holds
(All (x,p)) => (All (y,q)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p holds
(All (x,p)) => (All (y,q)) is valid
let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p holds
(All (x,p)) => (All (y,q)) is valid
let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p implies (All (x,p)) => (All (y,q)) is valid )
assume ( p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p ) ; ::_thesis: (All (x,p)) => (All (y,q)) is valid
then ( not y in still_not-bound_in (All (x,p)) & (All (x,p)) => q is valid ) by Th5, Th25;
hence (All (x,p)) => (All (y,q)) is valid by CQC_THE1:67; ::_thesis: verum
end;
theorem :: CQC_THE2:28
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,p)) => (Ex (y,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,p)) => (Ex (y,p)) is valid
let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,p)) => (Ex (y,p)) is valid
let x, y be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (Ex (x,p)) => (Ex (y,p)) is valid )
assume not x in still_not-bound_in p ; ::_thesis: (Ex (x,p)) => (Ex (y,p)) is valid
then A1: not x in still_not-bound_in (Ex (y,p)) by Th6;
p => (Ex (y,p)) is valid by Th15;
hence (Ex (x,p)) => (Ex (y,p)) is valid by A1, Th19; ::_thesis: verum
end;
theorem :: CQC_THE2:29
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (y,q)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (y,q)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (y,q)) is valid
let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (y,q)) is valid
let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h implies (Ex (x,p)) => (Ex (y,q)) is valid )
assume ( p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h ) ; ::_thesis: (Ex (x,p)) => (Ex (y,q)) is valid
then ( not x in still_not-bound_in (Ex (y,q)) & p => (Ex (y,q)) is valid ) by Th6, Th22;
hence (Ex (x,p)) => (Ex (y,q)) is valid by Th19; ::_thesis: verum
end;
theorem Th30: :: CQC_THE2:30
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid
(All (x,(p => q))) => (p => q) is valid by CQC_THE1:66;
then A1: p => ((All (x,(p => q))) => q) is valid by LUKASI_1:44;
(All (x,p)) => p is valid by CQC_THE1:66;
then (All (x,p)) => ((All (x,(p => q))) => q) is valid by A1, LUKASI_1:42;
then A2: ((All (x,(p => q))) '&' (All (x,p))) => q is valid by Th2;
( not x in still_not-bound_in (All (x,(p => q))) & not x in still_not-bound_in (All (x,p)) ) by Th5;
then not x in still_not-bound_in ((All (x,(p => q))) '&' (All (x,p))) by Th8;
then ((All (x,(p => q))) '&' (All (x,p))) => (All (x,q)) is valid by A2, CQC_THE1:67;
hence (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid by Th3; ::_thesis: verum
end;
theorem Th31: :: CQC_THE2:31
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st All (x,(p => q)) is valid holds
(All (x,p)) => (All (x,q)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st All (x,(p => q)) is valid holds
(All (x,p)) => (All (x,q)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st All (x,(p => q)) is valid holds
(All (x,p)) => (All (x,q)) is valid
let x be bound_QC-variable of A; ::_thesis: ( All (x,(p => q)) is valid implies (All (x,p)) => (All (x,q)) is valid )
assume A1: All (x,(p => q)) is valid ; ::_thesis: (All (x,p)) => (All (x,q)) is valid
(All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid by Th30;
hence (All (x,p)) => (All (x,q)) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
theorem Th32: :: CQC_THE2:32
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid
A1: (All (x,((p => q) '&' (q => p)))) => ((p => q) '&' (q => p)) is valid by CQC_THE1:66;
(p <=> q) => (p <=> q) is valid ;
then (p <=> q) => ((p => q) '&' (q => p)) is valid by QC_LANG2:def_4;
then All (x,((p <=> q) => ((p => q) '&' (q => p)))) is valid by Th23;
then A2: (All (x,(p <=> q))) => (All (x,((p => q) '&' (q => p)))) is valid by Th31;
( (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid & (All (x,(q => p))) => ((All (x,q)) => (All (x,p))) is valid ) by Th30;
then ((All (x,(p => q))) '&' (All (x,(q => p)))) => (((All (x,p)) => (All (x,q))) '&' ((All (x,q)) => (All (x,p)))) is valid by Lm5;
then A3: ((All (x,(p => q))) '&' (All (x,(q => p)))) => ((All (x,p)) <=> (All (x,q))) is valid by QC_LANG2:def_4;
A4: not x in still_not-bound_in (All (x,((p => q) '&' (q => p)))) by Th5;
((p => q) '&' (q => p)) => (q => p) is valid by Lm1;
then (All (x,((p => q) '&' (q => p)))) => (q => p) is valid by A1, LUKASI_1:42;
then A5: (All (x,((p => q) '&' (q => p)))) => (All (x,(q => p))) is valid by A4, CQC_THE1:67;
((p => q) '&' (q => p)) => (p => q) is valid by Lm1;
then (All (x,((p => q) '&' (q => p)))) => (p => q) is valid by A1, LUKASI_1:42;
then (All (x,((p => q) '&' (q => p)))) => (All (x,(p => q))) is valid by A4, CQC_THE1:67;
then (All (x,((p => q) '&' (q => p)))) => ((All (x,(p => q))) '&' (All (x,(q => p)))) is valid by A5, Lm3;
then (All (x,((p => q) '&' (q => p)))) => ((All (x,p)) <=> (All (x,q))) is valid by A3, LUKASI_1:42;
hence (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid by A2, LUKASI_1:42; ::_thesis: verum
end;
theorem :: CQC_THE2:33
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st All (x,(p <=> q)) is valid holds
(All (x,p)) <=> (All (x,q)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st All (x,(p <=> q)) is valid holds
(All (x,p)) <=> (All (x,q)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st All (x,(p <=> q)) is valid holds
(All (x,p)) <=> (All (x,q)) is valid
let x be bound_QC-variable of A; ::_thesis: ( All (x,(p <=> q)) is valid implies (All (x,p)) <=> (All (x,q)) is valid )
assume A1: All (x,(p <=> q)) is valid ; ::_thesis: (All (x,p)) <=> (All (x,q)) is valid
(All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid by Th32;
hence (All (x,p)) <=> (All (x,q)) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
theorem Th34: :: CQC_THE2:34
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid
(All (x,(p => q))) => (p => q) is valid by CQC_THE1:66;
then A1: (p '&' (All (x,(p => q)))) => q is valid by Th2;
q => (Ex (x,q)) is valid by Th15;
then (p '&' (All (x,(p => q)))) => (Ex (x,q)) is valid by A1, LUKASI_1:42;
then A2: p => ((All (x,(p => q))) => (Ex (x,q))) is valid by Th3;
( not x in still_not-bound_in (All (x,(p => q))) & not x in still_not-bound_in (Ex (x,q)) ) by Th5, Th6;
then not x in still_not-bound_in ((All (x,(p => q))) => (Ex (x,q))) by Th7;
then (Ex (x,p)) => ((All (x,(p => q))) => (Ex (x,q))) is valid by A2, Th19;
hence (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid by LUKASI_1:44; ::_thesis: verum
end;
theorem Th35: :: CQC_THE2:35
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st All (x,(p => q)) is valid holds
(Ex (x,p)) => (Ex (x,q)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st All (x,(p => q)) is valid holds
(Ex (x,p)) => (Ex (x,q)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st All (x,(p => q)) is valid holds
(Ex (x,p)) => (Ex (x,q)) is valid
let x be bound_QC-variable of A; ::_thesis: ( All (x,(p => q)) is valid implies (Ex (x,p)) => (Ex (x,q)) is valid )
assume A1: All (x,(p => q)) is valid ; ::_thesis: (Ex (x,p)) => (Ex (x,q)) is valid
(All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid by Th34;
hence (Ex (x,p)) => (Ex (x,q)) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
theorem Th36: :: CQC_THE2:36
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid )
( (All (x,p)) => p is valid & (All (x,q)) => q is valid ) by CQC_THE1:66;
then A1: ((All (x,p)) '&' (All (x,q))) => (p '&' q) is valid by Lm5;
( All (x,((p '&' q) => q)) is valid & (All (x,((p '&' q) => q))) => ((All (x,(p '&' q))) => (All (x,q))) is valid ) by Lm1, Th23, Th30;
then A2: (All (x,(p '&' q))) => (All (x,q)) is valid by CQC_THE1:65;
( All (x,((p '&' q) => p)) is valid & (All (x,((p '&' q) => p))) => ((All (x,(p '&' q))) => (All (x,p))) is valid ) by Lm1, Th23, Th30;
then (All (x,(p '&' q))) => (All (x,p)) is valid by CQC_THE1:65;
hence (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid by A2, Lm3; ::_thesis: ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid
( not x in still_not-bound_in (All (x,p)) & not x in still_not-bound_in (All (x,q)) ) by Th5;
then not x in still_not-bound_in ((All (x,p)) '&' (All (x,q))) by Th8;
hence ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid by A1, CQC_THE1:67; ::_thesis: verum
end;
theorem Th37: :: CQC_THE2:37
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid
( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid ) by Th36;
hence (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid by Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:38
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid )
let x be bound_QC-variable of A; ::_thesis: ( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid )
(All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid by Th37;
hence ( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid ) by Lm15; ::_thesis: verum
end;
theorem Th39: :: CQC_THE2:39
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid
let x be bound_QC-variable of A; ::_thesis: ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid
( All (x,(q => (p 'or' q))) is valid & (All (x,(q => (p 'or' q)))) => ((All (x,q)) => (All (x,(p 'or' q)))) is valid ) by Lm6, Th23, Th30;
then A1: (All (x,q)) => (All (x,(p 'or' q))) is valid by CQC_THE1:65;
( All (x,(p => (p 'or' q))) is valid & (All (x,(p => (p 'or' q)))) => ((All (x,p)) => (All (x,(p 'or' q)))) is valid ) by Lm6, Th23, Th30;
then (All (x,p)) => (All (x,(p 'or' q))) is valid by CQC_THE1:65;
hence ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid by A1, Lm7; ::_thesis: verum
end;
theorem Th40: :: CQC_THE2:40
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid )
( not x in still_not-bound_in (Ex (x,p)) & not x in still_not-bound_in (Ex (x,q)) ) by Th6;
then A1: not x in still_not-bound_in ((Ex (x,p)) 'or' (Ex (x,q))) by Th9;
( p => (Ex (x,p)) is valid & q => (Ex (x,q)) is valid ) by Th15;
then (p 'or' q) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid by Lm4;
hence (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid by A1, Th19; ::_thesis: ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid
( All (x,(q => (p 'or' q))) is valid & (All (x,(q => (p 'or' q)))) => ((Ex (x,q)) => (Ex (x,(p 'or' q)))) is valid ) by Lm6, Th23, Th34;
then A2: (Ex (x,q)) => (Ex (x,(p 'or' q))) is valid by CQC_THE1:65;
( All (x,(p => (p 'or' q))) is valid & (All (x,(p => (p 'or' q)))) => ((Ex (x,p)) => (Ex (x,(p 'or' q)))) is valid ) by Lm6, Th23, Th34;
then (Ex (x,p)) => (Ex (x,(p 'or' q))) is valid by CQC_THE1:65;
hence ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid by A2, Lm7; ::_thesis: verum
end;
theorem Th41: :: CQC_THE2:41
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid
( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid ) by Th40;
hence (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid by Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:42
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid )
let x be bound_QC-variable of A; ::_thesis: ( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid )
(Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid by Th41;
hence ( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid ) by Lm15; ::_thesis: verum
end;
theorem Th43: :: CQC_THE2:43
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid
All (x,((p '&' q) => q)) is valid by Lm1, Th23;
then A1: (Ex (x,(p '&' q))) => (Ex (x,q)) is valid by Th35;
All (x,((p '&' q) => p)) is valid by Lm1, Th23;
then (Ex (x,(p '&' q))) => (Ex (x,p)) is valid by Th35;
hence (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid by A1, Lm3; ::_thesis: verum
end;
theorem :: CQC_THE2:44
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st Ex (x,(p '&' q)) is valid holds
(Ex (x,p)) '&' (Ex (x,q)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st Ex (x,(p '&' q)) is valid holds
(Ex (x,p)) '&' (Ex (x,q)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st Ex (x,(p '&' q)) is valid holds
(Ex (x,p)) '&' (Ex (x,q)) is valid
let x be bound_QC-variable of A; ::_thesis: ( Ex (x,(p '&' q)) is valid implies (Ex (x,p)) '&' (Ex (x,q)) is valid )
assume A1: Ex (x,(p '&' q)) is valid ; ::_thesis: (Ex (x,p)) '&' (Ex (x,q)) is valid
(Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid by Th43;
hence (Ex (x,p)) '&' (Ex (x,q)) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
theorem Th45: :: CQC_THE2:45
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid )
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid )
( All (x,(('not' ('not' p)) => p)) is valid & All (x,(p => ('not' ('not' p)))) is valid ) by Th23;
hence ( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid ) by Th31; ::_thesis: verum
end;
theorem :: CQC_THE2:46
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid
let x be bound_QC-variable of A; ::_thesis: (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid
( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid ) by Th45;
hence (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid by Lm14; ::_thesis: verum
end;
theorem Th47: :: CQC_THE2:47
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid )
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid )
( All (x,(('not' ('not' p)) => p)) is valid & All (x,(p => ('not' ('not' p)))) is valid ) by Th23;
hence ( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid ) by Th35; ::_thesis: verum
end;
theorem :: CQC_THE2:48
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid
let x be bound_QC-variable of A; ::_thesis: (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid
( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid ) by Th47;
hence (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid by Lm14; ::_thesis: verum
end;
theorem Th49: :: CQC_THE2:49
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid )
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid )
A1: (All (x,('not' ('not' p)))) => (All (x,p)) is valid by Th45;
A2: 'not' (Ex (x,('not' p))) = 'not' ('not' (All (x,('not' ('not' p))))) by QC_LANG2:def_5;
then ('not' (Ex (x,('not' p)))) => (All (x,('not' ('not' p)))) is valid ;
hence ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid by A1, LUKASI_1:42; ::_thesis: (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid
( (All (x,p)) => (All (x,('not' ('not' p)))) is valid & (All (x,('not' ('not' p)))) => ('not' ('not' (All (x,('not' ('not' p)))))) is valid ) by Th45;
hence (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid by A2, LUKASI_1:42; ::_thesis: verum
end;
theorem :: CQC_THE2:50
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid
let x be bound_QC-variable of A; ::_thesis: ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid
( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid ) by Th49;
hence ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid by Lm14; ::_thesis: verum
end;
theorem Th51: :: CQC_THE2:51
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid )
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid )
A1: Ex (x,('not' p)) = 'not' (All (x,('not' ('not' p)))) by QC_LANG2:def_5;
(All (x,('not' ('not' p)))) => (All (x,p)) is valid by Th45;
hence ('not' (All (x,p))) => (Ex (x,('not' p))) is valid by A1, LUKASI_1:52; ::_thesis: (Ex (x,('not' p))) => ('not' (All (x,p))) is valid
(All (x,p)) => (All (x,('not' ('not' p)))) is valid by Th45;
hence (Ex (x,('not' p))) => ('not' (All (x,p))) is valid by A1, LUKASI_1:52; ::_thesis: verum
end;
theorem :: CQC_THE2:52
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid
let x be bound_QC-variable of A; ::_thesis: ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid
( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid ) by Th51;
hence ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid by Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:53
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( ('not' (Ex (x,p))) => (All (x,('not' p))) is valid & (All (x,('not' p))) => ('not' (Ex (x,p))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( ('not' (Ex (x,p))) => (All (x,('not' p))) is valid & (All (x,('not' p))) => ('not' (Ex (x,p))) is valid )
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( ('not' (Ex (x,p))) => (All (x,('not' p))) is valid & (All (x,('not' p))) => ('not' (Ex (x,p))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( ('not' (Ex (x,p))) => (All (x,('not' p))) is valid & (All (x,('not' p))) => ('not' (Ex (x,p))) is valid )
A1: 'not' (Ex (x,p)) = 'not' ('not' (All (x,('not' p)))) by QC_LANG2:def_5;
hence ('not' (Ex (x,p))) => (All (x,('not' p))) is valid ; ::_thesis: (All (x,('not' p))) => ('not' (Ex (x,p))) is valid
thus (All (x,('not' p))) => ('not' (Ex (x,p))) is valid by A1; ::_thesis: verum
end;
theorem Th54: :: CQC_THE2:54
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid
let x be bound_QC-variable of A; ::_thesis: (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid
('not' ('not' (All (x,('not' p))))) => (All (x,('not' p))) is valid ;
then A1: ('not' (Ex (x,p))) => (All (x,('not' p))) is valid by QC_LANG2:def_5;
(All (x,('not' p))) => ('not' ('not' (All (x,('not' p))))) is valid ;
then (All (x,('not' p))) => ('not' (Ex (x,p))) is valid by QC_LANG2:def_5;
hence (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid by A1, Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:55
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds
( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds
( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid )
let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A holds
( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid )
let x, y be bound_QC-variable of A; ::_thesis: ( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid )
not y in still_not-bound_in (All (y,p)) by Th5;
then A1: not y in still_not-bound_in (All (x,(All (y,p)))) by Th5;
( All (x,((All (y,p)) => p)) is valid & (All (x,((All (y,p)) => p))) => ((All (x,(All (y,p)))) => (All (x,p))) is valid ) by Th23, Th30, CQC_THE1:66;
then (All (x,(All (y,p)))) => (All (x,p)) is valid by CQC_THE1:65;
hence (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid by A1, CQC_THE1:67; ::_thesis: (All (x,y,p)) => (All (y,x,p)) is valid
then (All (x,y,p)) => (All (y,(All (x,p)))) is valid by QC_LANG2:14;
hence (All (x,y,p)) => (All (y,x,p)) is valid by QC_LANG2:14; ::_thesis: verum
end;
theorem :: CQC_THE2:56
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
(All (x,(All (y,q)))) => (All (x,p)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
(All (x,(All (y,q)))) => (All (x,p)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
(All (x,(All (y,q)))) => (All (x,p)) is valid
let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
(All (x,(All (y,q)))) => (All (x,p)) is valid
let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not y in still_not-bound_in h implies (All (x,(All (y,q)))) => (All (x,p)) is valid )
assume ( p = h . x & q = h . y & not y in still_not-bound_in h ) ; ::_thesis: (All (x,(All (y,q)))) => (All (x,p)) is valid
then All (x,((All (y,q)) => p)) is valid by Th23, Th25;
hence (All (x,(All (y,q)))) => (All (x,p)) is valid by Th31; ::_thesis: verum
end;
theorem :: CQC_THE2:57
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds
( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid & (Ex (x,y,p)) => (Ex (y,x,p)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds
( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid & (Ex (x,y,p)) => (Ex (y,x,p)) is valid )
let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A holds
( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid & (Ex (x,y,p)) => (Ex (y,x,p)) is valid )
let x, y be bound_QC-variable of A; ::_thesis: ( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid & (Ex (x,y,p)) => (Ex (y,x,p)) is valid )
not x in still_not-bound_in (Ex (x,p)) by Th6;
then A1: not x in still_not-bound_in (Ex (y,(Ex (x,p)))) by Th6;
( All (y,(p => (Ex (x,p)))) is valid & (All (y,(p => (Ex (x,p))))) => ((Ex (y,p)) => (Ex (y,(Ex (x,p))))) is valid ) by Th15, Th23, Th34;
then (Ex (y,p)) => (Ex (y,(Ex (x,p)))) is valid by CQC_THE1:65;
hence (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid by A1, Th19; ::_thesis: (Ex (x,y,p)) => (Ex (y,x,p)) is valid
then (Ex (x,y,p)) => (Ex (y,(Ex (x,p)))) is valid by QC_LANG2:14;
hence (Ex (x,y,p)) => (Ex (y,x,p)) is valid by QC_LANG2:14; ::_thesis: verum
end;
theorem :: CQC_THE2:58
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (x,y,q)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (x,y,q)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (x,y,q)) is valid
let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (x,y,q)) is valid
let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not y in still_not-bound_in h implies (Ex (x,p)) => (Ex (x,y,q)) is valid )
assume ( p = h . x & q = h . y & not y in still_not-bound_in h ) ; ::_thesis: (Ex (x,p)) => (Ex (x,y,q)) is valid
then All (x,(p => (Ex (y,q)))) is valid by Th22, Th23;
then (Ex (x,p)) => (Ex (x,(Ex (y,q)))) is valid by Th35;
hence (Ex (x,p)) => (Ex (x,y,q)) is valid by QC_LANG2:14; ::_thesis: verum
end;
theorem :: CQC_THE2:59
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid
let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A holds (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid
let x, y be bound_QC-variable of A; ::_thesis: (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid
not x in still_not-bound_in (Ex (x,p)) by Th6;
then A1: not x in still_not-bound_in (All (y,(Ex (x,p)))) by Th5;
( All (y,(p => (Ex (x,p)))) is valid & (All (y,(p => (Ex (x,p))))) => ((All (y,p)) => (All (y,(Ex (x,p))))) is valid ) by Th15, Th23, Th30;
then (All (y,p)) => (All (y,(Ex (x,p)))) is valid by CQC_THE1:65;
hence (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid by A1, Th19; ::_thesis: verum
end;
theorem :: CQC_THE2:60
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds Ex (x,(p <=> p)) is valid by Lm13, Th16;
theorem Th61: :: CQC_THE2:61
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid )
(All (x,p)) => p is valid by CQC_THE1:66;
then A1: (p => q) => ((All (x,p)) => q) is valid by LUKASI_1:41;
( not x in still_not-bound_in (All (x,p)) & not x in still_not-bound_in (Ex (x,q)) ) by Th5, Th6;
then A2: not x in still_not-bound_in ((All (x,p)) => (Ex (x,q))) by Th7;
q => (Ex (x,q)) is valid by Th15;
then (p => q) => ((All (x,p)) => (Ex (x,q))) is valid by A1, Lm16;
hence (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid by A2, Th19; ::_thesis: ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid
(All (x,(p '&' ('not' q)))) => ((All (x,p)) '&' (All (x,('not' q)))) is valid by Th36;
then A3: ('not' ((All (x,p)) '&' (All (x,('not' q))))) => ('not' (All (x,(p '&' ('not' q))))) is valid by LUKASI_1:52;
('not' (All (x,(p '&' ('not' q))))) => (Ex (x,('not' (p '&' ('not' q))))) is valid by Th51;
then ('not' ((All (x,p)) '&' (All (x,('not' q))))) => (Ex (x,('not' (p '&' ('not' q))))) is valid by A3, LUKASI_1:42;
then A4: ('not' ((All (x,p)) '&' (All (x,('not' q))))) => (Ex (x,(p => q))) is valid by QC_LANG2:def_2;
(All (x,('not' q))) => ('not' ('not' (All (x,('not' q))))) is valid ;
then A5: ((All (x,p)) '&' (All (x,('not' q)))) => ((All (x,p)) '&' ('not' ('not' (All (x,('not' q)))))) is valid by Lm9;
(All (x,p)) => (Ex (x,q)) = (All (x,p)) => ('not' (All (x,('not' q)))) by QC_LANG2:def_5
.= 'not' ((All (x,p)) '&' ('not' ('not' (All (x,('not' q)))))) by QC_LANG2:def_2 ;
then ((All (x,p)) => (Ex (x,q))) => ('not' ((All (x,p)) '&' (All (x,('not' q))))) is valid by A5, LUKASI_1:52;
hence ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid by A4, LUKASI_1:42; ::_thesis: verum
end;
theorem Th62: :: CQC_THE2:62
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid
( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid ) by Th61;
hence (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid by Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:63
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid )
let x be bound_QC-variable of A; ::_thesis: ( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid )
(Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid by Th62;
hence ( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid ) by Lm15; ::_thesis: verum
end;
theorem Th64: :: CQC_THE2:64
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid
A1: (All (x,(p '&' q))) => (p '&' q) is valid by CQC_THE1:66;
A2: not x in still_not-bound_in (All (x,(p '&' q))) by Th5;
(p '&' q) => q is valid by Lm1;
then (All (x,(p '&' q))) => q is valid by A1, LUKASI_1:42;
then A3: (All (x,(p '&' q))) => (All (x,q)) is valid by A2, CQC_THE1:67;
(p '&' q) => p is valid by Lm1;
then (All (x,(p '&' q))) => p is valid by A1, LUKASI_1:42;
hence (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid by A3, Lm3; ::_thesis: verum
end;
theorem Th65: :: CQC_THE2:65
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid
let x be bound_QC-variable of A; ::_thesis: (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid
A1: (q '&' (All (x,p))) => ((All (x,p)) '&' q) is valid by CQC_THE1:64;
( All (x,((p '&' q) => (q '&' p))) is valid & (All (x,((p '&' q) => (q '&' p)))) => ((All (x,(p '&' q))) => (All (x,(q '&' p)))) is valid ) by Th23, Th30, CQC_THE1:64;
then A2: (All (x,(p '&' q))) => (All (x,(q '&' p))) is valid by CQC_THE1:65;
(All (x,(q '&' p))) => (q '&' (All (x,p))) is valid by Th64;
then (All (x,(p '&' q))) => (q '&' (All (x,p))) is valid by A2, LUKASI_1:42;
hence (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid by A1, LUKASI_1:42; ::_thesis: verum
end;
theorem Th66: :: CQC_THE2:66
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p '&' (All (x,q))) => (All (x,(p '&' q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p '&' (All (x,q))) => (All (x,(p '&' q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p '&' (All (x,q))) => (All (x,(p '&' q))) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid )
assume A1: not x in still_not-bound_in p ; ::_thesis: (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid
(All (x,q)) => q is valid by CQC_THE1:66;
then A2: (p '&' (All (x,q))) => (p '&' q) is valid by Lm9;
not x in still_not-bound_in (All (x,q)) by Th5;
then not x in still_not-bound_in (p '&' (All (x,q))) by A1, Th8;
hence (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid by A2, CQC_THE1:67; ::_thesis: verum
end;
theorem :: CQC_THE2:67
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p & p '&' (All (x,q)) is valid holds
All (x,(p '&' q)) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p & p '&' (All (x,q)) is valid holds
All (x,(p '&' q)) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p & p '&' (All (x,q)) is valid holds
All (x,(p '&' q)) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p & p '&' (All (x,q)) is valid implies All (x,(p '&' q)) is valid )
assume that
A1: not x in still_not-bound_in p and
A2: p '&' (All (x,q)) is valid ; ::_thesis: All (x,(p '&' q)) is valid
(p '&' (All (x,q))) => (All (x,(p '&' q))) is valid by A1, Th66;
hence All (x,(p '&' q)) is valid by A2, CQC_THE1:65; ::_thesis: verum
end;
theorem Th68: :: CQC_THE2:68
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid ) )
A1: not x in still_not-bound_in (All (x,(p 'or' q))) by Th5;
( (All (x,(p 'or' q))) => (p 'or' q) is valid & (p 'or' q) => (('not' p) => q) is valid ) by Lm11, CQC_THE1:66;
then (All (x,(p 'or' q))) => (('not' p) => q) is valid by LUKASI_1:42;
then A2: ((All (x,(p 'or' q))) '&' ('not' p)) => q is valid by Th1;
assume A3: not x in still_not-bound_in p ; ::_thesis: ( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid )
then not x in still_not-bound_in ('not' p) by QC_LANG3:7;
then not x in still_not-bound_in ((All (x,(p 'or' q))) '&' ('not' p)) by A1, Th8;
then ((All (x,(p 'or' q))) '&' ('not' p)) => (All (x,q)) is valid by A2, CQC_THE1:67;
then A4: (All (x,(p 'or' q))) => (('not' p) => (All (x,q))) is valid by Th3;
p => p is valid ;
then p => (All (x,p)) is valid by A3, CQC_THE1:67;
then A5: (p 'or' (All (x,q))) => ((All (x,p)) 'or' (All (x,q))) is valid by Lm10;
((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid by Th39;
hence (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid by A5, LUKASI_1:42; ::_thesis: (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid
(('not' p) => (All (x,q))) => (p 'or' (All (x,q))) is valid by Lm12;
hence (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid by A4, LUKASI_1:42; ::_thesis: verum
end;
theorem Th69: :: CQC_THE2:69
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid )
assume not x in still_not-bound_in p ; ::_thesis: (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid
then ( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid ) by Th68;
hence (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid by Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:70
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid ) )
assume not x in still_not-bound_in p ; ::_thesis: ( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid )
then (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid by Th69;
hence ( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid ) by Lm15; ::_thesis: verum
end;
theorem Th71: :: CQC_THE2:71
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) )
assume A1: not x in still_not-bound_in p ; ::_thesis: ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid )
(p '&' q) => (Ex (x,(p '&' q))) is valid by Th15;
then A2: q => (p => (Ex (x,(p '&' q)))) is valid by Th4;
not x in still_not-bound_in (Ex (x,(p '&' q))) by Th6;
then not x in still_not-bound_in (p => (Ex (x,(p '&' q)))) by A1, Th7;
then (Ex (x,q)) => (p => (Ex (x,(p '&' q)))) is valid by A2, Th19;
hence (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid by Th2; ::_thesis: (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid
q => (Ex (x,q)) is valid by Th15;
then A3: (p '&' q) => (p '&' (Ex (x,q))) is valid by Lm9;
not x in still_not-bound_in (Ex (x,q)) by Th6;
then not x in still_not-bound_in (p '&' (Ex (x,q))) by A1, Th8;
hence (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid by A3, Th19; ::_thesis: verum
end;
theorem Th72: :: CQC_THE2:72
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid )
assume not x in still_not-bound_in p ; ::_thesis: (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid
then ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) by Th71;
hence (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid by Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:73
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid ) )
assume not x in still_not-bound_in p ; ::_thesis: ( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid )
then (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid by Th72;
hence ( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid ) by Lm15; ::_thesis: verum
end;
Lm17: for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(All (x,(p => q))) => (p => (All (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(All (x,(p => q))) => (p => (All (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(All (x,(p => q))) => (p => (All (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (All (x,(p => q))) => (p => (All (x,q))) is valid )
assume not x in still_not-bound_in p ; ::_thesis: (All (x,(p => q))) => (p => (All (x,q))) is valid
then A1: p => (All (x,p)) is valid by Th24;
(All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid by Th30;
then (All (x,p)) => ((All (x,(p => q))) => (All (x,q))) is valid by LUKASI_1:44;
then p => ((All (x,(p => q))) => (All (x,q))) is valid by A1, LUKASI_1:42;
hence (All (x,(p => q))) => (p => (All (x,q))) is valid by LUKASI_1:44; ::_thesis: verum
end;
theorem Th74: :: CQC_THE2:74
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid ) )
assume A1: not x in still_not-bound_in p ; ::_thesis: ( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid )
hence (All (x,(p => q))) => (p => (All (x,q))) is valid by Lm17; ::_thesis: (p => (All (x,q))) => (All (x,(p => q))) is valid
not x in still_not-bound_in (All (x,q)) by Th5;
then not x in still_not-bound_in (p => (All (x,q))) by A1, Th7;
then A2: (All (x,((p => (All (x,q))) => (p => q)))) => ((p => (All (x,q))) => (All (x,(p => q)))) is valid by Lm17;
( All (x,(((All (x,q)) => q) => ((p => (All (x,q))) => (p => q)))) is valid & (All (x,(((All (x,q)) => q) => ((p => (All (x,q))) => (p => q))))) => ((All (x,((All (x,q)) => q))) => (All (x,((p => (All (x,q))) => (p => q))))) is valid ) by Th23, Th30;
then A3: (All (x,((All (x,q)) => q))) => (All (x,((p => (All (x,q))) => (p => q)))) is valid by CQC_THE1:65;
All (x,((All (x,q)) => q)) is valid by Th23, CQC_THE1:66;
then All (x,((p => (All (x,q))) => (p => q))) is valid by A3, CQC_THE1:65;
hence (p => (All (x,q))) => (All (x,(p => q))) is valid by A2, CQC_THE1:65; ::_thesis: verum
end;
theorem Th75: :: CQC_THE2:75
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p => (All (x,q))) <=> (All (x,(p => q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p => (All (x,q))) <=> (All (x,(p => q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p => (All (x,q))) <=> (All (x,(p => q))) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p => (All (x,q))) <=> (All (x,(p => q))) is valid )
assume not x in still_not-bound_in p ; ::_thesis: (p => (All (x,q))) <=> (All (x,(p => q))) is valid
then ( (p => (All (x,q))) => (All (x,(p => q))) is valid & (All (x,(p => q))) => (p => (All (x,q))) is valid ) by Th74;
hence (p => (All (x,q))) <=> (All (x,(p => q))) is valid by Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:76
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( All (x,(p => q)) is valid iff p => (All (x,q)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( All (x,(p => q)) is valid iff p => (All (x,q)) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( All (x,(p => q)) is valid iff p => (All (x,q)) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( All (x,(p => q)) is valid iff p => (All (x,q)) is valid ) )
assume not x in still_not-bound_in p ; ::_thesis: ( All (x,(p => q)) is valid iff p => (All (x,q)) is valid )
then (p => (All (x,q))) <=> (All (x,(p => q))) is valid by Th75;
hence ( All (x,(p => q)) is valid iff p => (All (x,q)) is valid ) by Lm15; ::_thesis: verum
end;
theorem Th77: :: CQC_THE2:77
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
(Ex (x,(p => q))) => ((All (x,p)) => q) is valid
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
(Ex (x,(p => q))) => ((All (x,p)) => q) is valid
let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds
(Ex (x,(p => q))) => ((All (x,p)) => q) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies (Ex (x,(p => q))) => ((All (x,p)) => q) is valid )
assume A1: not x in still_not-bound_in q ; ::_thesis: (Ex (x,(p => q))) => ((All (x,p)) => q) is valid
not x in still_not-bound_in (All (x,p)) by Th5;
then not x in still_not-bound_in ((All (x,p)) => q) by A1, Th7;
then A2: (Ex (x,((All (x,p)) => q))) => ((All (x,p)) => q) is valid by Th20;
(All (x,p)) => p is valid by CQC_THE1:66;
then A3: All (x,((p => q) => ((All (x,p)) => q))) is valid by Th23, LUKASI_1:41;
(All (x,((p => q) => ((All (x,p)) => q)))) => ((Ex (x,(p => q))) => (Ex (x,((All (x,p)) => q)))) is valid by Th34;
then (Ex (x,(p => q))) => (Ex (x,((All (x,p)) => q))) is valid by A3, CQC_THE1:65;
hence (Ex (x,(p => q))) => ((All (x,p)) => q) is valid by A2, LUKASI_1:42; ::_thesis: verum
end;
theorem Th78: :: CQC_THE2:78
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds ((All (x,p)) => q) => (Ex (x,(p => q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds ((All (x,p)) => q) => (Ex (x,(p => q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ((All (x,p)) => q) => (Ex (x,(p => q))) is valid
let x be bound_QC-variable of A; ::_thesis: ((All (x,p)) => q) => (Ex (x,(p => q))) is valid
(All (x,(p '&' ('not' q)))) => ((All (x,p)) '&' ('not' q)) is valid by Th65;
then ('not' ((All (x,p)) '&' ('not' q))) => ('not' (All (x,(p '&' ('not' q))))) is valid by LUKASI_1:52;
then A1: ((All (x,p)) => q) => ('not' (All (x,(p '&' ('not' q))))) is valid by QC_LANG2:def_2;
( All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q)))) is valid & (All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q))))) => ((All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q))))) is valid ) by Th23, Th30;
then (All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q)))) is valid by CQC_THE1:65;
then ('not' (All (x,(p '&' ('not' q))))) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by LUKASI_1:52;
then ((All (x,p)) => q) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by A1, LUKASI_1:42;
then ((All (x,p)) => q) => (Ex (x,('not' (p '&' ('not' q))))) is valid by QC_LANG2:def_5;
hence ((All (x,p)) => q) => (Ex (x,(p => q))) is valid by QC_LANG2:def_2; ::_thesis: verum
end;
theorem :: CQC_THE2:79
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid )
let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies ( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid ) )
assume not x in still_not-bound_in q ; ::_thesis: ( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid )
then A1: (Ex (x,(p => q))) => ((All (x,p)) => q) is valid by Th77;
((All (x,p)) => q) => (Ex (x,(p => q))) is valid by Th78;
then ((All (x,p)) => q) <=> (Ex (x,(p => q))) is valid by A1, Lm14;
hence ( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid ) by Lm15; ::_thesis: verum
end;
theorem Th80: :: CQC_THE2:80
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid )
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid )
let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies ( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid ) )
assume A1: not x in still_not-bound_in q ; ::_thesis: ( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid )
p => (Ex (x,p)) is valid by Th15;
then A2: ((Ex (x,p)) => q) => (p => q) is valid by LUKASI_1:41;
not x in still_not-bound_in (Ex (x,p)) by Th6;
then not x in still_not-bound_in ((Ex (x,p)) => q) by A1, Th7;
hence ((Ex (x,p)) => q) => (All (x,(p => q))) is valid by A2, CQC_THE1:67; ::_thesis: (All (x,(p => q))) => ((Ex (x,p)) => q) is valid
(All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid by Th34;
then A3: ((All (x,(p => q))) '&' (Ex (x,p))) => (Ex (x,q)) is valid by Th1;
(Ex (x,q)) => q is valid by A1, Th20;
then ((All (x,(p => q))) '&' (Ex (x,p))) => q is valid by A3, LUKASI_1:42;
hence (All (x,(p => q))) => ((Ex (x,p)) => q) is valid by Th3; ::_thesis: verum
end;
theorem Th81: :: CQC_THE2:81
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid
let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds
((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid )
assume not x in still_not-bound_in q ; ::_thesis: ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid
then ( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid ) by Th80;
hence ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid by Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:82
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid )
let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies ( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid ) )
assume not x in still_not-bound_in q ; ::_thesis: ( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid )
then ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid by Th81;
hence ( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid ) by Lm15; ::_thesis: verum
end;
theorem Th83: :: CQC_THE2:83
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid )
assume A1: not x in still_not-bound_in p ; ::_thesis: (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
not x in still_not-bound_in (Ex (x,q)) by Th6;
then not x in still_not-bound_in (p => (Ex (x,q))) by A1, Th7;
then A2: (Ex (x,(p => (Ex (x,q))))) => (p => (Ex (x,q))) is valid by Th20;
q => (Ex (x,q)) is valid by Th15;
then A3: All (x,((p => q) => (p => (Ex (x,q))))) is valid by Th23, LUKASI_1:51;
(All (x,((p => q) => (p => (Ex (x,q)))))) => ((Ex (x,(p => q))) => (Ex (x,(p => (Ex (x,q)))))) is valid by Th34;
then (Ex (x,(p => q))) => (Ex (x,(p => (Ex (x,q))))) is valid by A3, CQC_THE1:65;
hence (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid by A2, LUKASI_1:42; ::_thesis: verum
end;
theorem Th84: :: CQC_THE2:84
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid
let x be bound_QC-variable of A; ::_thesis: (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid
( All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q)))) is valid & (All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q))))) => ((All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q))))) is valid ) by Th23, Th30;
then (All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q)))) is valid by CQC_THE1:65;
then A1: ('not' (All (x,(p '&' ('not' q))))) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by LUKASI_1:52;
(All (x,('not' q))) <=> ('not' (Ex (x,q))) is valid by Th54;
then (All (x,('not' q))) => ('not' (Ex (x,q))) is valid by Lm14;
then (p '&' (All (x,('not' q)))) => (p '&' ('not' (Ex (x,q)))) is valid by Lm9;
then A2: ('not' (p '&' ('not' (Ex (x,q))))) => ('not' (p '&' (All (x,('not' q))))) is valid by LUKASI_1:52;
(All (x,(p '&' ('not' q)))) => (p '&' (All (x,('not' q)))) is valid by Th64;
then ('not' (p '&' (All (x,('not' q))))) => ('not' (All (x,(p '&' ('not' q))))) is valid by LUKASI_1:52;
then ('not' (p '&' ('not' (Ex (x,q))))) => ('not' (All (x,(p '&' ('not' q))))) is valid by A2, LUKASI_1:42;
then (p => (Ex (x,q))) => ('not' (All (x,(p '&' ('not' q))))) is valid by QC_LANG2:def_2;
then (p => (Ex (x,q))) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by A1, LUKASI_1:42;
then (p => (Ex (x,q))) => ('not' (All (x,('not' (p => q))))) is valid by QC_LANG2:def_2;
hence (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid by QC_LANG2:def_5; ::_thesis: verum
end;
theorem Th85: :: CQC_THE2:85
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid )
assume not x in still_not-bound_in p ; ::_thesis: (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid
then A1: (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid by Th83;
(p => (Ex (x,q))) => (Ex (x,(p => q))) is valid by Th84;
hence (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid by A1, Lm14; ::_thesis: verum
end;
theorem :: CQC_THE2:86
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid )
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid )
let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid ) )
assume not x in still_not-bound_in p ; ::_thesis: ( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid )
then (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid by Th85;
hence ( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid ) by Lm15; ::_thesis: verum
end;
theorem :: CQC_THE2:87
for A being QC-alphabet
for p being Element of CQC-WFF A holds {p} |- p
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds {p} |- p
let p be Element of CQC-WFF A; ::_thesis: {p} |- p
( p in {p} & {p} c= Cn {p} ) by CQC_THE1:17, TARSKI:def_1;
hence p in Cn {p} ; :: according to CQC_THE1:def_8 ::_thesis: verum
end;
theorem Th88: :: CQC_THE2:88
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds Cn ({p} \/ {q}) = Cn {(p '&' q)}
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds Cn ({p} \/ {q}) = Cn {(p '&' q)}
let p, q be Element of CQC-WFF A; ::_thesis: Cn ({p} \/ {q}) = Cn {(p '&' q)}
for t being Element of CQC-WFF A holds
( t in Cn ({p} \/ {q}) iff for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T )
proof
let t be Element of CQC-WFF A; ::_thesis: ( t in Cn ({p} \/ {q}) iff for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T )
thus ( t in Cn ({p} \/ {q}) implies for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T ) ::_thesis: ( ( for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T ) implies t in Cn ({p} \/ {q}) )
proof
assume A1: t in Cn ({p} \/ {q}) ; ::_thesis: for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T
let T be Subset of (CQC-WFF A); ::_thesis: ( T is being_a_theory & {(p '&' q)} c= T implies t in T )
assume that
A2: T is being_a_theory and
A3: {(p '&' q)} c= T ; ::_thesis: t in T
A4: ( p '&' q in T & TAUT A c= T ) by A2, A3, CQC_THE1:38, ZFMISC_1:31;
(p '&' q) => q in TAUT A by PROCAL_1:21;
then q in T by A2, A4, CQC_THE1:def_1;
then A5: {q} c= T by ZFMISC_1:31;
(p '&' q) => p in TAUT A by PROCAL_1:19;
then p in T by A2, A4, CQC_THE1:def_1;
then {p} c= T by ZFMISC_1:31;
then {p} \/ {q} c= T by A5, XBOOLE_1:8;
hence t in T by A1, A2, CQC_THE1:def_2; ::_thesis: verum
end;
thus ( ( for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T ) implies t in Cn ({p} \/ {q}) ) ::_thesis: verum
proof
assume A6: for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T ; ::_thesis: t in Cn ({p} \/ {q})
for T being Subset of (CQC-WFF A) st T is being_a_theory & {p} \/ {q} c= T holds
t in T
proof
let T be Subset of (CQC-WFF A); ::_thesis: ( T is being_a_theory & {p} \/ {q} c= T implies t in T )
assume that
A7: T is being_a_theory and
A8: {p} \/ {q} c= T ; ::_thesis: t in T
{p} c= {p} \/ {q} by XBOOLE_1:7;
then {p} c= T by A8, XBOOLE_1:1;
then A9: p in T by ZFMISC_1:31;
{q} c= {p} \/ {q} by XBOOLE_1:7;
then {q} c= T by A8, XBOOLE_1:1;
then A10: q in T by ZFMISC_1:31;
( p => (q => (p '&' q)) in TAUT A & TAUT A c= T ) by A7, CQC_THE1:38, PROCAL_1:28;
then q => (p '&' q) in T by A7, A9, CQC_THE1:def_1;
then p '&' q in T by A7, A10, CQC_THE1:def_1;
then {(p '&' q)} c= T by ZFMISC_1:31;
hence t in T by A6, A7; ::_thesis: verum
end;
hence t in Cn ({p} \/ {q}) by CQC_THE1:def_2; ::_thesis: verum
end;
end;
hence Cn ({p} \/ {q}) = Cn {(p '&' q)} by CQC_THE1:def_2; ::_thesis: verum
end;
theorem :: CQC_THE2:89
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds
( {p,q} |- r iff {(p '&' q)} |- r )
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds
( {p,q} |- r iff {(p '&' q)} |- r )
let p, q, r be Element of CQC-WFF A; ::_thesis: ( {p,q} |- r iff {(p '&' q)} |- r )
thus ( {p,q} |- r implies {(p '&' q)} |- r ) ::_thesis: ( {(p '&' q)} |- r implies {p,q} |- r )
proof
assume r in Cn {p,q} ; :: according to CQC_THE1:def_8 ::_thesis: {(p '&' q)} |- r
then r in Cn ({p} \/ {q}) by ENUMSET1:1;
hence r in Cn {(p '&' q)} by Th88; :: according to CQC_THE1:def_8 ::_thesis: verum
end;
assume r in Cn {(p '&' q)} ; :: according to CQC_THE1:def_8 ::_thesis: {p,q} |- r
then r in Cn ({p} \/ {q}) by Th88;
hence r in Cn {p,q} by ENUMSET1:1; :: according to CQC_THE1:def_8 ::_thesis: verum
end;
theorem Th90: :: CQC_THE2:90
for A being QC-alphabet
for X being Subset of (CQC-WFF A)
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st X |- p holds
X |- All (x,p)
proof
let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A)
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st X |- p holds
X |- All (x,p)
let X be Subset of (CQC-WFF A); ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A st X |- p holds
X |- All (x,p)
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st X |- p holds
X |- All (x,p)
let x be bound_QC-variable of A; ::_thesis: ( X |- p implies X |- All (x,p) )
A1: X |- p => (((All (x,p)) => (All (x,p))) => p) by CQC_THE1:59;
not x in still_not-bound_in (All (x,p)) by Th5;
then A2: not x in still_not-bound_in ((All (x,p)) => (All (x,p))) by Th7;
assume X |- p ; ::_thesis: X |- All (x,p)
then X |- ((All (x,p)) => (All (x,p))) => p by A1, CQC_THE1:55;
then A3: X |- ((All (x,p)) => (All (x,p))) => (All (x,p)) by A2, CQC_THE1:57;
X |- (All (x,p)) => (All (x,p)) by CQC_THE1:59;
hence X |- All (x,p) by A3, CQC_THE1:55; ::_thesis: verum
end;
theorem :: CQC_THE2:91
for A being QC-alphabet
for X being Subset of (CQC-WFF A)
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
X |- (All (x,(p => q))) => (p => (All (x,q))) by Th74, CQC_THE1:59;
theorem :: CQC_THE2:92
for A being QC-alphabet
for X being Subset of (CQC-WFF A)
for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds
X |- F => G
proof
let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A)
for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds
X |- F => G
let X be Subset of (CQC-WFF A); ::_thesis: for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds
X |- F => G
let F, G be Element of CQC-WFF A; ::_thesis: ( F is closed & X \/ {F} |- G implies X |- F => G )
assume that
A1: F is closed and
A2: X \/ {F} |- G ; ::_thesis: X |- F => G
G in Cn (X \/ {F}) by A2, CQC_THE1:def_8;
then consider f being FinSequence of [:(CQC-WFF A),Proof_Step_Kinds:] such that
A3: f is_a_proof_wrt X \/ {F} and
A4: Effect f = G by CQC_THE1:36;
f <> {} by A3, CQC_THE1:def_5;
then A5: G = (f . (len f)) `1 by A4, CQC_THE1:def_6;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies for H being Element of CQC-WFF A st H = (f . $1) `1 holds
X |- F => H );
A6: 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 A7: for k being Nat st k < n & 1 <= k & k <= len f holds
for H being Element of CQC-WFF A st H = (f . k) `1 holds
X |- F => H ; ::_thesis: S1[n]
assume that
A8: 1 <= n and
A9: n <= len f ; ::_thesis: for H being Element of CQC-WFF A st H = (f . n) `1 holds
X |- F => H
n in NAT by ORDINAL1:def_12;
then A10: f,n is_a_correct_step_wrt X \/ {F} by A3, A8, A9, CQC_THE1:def_5;
let H be Element of CQC-WFF A; ::_thesis: ( H = (f . n) `1 implies X |- F => H )
assume A11: H = (f . n) `1 ; ::_thesis: X |- F => H
now__::_thesis:_X_|-_F_=>_H
percases ( (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 A8, A9, CQC_THE1:23;
suppose (f . n) `2 = 0 ; ::_thesis: X |- F => H
then H in X \/ {F} by A11, A10, CQC_THE1:def_4;
then A12: ( H in X or H in {F} ) by XBOOLE_0:def_3;
now__::_thesis:_X_|-_F_=>_H
percases ( H in X or H = F ) by A12, TARSKI:def_1;
supposeA13: H in X ; ::_thesis: X |- F => H
X c= Cn X by CQC_THE1:17;
then A14: X |- H by A13, CQC_THE1:def_8;
X |- H => (F => H) by CQC_THE1:59;
hence X |- F => H by A14, CQC_THE1:55; ::_thesis: verum
end;
suppose H = F ; ::_thesis: X |- F => H
hence X |- F => H by CQC_THE1:59; ::_thesis: verum
end;
end;
end;
hence X |- F => H ; ::_thesis: verum
end;
suppose (f . n) `2 = 1 ; ::_thesis: X |- F => H
then H = VERUM A by A11, A10, CQC_THE1:def_4;
hence X |- F => H by CQC_THE1:59, LUKASI_1:46; ::_thesis: verum
end;
suppose (f . n) `2 = 2 ; ::_thesis: X |- F => H
then ex p being Element of CQC-WFF A st H = (('not' p) => p) => p by A11, A10, CQC_THE1:def_4;
then H is valid by CQC_THE1:61;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum
end;
suppose (f . n) `2 = 3 ; ::_thesis: X |- F => H
then ex p, q being Element of CQC-WFF A st H = p => (('not' p) => q) by A11, A10, CQC_THE1:def_4;
then H is valid by CQC_THE1:62;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum
end;
suppose (f . n) `2 = 4 ; ::_thesis: X |- F => H
then ex p, q, r being Element of CQC-WFF A st H = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A11, A10, CQC_THE1:def_4;
then H is valid by CQC_THE1:63;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum
end;
suppose (f . n) `2 = 5 ; ::_thesis: X |- F => H
then ex p, q being Element of CQC-WFF A st H = (p '&' q) => (q '&' p) by A11, A10, CQC_THE1:def_4;
then H is valid by CQC_THE1:64;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum
end;
suppose (f . n) `2 = 6 ; ::_thesis: X |- F => H
then ex p being Element of CQC-WFF A ex x being bound_QC-variable of A st H = (All (x,p)) => p by A11, A10, CQC_THE1:def_4;
then H is valid by CQC_THE1:66;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum
end;
suppose (f . n) `2 = 7 ; ::_thesis: X |- F => H
then consider i, j being Element of NAT , p, q being Element of CQC-WFF A such that
A15: 1 <= i and
A16: i < n and
A17: 1 <= j and
A18: j < i and
A19: p = (f . j) `1 and
A20: q = H and
A21: (f . i) `1 = p => q by A11, A10, CQC_THE1:def_4;
i <= len f by A9, A16, XXREAL_0:2;
then A22: X |- F => (p => q) by A7, A15, A16, A21;
X |- (F => (p => q)) => ((F => p) => (F => q)) by CQC_THE1:59;
then A23: X |- (F => p) => (F => q) by A22, CQC_THE1:55;
j < n by A16, A18, XXREAL_0:2;
then A24: j <= len f by A9, XXREAL_0:2;
j < n by A16, A18, XXREAL_0:2;
then X |- F => p by A7, A17, A19, A24;
hence X |- F => H by A20, A23, CQC_THE1:55; ::_thesis: verum
end;
suppose (f . n) `2 = 8 ; ::_thesis: X |- F => H
then consider i being Element of NAT , p, q being Element of CQC-WFF A, x being bound_QC-variable of A such that
A25: 1 <= i and
A26: i < n and
A27: (f . i) `1 = p => q and
A28: not x in still_not-bound_in p and
A29: H = p => (All (x,q)) by A11, A10, CQC_THE1:def_4;
A30: X |- (All (x,(p => q))) => (p => (All (x,q))) by A28, Th74, CQC_THE1:59;
not x in still_not-bound_in F by A1, QC_LANG1:def_31;
then A31: X |- (All (x,(F => (p => q)))) => (F => (All (x,(p => q)))) by Th74, CQC_THE1:59;
i <= len f by A9, A26, XXREAL_0:2;
then X |- All (x,(F => (p => q))) by A7, A25, A26, A27, Th90;
then X |- F => (All (x,(p => q))) by A31, CQC_THE1:55;
hence X |- F => H by A29, A30, LUKASI_1:59; ::_thesis: verum
end;
suppose (f . n) `2 = 9 ; ::_thesis: X |- F => H
then consider i being Element of NAT , x, y being bound_QC-variable of A, s being QC-formula of A such that
A32: 1 <= i and
A33: i < n and
A34: ( s . x in CQC-WFF A & s . y in CQC-WFF A ) and
A35: not x in still_not-bound_in s and
A36: s . x = (f . i) `1 and
A37: H = s . y by A11, A10, CQC_THE1:def_4;
reconsider s1 = s . x, s2 = s . y as Element of CQC-WFF A by A34;
A38: X |- (All (x,s1)) => s2 by A35, Th25, CQC_THE1:59;
not x in still_not-bound_in F by A1, QC_LANG1:def_31;
then A39: X |- (All (x,(F => s1))) => (F => (All (x,s1))) by Th74, CQC_THE1:59;
i <= len f by A9, A33, XXREAL_0:2;
then X |- All (x,(F => s1)) by A7, A32, A33, A36, Th90;
then X |- F => (All (x,s1)) by A39, CQC_THE1:55;
hence X |- F => H by A37, A38, LUKASI_1:59; ::_thesis: verum
end;
end;
end;
hence X |- F => H ; ::_thesis: verum
end;
A40: for n being Nat holds S1[n] from NAT_1:sch_4(A6);
1 <= len f by A3, CQC_THE1:25;
hence X |- F => G by A40, A5; ::_thesis: verum
end;