:: HILBERT2 semantic presentation
begin
theorem Th1: :: HILBERT2:1
for Z being set
for M being ManySortedSet of Z st ( for x being set st x in Z holds
M . x is ManySortedSet of x ) holds
for f being Function st f = Union M holds
dom f = union Z
proof
let Z be set ; ::_thesis: for M being ManySortedSet of Z st ( for x being set st x in Z holds
M . x is ManySortedSet of x ) holds
for f being Function st f = Union M holds
dom f = union Z
let M be ManySortedSet of Z; ::_thesis: ( ( for x being set st x in Z holds
M . x is ManySortedSet of x ) implies for f being Function st f = Union M holds
dom f = union Z )
assume A1: for x being set st x in Z holds
M . x is ManySortedSet of x ; ::_thesis: for f being Function st f = Union M holds
dom f = union Z
let f be Function; ::_thesis: ( f = Union M implies dom f = union Z )
assume f = Union M ; ::_thesis: dom f = union Z
then A2: f = union (rng M) by CARD_3:def_4;
for x being set holds
( x in dom f iff ex Y being set st
( x in Y & Y in Z ) )
proof
let x be set ; ::_thesis: ( x in dom f iff ex Y being set st
( x in Y & Y in Z ) )
thus ( x in dom f implies ex Y being set st
( x in Y & Y in Z ) ) ::_thesis: ( ex Y being set st
( x in Y & Y in Z ) implies x in dom f )
proof
assume x in dom f ; ::_thesis: ex Y being set st
( x in Y & Y in Z )
then [x,(f . x)] in f by FUNCT_1:def_2;
then consider g being set such that
A3: [x,(f . x)] in g and
A4: g in rng M by A2, TARSKI:def_4;
consider a being set such that
A5: a in dom M and
A6: g = M . a by A4, FUNCT_1:def_3;
A7: a in Z by A5, PARTFUN1:def_2;
then reconsider g = g as ManySortedSet of a by A1, A6;
take dom g ; ::_thesis: ( x in dom g & dom g in Z )
thus x in dom g by A3, FUNCT_1:1; ::_thesis: dom g in Z
thus dom g in Z by A7, PARTFUN1:def_2; ::_thesis: verum
end;
given Y being set such that A8: x in Y and
A9: Y in Z ; ::_thesis: x in dom f
reconsider g = M . Y as ManySortedSet of Y by A1, A9;
Y = dom g by PARTFUN1:def_2;
then A10: [x,(g . x)] in g by A8, FUNCT_1:1;
Z = dom M by PARTFUN1:def_2;
then g in rng M by A9, FUNCT_1:def_3;
then [x,(g . x)] in f by A2, A10, TARSKI:def_4;
hence x in dom f by FUNCT_1:1; ::_thesis: verum
end;
hence dom f = union Z by TARSKI:def_4; ::_thesis: verum
end;
theorem Th2: :: HILBERT2:2
for x, y being set
for f, g being FinSequence st <*x*> ^ f = <*y*> ^ g holds
f = g
proof
let x, y be set ; ::_thesis: for f, g being FinSequence st <*x*> ^ f = <*y*> ^ g holds
f = g
let f, g be FinSequence; ::_thesis: ( <*x*> ^ f = <*y*> ^ g implies f = g )
assume A1: <*x*> ^ f = <*y*> ^ g ; ::_thesis: f = g
then x = (<*y*> ^ g) . 1 by FINSEQ_1:41
.= y by FINSEQ_1:41 ;
hence f = g by A1, FINSEQ_1:33; ::_thesis: verum
end;
theorem Th3: :: HILBERT2:3
for x, X being set st <*x*> is FinSequence of X holds
x in X
proof
let x, X be set ; ::_thesis: ( <*x*> is FinSequence of X implies x in X )
A1: rng <*x*> = {x} by FINSEQ_1:38;
assume <*x*> is FinSequence of X ; ::_thesis: x in X
then {x} c= X by A1, FINSEQ_1:def_4;
hence x in X by ZFMISC_1:31; ::_thesis: verum
end;
theorem Th4: :: HILBERT2:4
for X being set
for f being FinSequence of X st f <> {} holds
ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*>
proof
let X be set ; ::_thesis: for f being FinSequence of X st f <> {} holds
ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*>
let f be FinSequence of X; ::_thesis: ( f <> {} implies ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*> )
assume f <> {} ; ::_thesis: ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*>
then consider q being FinSequence, x being set such that
A1: f = q ^ <*x*> by FINSEQ_1:46;
reconsider q = q as FinSequence of X by A1, FINSEQ_1:36;
take q ; ::_thesis: ex d being Element of X st f = q ^ <*d*>
take x ; ::_thesis: ( x is Element of X & f = q ^ <*x*> )
<*x*> is FinSequence of X by A1, FINSEQ_1:36;
hence x is Element of X by Th3; ::_thesis: f = q ^ <*x*>
thus f = q ^ <*x*> by A1; ::_thesis: verum
end;
theorem Th5: :: HILBERT2:5
for x being set
for T1, T2 being Tree holds
( <*x*> in tree (T1,T2) iff ( x = 0 or x = 1 ) )
proof
let x be set ; ::_thesis: for T1, T2 being Tree holds
( <*x*> in tree (T1,T2) iff ( x = 0 or x = 1 ) )
let T1, T2 be Tree; ::_thesis: ( <*x*> in tree (T1,T2) iff ( x = 0 or x = 1 ) )
A1: ( len <*T1,T2*> = 2 & tree (T1,T2) = tree <*T1,T2*> ) by FINSEQ_1:44, TREES_3:def_17;
thus ( not <*x*> in tree (T1,T2) or x = 0 or x = 1 ) ::_thesis: ( ( x = 0 or x = 1 ) implies <*x*> in tree (T1,T2) )
proof
assume <*x*> in tree (T1,T2) ; ::_thesis: ( x = 0 or x = 1 )
then consider n being Element of NAT , q being FinSequence such that
A2: n < 2 and
q in <*T1,T2*> . (n + 1) and
A3: <*x*> = <*n*> ^ q by A1, TREES_3:def_15;
x = <*x*> . 1 by FINSEQ_1:40
.= n by A3, FINSEQ_1:41 ;
hence ( x = 0 or x = 1 ) by A2, NAT_1:23; ::_thesis: verum
end;
assume A4: ( x = 0 or x = 1 ) ; ::_thesis: <*x*> in tree (T1,T2)
then reconsider n = x as Element of NAT ;
( <*T1,T2*> . (n + 1) = T1 or <*T1,T2*> . (n + 1) = T2 ) by A4, FINSEQ_1:44;
then A5: {} in <*T1,T2*> . (n + 1) by TREES_1:22;
<*n*> = <*n*> ^ {} by FINSEQ_1:34;
hence <*x*> in tree (T1,T2) by A1, A4, A5, TREES_3:def_15; ::_thesis: verum
end;
scheme :: HILBERT2:sch 1
InTreeInd{ F1() -> Tree, P1[ set ] } :
for f being Element of F1() holds P1[f]
provided
A1: P1[ <*> NAT] and
A2: for f being Element of F1() st P1[f] holds
for n being Element of NAT st f ^ <*n*> in F1() holds
P1[f ^ <*n*>]
proof
defpred S1[ FinSequence] means ( $1 in F1() implies P1[$1] );
A3: for p being FinSequence
for x being set st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence; ::_thesis: for x being set st S1[p] holds
S1[p ^ <*x*>]
let x be set ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A4: S1[p] ; ::_thesis: S1[p ^ <*x*>]
assume A5: p ^ <*x*> in F1() ; ::_thesis: P1[p ^ <*x*>]
then reconsider h = p ^ <*x*> as FinSequence of NAT by TREES_1:19;
consider g being FinSequence of NAT , n being Element of NAT such that
A6: h = g ^ <*n*> by Th4;
A7: g = p by A6, FINSEQ_2:17;
reconsider g = g as Element of F1() by A5, A6, TREES_1:21;
P1[g] by A4, A7;
hence P1[p ^ <*x*>] by A2, A5, A6; ::_thesis: verum
end;
A8: S1[ {} ] by A1;
for p being FinSequence holds S1[p] from FINSEQ_1:sch_3(A8, A3);
hence for f being Element of F1() holds P1[f] ; ::_thesis: verum
end;
theorem Th6: :: HILBERT2:6
for x being set
for T1, T2 being DecoratedTree holds (x -tree (T1,T2)) . {} = x
proof
let x be set ; ::_thesis: for T1, T2 being DecoratedTree holds (x -tree (T1,T2)) . {} = x
let T1, T2 be DecoratedTree; ::_thesis: (x -tree (T1,T2)) . {} = x
x -tree (T1,T2) = x -tree <*T1,T2*> by TREES_4:def_6;
hence (x -tree (T1,T2)) . {} = x by TREES_4:def_4; ::_thesis: verum
end;
theorem Th7: :: HILBERT2:7
for x being set
for T1, T2 being DecoratedTree holds
( (x -tree (T1,T2)) . <*0*> = T1 . {} & (x -tree (T1,T2)) . <*1*> = T2 . {} )
proof
let x be set ; ::_thesis: for T1, T2 being DecoratedTree holds
( (x -tree (T1,T2)) . <*0*> = T1 . {} & (x -tree (T1,T2)) . <*1*> = T2 . {} )
let T1, T2 be DecoratedTree; ::_thesis: ( (x -tree (T1,T2)) . <*0*> = T1 . {} & (x -tree (T1,T2)) . <*1*> = T2 . {} )
A1: len <*T1,T2*> = 2 by FINSEQ_1:44;
reconsider w = {} as Node of T1 by TREES_1:22;
A2: <*T1,T2*> . (0 + 1) = T1 by FINSEQ_1:44;
thus (x -tree (T1,T2)) . <*0*> = (x -tree <*T1,T2*>) . <*0*> by TREES_4:def_6
.= (x -tree <*T1,T2*>) . (<*0*> ^ w) by FINSEQ_1:34
.= T1 . {} by A1, A2, TREES_4:12 ; ::_thesis: (x -tree (T1,T2)) . <*1*> = T2 . {}
reconsider w = {} as Node of T2 by TREES_1:22;
A3: <*T1,T2*> . (1 + 1) = T2 by FINSEQ_1:44;
thus (x -tree (T1,T2)) . <*1*> = (x -tree <*T1,T2*>) . <*1*> by TREES_4:def_6
.= (x -tree <*T1,T2*>) . (<*1*> ^ w) by FINSEQ_1:34
.= T2 . {} by A1, A3, TREES_4:12 ; ::_thesis: verum
end;
theorem Th8: :: HILBERT2:8
for x being set
for T1, T2 being DecoratedTree holds
( (x -tree (T1,T2)) | <*0*> = T1 & (x -tree (T1,T2)) | <*1*> = T2 )
proof
let x be set ; ::_thesis: for T1, T2 being DecoratedTree holds
( (x -tree (T1,T2)) | <*0*> = T1 & (x -tree (T1,T2)) | <*1*> = T2 )
let T1, T2 be DecoratedTree; ::_thesis: ( (x -tree (T1,T2)) | <*0*> = T1 & (x -tree (T1,T2)) | <*1*> = T2 )
A1: len <*T1,T2*> = 2 by FINSEQ_1:44;
thus (x -tree (T1,T2)) | <*0*> = (x -tree <*T1,T2*>) | <*0*> by TREES_4:def_6
.= <*T1,T2*> . (0 + 1) by A1, TREES_4:def_4
.= T1 by FINSEQ_1:44 ; ::_thesis: (x -tree (T1,T2)) | <*1*> = T2
thus (x -tree (T1,T2)) | <*1*> = (x -tree <*T1,T2*>) | <*1*> by TREES_4:def_6
.= <*T1,T2*> . (1 + 1) by A1, TREES_4:def_4
.= T2 by FINSEQ_1:44 ; ::_thesis: verum
end;
registration
let x be set ;
let p be non empty DTree-yielding FinSequence;
clusterx -tree p -> non root ;
coherence
not x -tree p is trivial
proof
assume x -tree p is root ; ::_thesis: contradiction
then A1: dom (x -tree p) = tree {} by TREES_3:52, TREES_9:def_1;
ex q being DTree-yielding FinSequence st
( p = q & dom (x -tree p) = tree (doms q) ) by TREES_4:def_4;
then ( dom p <> {} & doms p = {} ) by A1, TREES_3:50;
hence contradiction by RELAT_1:38, TREES_3:37; ::_thesis: verum
end;
end;
registration
let x be set ;
let T1 be DecoratedTree;
clusterx -tree T1 -> non root ;
coherence
not x -tree T1 is trivial
proof
x -tree T1 = x -tree <*T1*> by TREES_4:def_5;
hence not x -tree T1 is trivial ; ::_thesis: verum
end;
let T2 be DecoratedTree;
clusterx -tree (T1,T2) -> non root ;
coherence
not x -tree (T1,T2) is trivial
proof
x -tree (T1,T2) = x -tree <*T1,T2*> by TREES_4:def_6;
hence not x -tree (T1,T2) is trivial ; ::_thesis: verum
end;
end;
begin
definition
let n be Element of NAT ;
func prop n -> Element of HP-WFF equals :: HILBERT2:def 1
<*(3 + n)*>;
coherence
<*(3 + n)*> is Element of HP-WFF by HILBERT1:def_4;
end;
:: deftheorem defines prop HILBERT2:def_1_:_
for n being Element of NAT holds prop n = <*(3 + n)*>;
definition
let D be set ;
redefine attr D is with_VERUM means :Def2: :: HILBERT2:def 2
VERUM in D;
compatibility
( D is with_VERUM iff VERUM in D ) by HILBERT1:def_1;
redefine attr D is with_propositional_variables means :: HILBERT2:def 3
for n being Element of NAT holds prop n in D;
compatibility
( D is with_propositional_variables iff for n being Element of NAT holds prop n in D )
proof
thus ( D is with_propositional_variables implies for n being Element of NAT holds prop n in D ) by HILBERT1:def_4; ::_thesis: ( ( for n being Element of NAT holds prop n in D ) implies D is with_propositional_variables )
assume A1: for n being Element of NAT holds prop n in D ; ::_thesis: D is with_propositional_variables
let n be Element of NAT ; :: according to HILBERT1:def_4 ::_thesis: <*(3 + n)*> in D
prop n = <*(3 + n)*> ;
hence <*(3 + n)*> in D by A1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines with_VERUM HILBERT2:def_2_:_
for D being set holds
( D is with_VERUM iff VERUM in D );
:: deftheorem defines with_propositional_variables HILBERT2:def_3_:_
for D being set holds
( D is with_propositional_variables iff for n being Element of NAT holds prop n in D );
definition
let D be Subset of HP-WFF;
redefine attr D is with_implication means :: HILBERT2:def 4
for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D;
compatibility
( D is with_implication iff for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D )
proof
thus ( D is with_implication implies for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D ) by HILBERT1:def_2; ::_thesis: ( ( for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D ) implies D is with_implication )
assume A1: for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D ; ::_thesis: D is with_implication
let p, q be FinSequence; :: according to HILBERT1:def_2 ::_thesis: ( not p in D or not q in D or (<*1*> ^ p) ^ q in D )
assume A2: ( p in D & q in D ) ; ::_thesis: (<*1*> ^ p) ^ q in D
then reconsider p9 = p, q9 = q as Element of HP-WFF ;
p9 => q9 in D by A1, A2;
hence (<*1*> ^ p) ^ q in D ; ::_thesis: verum
end;
redefine attr D is with_conjunction means :: HILBERT2:def 5
for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D;
compatibility
( D is with_conjunction iff for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D )
proof
thus ( D is with_conjunction implies for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D ) by HILBERT1:def_3; ::_thesis: ( ( for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D ) implies D is with_conjunction )
assume A3: for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D ; ::_thesis: D is with_conjunction
let p, q be FinSequence; :: according to HILBERT1:def_3 ::_thesis: ( not p in D or not q in D or (<*2*> ^ p) ^ q in D )
assume A4: ( p in D & q in D ) ; ::_thesis: (<*2*> ^ p) ^ q in D
then reconsider p9 = p, q9 = q as Element of HP-WFF ;
p9 '&' q9 in D by A3, A4;
hence (<*2*> ^ p) ^ q in D ; ::_thesis: verum
end;
end;
:: deftheorem defines with_implication HILBERT2:def_4_:_
for D being Subset of HP-WFF holds
( D is with_implication iff for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D );
:: deftheorem defines with_conjunction HILBERT2:def_5_:_
for D being Subset of HP-WFF holds
( D is with_conjunction iff for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D );
definition
let p be Element of HP-WFF ;
attrp is conjunctive means :Def6: :: HILBERT2:def 6
ex r, s being Element of HP-WFF st p = r '&' s;
attrp is conditional means :Def7: :: HILBERT2:def 7
ex r, s being Element of HP-WFF st p = r => s;
attrp is simple means :Def8: :: HILBERT2:def 8
ex n being Element of NAT st p = prop n;
end;
:: deftheorem Def6 defines conjunctive HILBERT2:def_6_:_
for p being Element of HP-WFF holds
( p is conjunctive iff ex r, s being Element of HP-WFF st p = r '&' s );
:: deftheorem Def7 defines conditional HILBERT2:def_7_:_
for p being Element of HP-WFF holds
( p is conditional iff ex r, s being Element of HP-WFF st p = r => s );
:: deftheorem Def8 defines simple HILBERT2:def_8_:_
for p being Element of HP-WFF holds
( p is simple iff ex n being Element of NAT st p = prop n );
scheme :: HILBERT2:sch 2
HPInd{ P1[ set ] } :
for r being Element of HP-WFF holds P1[r]
provided
A1: P1[ VERUM ] and
A2: for n being Element of NAT holds P1[ prop n] and
A3: for r, s being Element of HP-WFF st P1[r] & P1[s] holds
( P1[r '&' s] & P1[r => s] )
proof
set X = { p where p is Element of HP-WFF : P1[p] } ;
{ p where p is Element of HP-WFF : P1[p] } c= HP-WFF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Element of HP-WFF : P1[p] } or x in HP-WFF )
assume x in { p where p is Element of HP-WFF : P1[p] } ; ::_thesis: x in HP-WFF
then ex p being Element of HP-WFF st
( x = p & P1[p] ) ;
hence x in HP-WFF ; ::_thesis: verum
end;
then reconsider X = { p where p is Element of HP-WFF : P1[p] } as Subset of HP-WFF ;
let r be Element of HP-WFF ; ::_thesis: P1[r]
A4: r in HP-WFF ;
A5: X is with_propositional_variables
proof
let n be Element of NAT ; :: according to HILBERT2:def_3 ::_thesis: prop n in X
P1[ prop n] by A2;
hence prop n in X ; ::_thesis: verum
end;
A6: X is with_implication
proof
let p be Element of HP-WFF ; :: according to HILBERT2:def_4 ::_thesis: for q being Element of HP-WFF st p in X & q in X holds
p => q in X
let q be Element of HP-WFF ; ::_thesis: ( p in X & q in X implies p => q in X )
assume p in X ; ::_thesis: ( not q in X or p => q in X )
then A7: ex x being Element of HP-WFF st
( p = x & P1[x] ) ;
assume q in X ; ::_thesis: p => q in X
then ex x being Element of HP-WFF st
( q = x & P1[x] ) ;
then P1[p => q] by A3, A7;
hence p => q in X ; ::_thesis: verum
end;
A8: HP-WFF c= NAT * by HILBERT1:def_5;
A9: X c= NAT *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in NAT * )
assume x in X ; ::_thesis: x in NAT *
then x in HP-WFF ;
hence x in NAT * by A8; ::_thesis: verum
end;
A10: X is with_conjunction
proof
let p be Element of HP-WFF ; :: according to HILBERT2:def_5 ::_thesis: for q being Element of HP-WFF st p in X & q in X holds
p '&' q in X
let q be Element of HP-WFF ; ::_thesis: ( p in X & q in X implies p '&' q in X )
assume p in X ; ::_thesis: ( not q in X or p '&' q in X )
then A11: ex x being Element of HP-WFF st
( p = x & P1[x] ) ;
assume q in X ; ::_thesis: p '&' q in X
then ex x being Element of HP-WFF st
( q = x & P1[x] ) ;
then P1[p '&' q] by A3, A11;
hence p '&' q in X ; ::_thesis: verum
end;
VERUM in X by A1;
then X is with_VERUM by Def2;
then HP-WFF c= X by A9, A6, A10, A5, HILBERT1:def_6;
then r in X by A4;
then ex p being Element of HP-WFF st
( r = p & P1[p] ) ;
hence P1[r] ; ::_thesis: verum
end;
theorem Th9: :: HILBERT2:9
for p being Element of HP-WFF holds
( p is conjunctive or p is conditional or p is simple or p = VERUM )
proof
let p be Element of HP-WFF ; ::_thesis: ( p is conjunctive or p is conditional or p is simple or p = VERUM )
defpred S1[ Element of HP-WFF ] means ( $1 is conjunctive or $1 is conditional or $1 is simple or $1 = VERUM );
A1: S1[ VERUM ] ;
A2: for n being Element of NAT holds S1[ prop n] by Def8;
A3: for r, s being Element of HP-WFF st S1[r] & S1[s] holds
( S1[r '&' s] & S1[r => s] ) by Def6, Def7;
for p being Element of HP-WFF holds S1[p] from HILBERT2:sch_2(A1, A2, A3);
hence ( p is conjunctive or p is conditional or p is simple or p = VERUM ) ; ::_thesis: verum
end;
theorem Th10: :: HILBERT2:10
for p being Element of HP-WFF holds len p >= 1
proof
let p be Element of HP-WFF ; ::_thesis: len p >= 1
percases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;
suppose p is conjunctive ; ::_thesis: len p >= 1
then consider r, s being Element of HP-WFF such that
A1: p = r '&' s by Def6;
len p = len (<*2*> ^ (r ^ s)) by A1, FINSEQ_1:32
.= (len <*2*>) + (len (r ^ s)) by FINSEQ_1:22
.= 1 + (len (r ^ s)) by FINSEQ_1:39 ;
hence len p >= 1 by NAT_1:11; ::_thesis: verum
end;
suppose p is conditional ; ::_thesis: len p >= 1
then consider r, s being Element of HP-WFF such that
A2: p = r => s by Def7;
len p = len (<*1*> ^ (r ^ s)) by A2, FINSEQ_1:32
.= (len <*1*>) + (len (r ^ s)) by FINSEQ_1:22
.= 1 + (len (r ^ s)) by FINSEQ_1:39 ;
hence len p >= 1 by NAT_1:11; ::_thesis: verum
end;
suppose p is simple ; ::_thesis: len p >= 1
then ex n being Element of NAT st p = prop n by Def8;
hence len p >= 1 by FINSEQ_1:39; ::_thesis: verum
end;
suppose p = VERUM ; ::_thesis: len p >= 1
hence len p >= 1 by FINSEQ_1:39; ::_thesis: verum
end;
end;
end;
theorem Th11: :: HILBERT2:11
for p being Element of HP-WFF st p . 1 = 1 holds
p is conditional
proof
let p be Element of HP-WFF ; ::_thesis: ( p . 1 = 1 implies p is conditional )
assume A1: p . 1 = 1 ; ::_thesis: p is conditional
percases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;
suppose p is conjunctive ; ::_thesis: p is conditional
then consider r, s being Element of HP-WFF such that
A2: p = r '&' s by Def6;
p = <*2*> ^ (r ^ s) by A2, FINSEQ_1:32;
hence p is conditional by A1, FINSEQ_1:41; ::_thesis: verum
end;
suppose p is conditional ; ::_thesis: p is conditional
hence p is conditional ; ::_thesis: verum
end;
suppose p is simple ; ::_thesis: p is conditional
then consider n being Element of NAT such that
A3: p = prop n by Def8;
1 + 0 = 1 + (2 + n) by A1, A3, FINSEQ_1:40;
hence p is conditional ; ::_thesis: verum
end;
suppose p = VERUM ; ::_thesis: p is conditional
hence p is conditional by A1, FINSEQ_1:40; ::_thesis: verum
end;
end;
end;
theorem Th12: :: HILBERT2:12
for p being Element of HP-WFF st p . 1 = 2 holds
p is conjunctive
proof
let p be Element of HP-WFF ; ::_thesis: ( p . 1 = 2 implies p is conjunctive )
assume A1: p . 1 = 2 ; ::_thesis: p is conjunctive
percases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;
suppose p is conjunctive ; ::_thesis: p is conjunctive
hence p is conjunctive ; ::_thesis: verum
end;
suppose p is conditional ; ::_thesis: p is conjunctive
then consider r, s being Element of HP-WFF such that
A2: p = r => s by Def7;
p = <*1*> ^ (r ^ s) by A2, FINSEQ_1:32;
hence p is conjunctive by A1, FINSEQ_1:41; ::_thesis: verum
end;
suppose p is simple ; ::_thesis: p is conjunctive
then consider n being Element of NAT such that
A3: p = prop n by Def8;
2 + 0 = 2 + (1 + n) by A1, A3, FINSEQ_1:40;
hence p is conjunctive ; ::_thesis: verum
end;
suppose p = VERUM ; ::_thesis: p is conjunctive
hence p is conjunctive by A1, FINSEQ_1:40; ::_thesis: verum
end;
end;
end;
theorem :: HILBERT2:13
for n being Element of NAT
for p being Element of HP-WFF st p . 1 = 3 + n holds
p is simple
proof
let n be Element of NAT ; ::_thesis: for p being Element of HP-WFF st p . 1 = 3 + n holds
p is simple
let p be Element of HP-WFF ; ::_thesis: ( p . 1 = 3 + n implies p is simple )
assume A1: p . 1 = 3 + n ; ::_thesis: p is simple
percases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;
suppose p is conjunctive ; ::_thesis: p is simple
then consider r, s being Element of HP-WFF such that
A2: p = r '&' s by Def6;
p = <*2*> ^ (r ^ s) by A2, FINSEQ_1:32;
then 2 + 0 = 2 + (1 + n) by A1, FINSEQ_1:41;
hence p is simple ; ::_thesis: verum
end;
suppose p is conditional ; ::_thesis: p is simple
then consider r, s being Element of HP-WFF such that
A3: p = r => s by Def7;
p = <*1*> ^ (r ^ s) by A3, FINSEQ_1:32;
then 1 + 0 = 1 + (2 + n) by A1, FINSEQ_1:41;
hence p is simple ; ::_thesis: verum
end;
suppose p is simple ; ::_thesis: p is simple
hence p is simple ; ::_thesis: verum
end;
suppose p = VERUM ; ::_thesis: p is simple
hence p is simple by A1, FINSEQ_1:40; ::_thesis: verum
end;
end;
end;
theorem :: HILBERT2:14
for p being Element of HP-WFF st p . 1 = 0 holds
p = VERUM
proof
let p be Element of HP-WFF ; ::_thesis: ( p . 1 = 0 implies p = VERUM )
assume A1: p . 1 = 0 ; ::_thesis: p = VERUM
percases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;
suppose p is conjunctive ; ::_thesis: p = VERUM
then consider r, s being Element of HP-WFF such that
A2: p = r '&' s by Def6;
p = <*2*> ^ (r ^ s) by A2, FINSEQ_1:32;
hence p = VERUM by A1, FINSEQ_1:41; ::_thesis: verum
end;
suppose p is conditional ; ::_thesis: p = VERUM
then consider r, s being Element of HP-WFF such that
A3: p = r => s by Def7;
p = <*1*> ^ (r ^ s) by A3, FINSEQ_1:32;
hence p = VERUM by A1, FINSEQ_1:41; ::_thesis: verum
end;
suppose p is simple ; ::_thesis: p = VERUM
then ex n being Element of NAT st p = prop n by Def8;
hence p = VERUM by A1, FINSEQ_1:40; ::_thesis: verum
end;
suppose p = VERUM ; ::_thesis: p = VERUM
hence p = VERUM ; ::_thesis: verum
end;
end;
end;
theorem Th15: :: HILBERT2:15
for p, q being Element of HP-WFF holds
( len p < len (p '&' q) & len q < len (p '&' q) )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( len p < len (p '&' q) & len q < len (p '&' q) )
len (p '&' q) = (len (<*2*> ^ p)) + (len q) by FINSEQ_1:22
.= ((len <*2*>) + (len p)) + (len q) by FINSEQ_1:22
.= (1 + (len p)) + (len q) by FINSEQ_1:39
.= 1 + ((len p) + (len q)) ;
then A1: (len p) + (len q) < len (p '&' q) by XREAL_1:29;
( len p <= (len p) + (len q) & len q <= (len p) + (len q) ) by NAT_1:11;
hence ( len p < len (p '&' q) & len q < len (p '&' q) ) by A1, XXREAL_0:2; ::_thesis: verum
end;
theorem Th16: :: HILBERT2:16
for p, q being Element of HP-WFF holds
( len p < len (p => q) & len q < len (p => q) )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( len p < len (p => q) & len q < len (p => q) )
len (p => q) = (len (<*1*> ^ p)) + (len q) by FINSEQ_1:22
.= ((len <*1*>) + (len p)) + (len q) by FINSEQ_1:22
.= (1 + (len p)) + (len q) by FINSEQ_1:39
.= 1 + ((len p) + (len q)) ;
then A1: (len p) + (len q) < len (p => q) by XREAL_1:29;
( len p <= (len p) + (len q) & len q <= (len p) + (len q) ) by NAT_1:11;
hence ( len p < len (p => q) & len q < len (p => q) ) by A1, XXREAL_0:2; ::_thesis: verum
end;
theorem Th17: :: HILBERT2:17
for p, q being Element of HP-WFF
for t being FinSequence st p = q ^ t holds
p = q
proof
let p, q be Element of HP-WFF ; ::_thesis: for t being FinSequence st p = q ^ t holds
p = q
let t be FinSequence; ::_thesis: ( p = q ^ t implies p = q )
defpred S1[ Nat] means for p, q being Element of HP-WFF
for t being FinSequence st len p = $1 & p = q ^ t holds
p = q;
A1: 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 A2: for k being Nat st k < n holds
for p, q being Element of HP-WFF
for t being FinSequence st len p = k & p = q ^ t holds
p = q ; ::_thesis: S1[n]
let p, q be Element of HP-WFF ; ::_thesis: for t being FinSequence st len p = n & p = q ^ t holds
p = q
let t be FinSequence; ::_thesis: ( len p = n & p = q ^ t implies p = q )
assume that
A3: len p = n and
A4: p = q ^ t ; ::_thesis: p = q
len q >= 1 by Th10;
then A5: p . 1 = q . 1 by A4, FINSEQ_1:64;
percases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;
suppose p is conjunctive ; ::_thesis: p = q
then consider r, s being Element of HP-WFF such that
A6: p = r '&' s by Def6;
q . 1 = (<*2*> ^ (r ^ s)) . 1 by A5, A6, FINSEQ_1:32
.= 2 by FINSEQ_1:41 ;
then q is conjunctive by Th12;
then consider r9, s9 being Element of HP-WFF such that
A7: q = r9 '&' s9 by Def6;
<*2*> ^ ((r9 ^ s9) ^ t) = (<*2*> ^ (r9 ^ s9)) ^ t by FINSEQ_1:32
.= (<*2*> ^ r) ^ s by A4, A6, A7, FINSEQ_1:32
.= <*2*> ^ (r ^ s) by FINSEQ_1:32 ;
then (r9 ^ s9) ^ t = r ^ s by Th2;
then A8: r9 ^ (s9 ^ t) = r ^ s by FINSEQ_1:32;
now__::_thesis:_p_=_q
percases ( len r <= len r9 or len r >= len r9 ) ;
supposeA9: len r <= len r9 ; ::_thesis: p = q
n = (len q) + (len t) by A3, A4, FINSEQ_1:22;
then len q <= n by NAT_1:11;
then A10: len r9 < n by A7, Th15, XXREAL_0:2;
ex t1 being FinSequence st r ^ t1 = r9 by A8, A9, FINSEQ_1:47;
then r = r9 by A2, A10;
then A11: s9 ^ t = s by A8, FINSEQ_1:33;
len s < n by A3, A6, Th15;
then s9 = s by A2, A11;
then t = {} by A11, FINSEQ_1:87;
hence p = q by A4, FINSEQ_1:34; ::_thesis: verum
end;
suppose len r >= len r9 ; ::_thesis: p = q
then A12: ex t1 being FinSequence st r9 ^ t1 = r by A8, FINSEQ_1:47;
len r < n by A3, A6, Th15;
then r = r9 by A2, A12;
then A13: s9 ^ t = s by A8, FINSEQ_1:33;
len s < n by A3, A6, Th15;
then s9 = s by A2, A13;
then t = {} by A13, FINSEQ_1:87;
hence p = q by A4, FINSEQ_1:34; ::_thesis: verum
end;
end;
end;
hence p = q ; ::_thesis: verum
end;
suppose p is conditional ; ::_thesis: p = q
then consider r, s being Element of HP-WFF such that
A14: p = r => s by Def7;
q . 1 = (<*1*> ^ (r ^ s)) . 1 by A5, A14, FINSEQ_1:32
.= 1 by FINSEQ_1:41 ;
then q is conditional by Th11;
then consider r9, s9 being Element of HP-WFF such that
A15: q = r9 => s9 by Def7;
<*1*> ^ ((r9 ^ s9) ^ t) = (<*1*> ^ (r9 ^ s9)) ^ t by FINSEQ_1:32
.= (<*1*> ^ r) ^ s by A4, A14, A15, FINSEQ_1:32
.= <*1*> ^ (r ^ s) by FINSEQ_1:32 ;
then (r9 ^ s9) ^ t = r ^ s by Th2;
then A16: r9 ^ (s9 ^ t) = r ^ s by FINSEQ_1:32;
now__::_thesis:_p_=_q
percases ( len r <= len r9 or len r >= len r9 ) ;
supposeA17: len r <= len r9 ; ::_thesis: p = q
n = (len q) + (len t) by A3, A4, FINSEQ_1:22;
then len q <= n by NAT_1:11;
then A18: len r9 < n by A15, Th16, XXREAL_0:2;
ex t1 being FinSequence st r ^ t1 = r9 by A16, A17, FINSEQ_1:47;
then r = r9 by A2, A18;
then A19: s9 ^ t = s by A16, FINSEQ_1:33;
len s < n by A3, A14, Th16;
then s9 = s by A2, A19;
then t = {} by A19, FINSEQ_1:87;
hence p = q by A4, FINSEQ_1:34; ::_thesis: verum
end;
suppose len r >= len r9 ; ::_thesis: p = q
then A20: ex t1 being FinSequence st r9 ^ t1 = r by A16, FINSEQ_1:47;
len r < n by A3, A14, Th16;
then r = r9 by A2, A20;
then A21: s9 ^ t = s by A16, FINSEQ_1:33;
len s < n by A3, A14, Th16;
then s9 = s by A2, A21;
then t = {} by A21, FINSEQ_1:87;
hence p = q by A4, FINSEQ_1:34; ::_thesis: verum
end;
end;
end;
hence p = q ; ::_thesis: verum
end;
supposeA22: p is simple ; ::_thesis: p = q
A23: q <> {} by Th10, CARD_1:27;
ex n being Element of NAT st p = prop n by A22, Def8;
hence p = q by A4, A23, FINSEQ_1:88; ::_thesis: verum
end;
supposeA24: p = VERUM ; ::_thesis: p = q
q <> {} by Th10, CARD_1:27;
hence p = q by A4, A24, FINSEQ_1:88; ::_thesis: verum
end;
end;
end;
A25: for n being Nat holds S1[n] from NAT_1:sch_4(A1);
len p = len p ;
hence ( p = q ^ t implies p = q ) by A25; ::_thesis: verum
end;
theorem Th18: :: HILBERT2:18
for p, q, r, s being Element of HP-WFF st p ^ q = r ^ s holds
( p = r & q = s )
proof
let p, q, r, s be Element of HP-WFF ; ::_thesis: ( p ^ q = r ^ s implies ( p = r & q = s ) )
assume A1: p ^ q = r ^ s ; ::_thesis: ( p = r & q = s )
percases ( len p <= len r or len p >= len r ) ;
suppose len p <= len r ; ::_thesis: ( p = r & q = s )
then ex t being FinSequence st p ^ t = r by A1, FINSEQ_1:47;
hence p = r by Th17; ::_thesis: q = s
hence q = s by A1, FINSEQ_1:33; ::_thesis: verum
end;
suppose len p >= len r ; ::_thesis: ( p = r & q = s )
then ex t being FinSequence st r ^ t = p by A1, FINSEQ_1:47;
hence p = r by Th17; ::_thesis: q = s
hence q = s by A1, FINSEQ_1:33; ::_thesis: verum
end;
end;
end;
theorem Th19: :: HILBERT2:19
for p, q, r, s being Element of HP-WFF st p '&' q = r '&' s holds
( p = r & s = q )
proof
let p, q, r, s be Element of HP-WFF ; ::_thesis: ( p '&' q = r '&' s implies ( p = r & s = q ) )
assume p '&' q = r '&' s ; ::_thesis: ( p = r & s = q )
then <*2*> ^ (p ^ q) = r '&' s by FINSEQ_1:32
.= <*2*> ^ (r ^ s) by FINSEQ_1:32 ;
then p ^ q = r ^ s by Th2;
hence ( p = r & s = q ) by Th18; ::_thesis: verum
end;
theorem Th20: :: HILBERT2:20
for p, q, r, s being Element of HP-WFF st p => q = r => s holds
( p = r & s = q )
proof
let p, q, r, s be Element of HP-WFF ; ::_thesis: ( p => q = r => s implies ( p = r & s = q ) )
assume p => q = r => s ; ::_thesis: ( p = r & s = q )
then <*1*> ^ (p ^ q) = r => s by FINSEQ_1:32
.= <*1*> ^ (r ^ s) by FINSEQ_1:32 ;
then p ^ q = r ^ s by Th2;
hence ( p = r & s = q ) by Th18; ::_thesis: verum
end;
theorem Th21: :: HILBERT2:21
for n, m being Element of NAT st prop n = prop m holds
n = m
proof
let n, m be Element of NAT ; ::_thesis: ( prop n = prop m implies n = m )
assume prop n = prop m ; ::_thesis: n = m
then 3 + n = 3 + m by FINSEQ_1:76;
hence n = m ; ::_thesis: verum
end;
theorem Th22: :: HILBERT2:22
for p, q, r, s being Element of HP-WFF holds p '&' q <> r => s
proof
let p, q, r, s be Element of HP-WFF ; ::_thesis: p '&' q <> r => s
p '&' q = <*2*> ^ (p ^ q) by FINSEQ_1:32;
then ( r => s = <*1*> ^ (r ^ s) & (p '&' q) . 1 = 2 ) by FINSEQ_1:32, FINSEQ_1:41;
hence p '&' q <> r => s by FINSEQ_1:41; ::_thesis: verum
end;
theorem Th23: :: HILBERT2:23
for p, q being Element of HP-WFF holds p '&' q <> VERUM
proof
let p, q be Element of HP-WFF ; ::_thesis: p '&' q <> VERUM
p '&' q = <*2*> ^ (p ^ q) by FINSEQ_1:32;
then (p '&' q) . 1 = 2 by FINSEQ_1:41;
hence p '&' q <> VERUM by FINSEQ_1:40; ::_thesis: verum
end;
theorem Th24: :: HILBERT2:24
for n being Element of NAT
for p, q being Element of HP-WFF holds p '&' q <> prop n
proof
let n be Element of NAT ; ::_thesis: for p, q being Element of HP-WFF holds p '&' q <> prop n
let p, q be Element of HP-WFF ; ::_thesis: p '&' q <> prop n
A1: now__::_thesis:_not_2_=_(2_+_1)_+_n
assume 2 = (2 + 1) + n ; ::_thesis: contradiction
then 2 + 0 = 2 + (1 + n) ;
hence contradiction ; ::_thesis: verum
end;
p '&' q = <*2*> ^ (p ^ q) by FINSEQ_1:32;
then (p '&' q) . 1 = 2 by FINSEQ_1:41;
hence p '&' q <> prop n by A1, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th25: :: HILBERT2:25
for p, q being Element of HP-WFF holds p => q <> VERUM
proof
let p, q be Element of HP-WFF ; ::_thesis: p => q <> VERUM
p => q = <*1*> ^ (p ^ q) by FINSEQ_1:32;
then (p => q) . 1 = 1 by FINSEQ_1:41;
hence p => q <> VERUM by FINSEQ_1:40; ::_thesis: verum
end;
theorem Th26: :: HILBERT2:26
for n being Element of NAT
for p, q being Element of HP-WFF holds p => q <> prop n
proof
let n be Element of NAT ; ::_thesis: for p, q being Element of HP-WFF holds p => q <> prop n
let p, q be Element of HP-WFF ; ::_thesis: p => q <> prop n
A1: now__::_thesis:_not_1_=_(1_+_2)_+_n
assume 1 = (1 + 2) + n ; ::_thesis: contradiction
then 1 + 0 = 1 + (2 + n) ;
hence contradiction ; ::_thesis: verum
end;
p => q = <*1*> ^ (p ^ q) by FINSEQ_1:32;
then (p => q) . 1 = 1 by FINSEQ_1:41;
hence p => q <> prop n by A1, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th27: :: HILBERT2:27
for p, q being Element of HP-WFF holds
( p '&' q <> p & p '&' q <> q )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q <> p & p '&' q <> q )
len p < len (p '&' q) by Th15;
hence ( p '&' q <> p & p '&' q <> q ) by Th15; ::_thesis: verum
end;
theorem Th28: :: HILBERT2:28
for p, q being Element of HP-WFF holds
( p => q <> p & p => q <> q )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p => q <> p & p => q <> q )
len p < len (p => q) by Th16;
hence ( p => q <> p & p => q <> q ) by Th16; ::_thesis: verum
end;
theorem Th29: :: HILBERT2:29
for n being Element of NAT holds VERUM <> prop n
proof
let n be Element of NAT ; ::_thesis: VERUM <> prop n
assume A1: not VERUM <> prop n ; ::_thesis: contradiction
VERUM . 1 = 0 by FINSEQ_1:40;
hence contradiction by A1, FINSEQ_1:40; ::_thesis: verum
end;
begin
scheme :: HILBERT2:sch 3
HPMSSExL{ F1() -> set , F2( Element of NAT ) -> set , P1[ Element of HP-WFF , Element of HP-WFF , set , set , set ], P2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] } :
ex M being ManySortedSet of HP-WFF st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( P1[p,q,M . p,M . q,M . (p '&' q)] & P2[p,q,M . p,M . q,M . (p => q)] ) ) )
provided
A1: for p, q being Element of HP-WFF
for a, b being set ex c being set st P1[p,q,a,b,c] and
A2: for p, q being Element of HP-WFF
for a, b being set ex d being set st P2[p,q,a,b,d] and
A3: for p, q being Element of HP-WFF
for a, b, c, d being set st P1[p,q,a,b,c] & P1[p,q,a,b,d] holds
c = d and
A4: for p, q being Element of HP-WFF
for a, b, c, d being set st P2[p,q,a,b,c] & P2[p,q,a,b,d] holds
c = d
proof
defpred S1[ set , set ] means ( ( $1 = VERUM implies $2 = F1() ) & ( for n being Element of NAT st $1 = prop n holds
$2 = F2(n) ) );
set Pn = { (prop n) where n is Element of NAT : verum } ;
set X = { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } ;
A5: { (prop n) where n is Element of NAT : verum } c= HP-WFF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (prop n) where n is Element of NAT : verum } or x in HP-WFF )
assume x in { (prop n) where n is Element of NAT : verum } ; ::_thesis: x in HP-WFF
then ex n being Element of NAT st x = prop n ;
hence x in HP-WFF ; ::_thesis: verum
end;
{VERUM} c= HP-WFF by ZFMISC_1:31;
then reconsider Y0 = { (prop n) where n is Element of NAT : verum } \/ {VERUM} as Subset of HP-WFF by A5, XBOOLE_1:8;
A6: for x being set st x in Y0 holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in Y0 implies ex y being set st S1[x,y] )
assume A7: x in Y0 ; ::_thesis: ex y being set st S1[x,y]
percases ( x in { (prop n) where n is Element of NAT : verum } or x in {VERUM} ) by A7, XBOOLE_0:def_3;
suppose x in { (prop n) where n is Element of NAT : verum } ; ::_thesis: ex y being set st S1[x,y]
then consider n being Element of NAT such that
A8: x = prop n ;
take F2(n) ; ::_thesis: S1[x,F2(n)]
thus ( x = VERUM implies F2(n) = F1() ) by A8, Th29; ::_thesis: for n being Element of NAT st x = prop n holds
F2(n) = F2(n)
let k be Element of NAT ; ::_thesis: ( x = prop k implies F2(n) = F2(k) )
assume x = prop k ; ::_thesis: F2(n) = F2(k)
hence F2(n) = F2(k) by A8, Th21; ::_thesis: verum
end;
supposeA9: x in {VERUM} ; ::_thesis: ex y being set st S1[x,y]
take F1() ; ::_thesis: S1[x,F1()]
x = VERUM by A9, TARSKI:def_1;
hence S1[x,F1()] by Th29; ::_thesis: verum
end;
end;
end;
consider M0 being ManySortedSet of Y0 such that
A10: for x being set st x in Y0 holds
S1[x,M0 . x] from PBOOLE:sch_3(A6);
A11: for p, q being Element of HP-WFF holds
( not p '&' q in Y0 & not p => q in Y0 )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( not p '&' q in Y0 & not p => q in Y0 )
assume A12: ( p '&' q in Y0 or p => q in Y0 ) ; ::_thesis: contradiction
percases ( p '&' q in {VERUM} or p => q in {VERUM} or p '&' q in { (prop n) where n is Element of NAT : verum } or p => q in { (prop n) where n is Element of NAT : verum } ) by A12, XBOOLE_0:def_3;
suppose ( p '&' q in {VERUM} or p => q in {VERUM} ) ; ::_thesis: contradiction
then ( p '&' q = VERUM or p => q = VERUM ) by TARSKI:def_1;
hence contradiction by Th23, Th25; ::_thesis: verum
end;
suppose p '&' q in { (prop n) where n is Element of NAT : verum } ; ::_thesis: contradiction
then ex n being Element of NAT st p '&' q = prop n ;
hence contradiction by Th24; ::_thesis: verum
end;
suppose p => q in { (prop n) where n is Element of NAT : verum } ; ::_thesis: contradiction
then ex n being Element of NAT st p => q = prop n ;
hence contradiction by Th26; ::_thesis: verum
end;
end;
end;
then A13: ( ( for p, q being Element of HP-WFF st ( p '&' q in Y0 or p => q in Y0 ) holds
( p in Y0 & q in Y0 ) ) & ( for p, q being Element of HP-WFF st p '&' q in Y0 holds
for x, y, z being set st x = M0 . p & y = M0 . q & z = M0 . (p '&' q) holds
P1[p,q,x,y,z] ) ) ;
A14: for n being Element of NAT holds prop n in Y0
proof
let k be Element of NAT ; ::_thesis: prop k in Y0
prop k in { (prop n) where n is Element of NAT : verum } ;
hence prop k in Y0 by XBOOLE_0:def_3; ::_thesis: verum
end;
A15: for n being Element of NAT holds M0 . (prop n) = F2(n)
proof
let n be Element of NAT ; ::_thesis: M0 . (prop n) = F2(n)
prop n in Y0 by A14;
hence M0 . (prop n) = F2(n) by A10; ::_thesis: verum
end;
VERUM in {VERUM} by TARSKI:def_1;
then A16: VERUM in Y0 by XBOOLE_0:def_3;
A17: for Z being set st Z <> {} & Z c= { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } & Z is c=-linear holds
union Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
proof
defpred S2[ set , set ] means ex M being ManySortedSet of $1 st
( M = $2 & M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in $1 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in $1 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) );
let Z be set ; ::_thesis: ( Z <> {} & Z c= { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } & Z is c=-linear implies union Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } )
assume that
A18: Z <> {} and
A19: Z c= { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } and
A20: Z is c=-linear ; ::_thesis: union Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) }
A21: { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } c= bool HP-WFF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } or x in bool HP-WFF )
assume x in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } ; ::_thesis: x in bool HP-WFF
then ex Y being Subset of HP-WFF st
( x = Y & VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) ) ;
hence x in bool HP-WFF ; ::_thesis: verum
end;
then reconsider uZ = union Z as Subset of HP-WFF by A19, EQREL_1:61;
consider Z0 being set such that
A22: Z0 in Z by A18, XBOOLE_0:def_1;
A23: for x being set st x in Z holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in Z implies ex y being set st S2[x,y] )
assume x in Z ; ::_thesis: ex y being set st S2[x,y]
then x in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A19;
then consider Y being Subset of HP-WFF such that
A24: Y = x and
VERUM in Y and
for n being Element of NAT holds prop n in Y and
for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) and
A25: ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) ;
consider M being ManySortedSet of Y such that
A26: ( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) by A25;
take M ; ::_thesis: S2[x,M]
thus S2[x,M] by A24, A26; ::_thesis: verum
end;
consider MM being ManySortedSet of Z such that
A27: for x being set st x in Z holds
S2[x,MM . x] from PBOOLE:sch_3(A23);
rng MM is functional
proof
let y be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not y in rng MM or y is set )
assume y in rng MM ; ::_thesis: y is set
then consider x being set such that
A28: x in dom MM and
A29: y = MM . x by FUNCT_1:def_3;
x in Z by A28, PARTFUN1:def_2;
then S2[x,y] by A27, A29;
hence y is set ; ::_thesis: verum
end;
then reconsider rr = rng MM as functional set ;
A30: for f, g being Function st f in rr & g in rr & dom f c= dom g holds
f tolerates g
proof
let f, g be Function; ::_thesis: ( f in rr & g in rr & dom f c= dom g implies f tolerates g )
assume f in rr ; ::_thesis: ( not g in rr or not dom f c= dom g or f tolerates g )
then consider x1 being set such that
A31: x1 in dom MM and
A32: f = MM . x1 by FUNCT_1:def_3;
A33: x1 in Z by A31, PARTFUN1:def_2;
then A34: ex M being ManySortedSet of x1 st
( M = f & M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in x1 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in x1 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) by A27, A32;
then A35: x1 = dom f by PARTFUN1:def_2;
assume g in rr ; ::_thesis: ( not dom f c= dom g or f tolerates g )
then consider x2 being set such that
A36: x2 in dom MM and
A37: g = MM . x2 by FUNCT_1:def_3;
defpred S3[ Element of HP-WFF ] means ( $1 in x1 implies f . $1 = g . $1 );
assume A38: dom f c= dom g ; ::_thesis: f tolerates g
x2 in Z by A36, PARTFUN1:def_2;
then A39: ex M being ManySortedSet of x2 st
( M = g & M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in x2 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in x2 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) by A27, A37;
A40: for n being Element of NAT holds S3[ prop n]
proof
let n be Element of NAT ; ::_thesis: S3[ prop n]
assume prop n in x1 ; ::_thesis: f . (prop n) = g . (prop n)
thus f . (prop n) = F2(n) by A34
.= g . (prop n) by A39 ; ::_thesis: verum
end;
A41: x1 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A19, A33;
A42: for r, s being Element of HP-WFF st S3[r] & S3[s] holds
( S3[r '&' s] & S3[r => s] )
proof
A43: ( ex Y being Subset of HP-WFF st
( Y = x1 & VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) ) & x1 c= x2 ) by A39, A38, A35, A41, PARTFUN1:def_2;
let r, s be Element of HP-WFF ; ::_thesis: ( S3[r] & S3[s] implies ( S3[r '&' s] & S3[r => s] ) )
assume A44: ( ( r in x1 implies f . r = g . r ) & ( s in x1 implies f . s = g . s ) ) ; ::_thesis: ( S3[r '&' s] & S3[r => s] )
thus ( r '&' s in x1 implies f . (r '&' s) = g . (r '&' s) ) ::_thesis: S3[r => s]
proof
assume r '&' s in x1 ; ::_thesis: f . (r '&' s) = g . (r '&' s)
then ( P1[r,s,g . r,g . s,f . (r '&' s)] & P1[r,s,g . r,g . s,g . (r '&' s)] ) by A34, A39, A44, A43;
hence f . (r '&' s) = g . (r '&' s) by A3; ::_thesis: verum
end;
thus ( r => s in x1 implies f . (r => s) = g . (r => s) ) ::_thesis: verum
proof
assume r => s in x1 ; ::_thesis: f . (r => s) = g . (r => s)
then ( P2[r,s,g . r,g . s,f . (r => s)] & P2[r,s,g . r,g . s,g . (r => s)] ) by A34, A39, A44, A43;
hence f . (r => s) = g . (r => s) by A4; ::_thesis: verum
end;
end;
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom f) /\ (dom g) or f . x = g . x )
assume x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x
then A45: x in x1 by A38, A35, XBOOLE_1:28;
A46: S3[ VERUM ] by A34, A39;
for p being Element of HP-WFF holds S3[p] from HILBERT2:sch_2(A46, A40, A42);
hence f . x = g . x by A21, A45, A41; ::_thesis: verum
end;
for f, g being Function st f in rr & g in rr holds
f tolerates g
proof
let f, g be Function; ::_thesis: ( f in rr & g in rr implies f tolerates g )
assume A47: f in rr ; ::_thesis: ( not g in rr or f tolerates g )
then consider x1 being set such that
A48: x1 in dom MM and
A49: f = MM . x1 by FUNCT_1:def_3;
A50: x1 in Z by A48, PARTFUN1:def_2;
then ex M being ManySortedSet of x1 st
( M = f & M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in x1 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in x1 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) by A27, A49;
then A51: x1 = dom f by PARTFUN1:def_2;
assume A52: g in rr ; ::_thesis: f tolerates g
then consider x2 being set such that
A53: x2 in dom MM and
A54: g = MM . x2 by FUNCT_1:def_3;
A55: x2 in Z by A53, PARTFUN1:def_2;
then x1,x2 are_c=-comparable by A20, A50, ORDINAL1:def_8;
then A56: ( x1 c= x2 or x2 c= x1 ) by XBOOLE_0:def_9;
ex M being ManySortedSet of x2 st
( M = g & M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in x2 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in x2 holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) by A27, A54, A55;
then x2 = dom g by PARTFUN1:def_2;
hence f tolerates g by A30, A47, A52, A51, A56; ::_thesis: verum
end;
then union rr is Function by WELLFND1:1;
then reconsider M = Union MM as Function by CARD_3:def_4;
for x being set st x in Z holds
MM . x is ManySortedSet of x
proof
let x be set ; ::_thesis: ( x in Z implies MM . x is ManySortedSet of x )
assume x in Z ; ::_thesis: MM . x is ManySortedSet of x
then S2[x,MM . x] by A27;
hence MM . x is ManySortedSet of x ; ::_thesis: verum
end;
then dom M = uZ by Th1;
then reconsider M = M as ManySortedSet of uZ by PARTFUN1:def_2, RELAT_1:def_18;
A57: M = union rr by CARD_3:def_4;
A58: for p, q being Element of HP-WFF st p '&' q in uZ holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z]
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q in uZ implies for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] )
assume p '&' q in uZ ; ::_thesis: for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z]
then consider Z1 being set such that
A59: p '&' q in Z1 and
A60: Z1 in Z by TARSKI:def_4;
Z1 in dom MM by A60, PARTFUN1:def_2;
then MM . Z1 in rr by FUNCT_1:def_3;
then A61: MM . Z1 c= M by A57, ZFMISC_1:74;
let x, y, z be set ; ::_thesis: ( x = M . p & y = M . q & z = M . (p '&' q) implies P1[p,q,x,y,z] )
assume that
A62: x = M . p and
A63: y = M . q and
A64: z = M . (p '&' q) ; ::_thesis: P1[p,q,x,y,z]
consider MZ1 being ManySortedSet of Z1 such that
A65: MZ1 = MM . Z1 and
MZ1 . VERUM = F1() and
for n being Element of NAT holds MZ1 . (prop n) = F2(n) and
A66: for p, q being Element of HP-WFF st p '&' q in Z1 holds
for x, y, z being set st x = MZ1 . p & y = MZ1 . q & z = MZ1 . (p '&' q) holds
P1[p,q,x,y,z] and
for p, q being Element of HP-WFF st p => q in Z1 holds
for x, y, z being set st x = MZ1 . p & y = MZ1 . q & z = MZ1 . (p => q) holds
P2[p,q,x,y,z] by A27, A60;
p '&' q in dom MZ1 by A59, PARTFUN1:def_2;
then A67: z = MZ1 . (p '&' q) by A65, A61, A64, GRFUNC_1:2;
Z1 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A19, A60;
then A68: ex Y being Subset of HP-WFF st
( Z1 = Y & VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) ) ;
then q in Z1 by A59;
then q in dom MZ1 by PARTFUN1:def_2;
then A69: y = MZ1 . q by A65, A61, A63, GRFUNC_1:2;
p in Z1 by A59, A68;
then p in dom MZ1 by PARTFUN1:def_2;
then x = MZ1 . p by A65, A61, A62, GRFUNC_1:2;
hence P1[p,q,x,y,z] by A59, A66, A69, A67; ::_thesis: verum
end;
Z0 in dom MM by A22, PARTFUN1:def_2;
then MM . Z0 in rr by FUNCT_1:def_3;
then A70: MM . Z0 c= M by A57, ZFMISC_1:74;
consider MZ0 being ManySortedSet of Z0 such that
A71: MZ0 = MM . Z0 and
A72: MZ0 . VERUM = F1() and
A73: for n being Element of NAT holds MZ0 . (prop n) = F2(n) and
for p, q being Element of HP-WFF st p '&' q in Z0 holds
for x, y, z being set st x = MZ0 . p & y = MZ0 . q & z = MZ0 . (p '&' q) holds
P1[p,q,x,y,z] and
for p, q being Element of HP-WFF st p => q in Z0 holds
for x, y, z being set st x = MZ0 . p & y = MZ0 . q & z = MZ0 . (p => q) holds
P2[p,q,x,y,z] by A22, A27;
A74: Y0 c= Z0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y0 or x in Z0 )
Z0 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A19, A22;
then A75: ex Y being Subset of HP-WFF st
( Y = Z0 & VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) ) ;
assume A76: x in Y0 ; ::_thesis: x in Z0
percases ( x in {VERUM} or x in { (prop n) where n is Element of NAT : verum } ) by A76, XBOOLE_0:def_3;
suppose x in {VERUM} ; ::_thesis: x in Z0
hence x in Z0 by A75, TARSKI:def_1; ::_thesis: verum
end;
suppose x in { (prop n) where n is Element of NAT : verum } ; ::_thesis: x in Z0
then ex n being Element of NAT st x = prop n ;
hence x in Z0 by A75; ::_thesis: verum
end;
end;
end;
then A77: Y0 c= dom MZ0 by PARTFUN1:def_2;
A78: for n being Element of NAT holds M . (prop n) = F2(n)
proof
let n be Element of NAT ; ::_thesis: M . (prop n) = F2(n)
prop n in Y0 by A14;
hence M . (prop n) = MZ0 . (prop n) by A70, A71, A77, GRFUNC_1:2
.= F2(n) by A73 ;
::_thesis: verum
end;
A79: for p, q being Element of HP-WFF st p => q in uZ holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z]
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p => q in uZ implies for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] )
assume p => q in uZ ; ::_thesis: for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z]
then consider Z1 being set such that
A80: p => q in Z1 and
A81: Z1 in Z by TARSKI:def_4;
Z1 in dom MM by A81, PARTFUN1:def_2;
then MM . Z1 in rr by FUNCT_1:def_3;
then A82: MM . Z1 c= M by A57, ZFMISC_1:74;
let x, y, z be set ; ::_thesis: ( x = M . p & y = M . q & z = M . (p => q) implies P2[p,q,x,y,z] )
assume that
A83: x = M . p and
A84: y = M . q and
A85: z = M . (p => q) ; ::_thesis: P2[p,q,x,y,z]
consider MZ1 being ManySortedSet of Z1 such that
A86: MZ1 = MM . Z1 and
MZ1 . VERUM = F1() and
for n being Element of NAT holds MZ1 . (prop n) = F2(n) and
for p, q being Element of HP-WFF st p '&' q in Z1 holds
for x, y, z being set st x = MZ1 . p & y = MZ1 . q & z = MZ1 . (p '&' q) holds
P1[p,q,x,y,z] and
A87: for p, q being Element of HP-WFF st p => q in Z1 holds
for x, y, z being set st x = MZ1 . p & y = MZ1 . q & z = MZ1 . (p => q) holds
P2[p,q,x,y,z] by A27, A81;
p => q in dom MZ1 by A80, PARTFUN1:def_2;
then A88: z = MZ1 . (p => q) by A86, A82, A85, GRFUNC_1:2;
Z1 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A19, A81;
then A89: ex Y being Subset of HP-WFF st
( Z1 = Y & VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) ) ;
then q in Z1 by A80;
then q in dom MZ1 by PARTFUN1:def_2;
then A90: y = MZ1 . q by A86, A82, A84, GRFUNC_1:2;
p in Z1 by A80, A89;
then p in dom MZ1 by PARTFUN1:def_2;
then x = MZ1 . p by A86, A82, A83, GRFUNC_1:2;
hence P2[p,q,x,y,z] by A80, A87, A90, A88; ::_thesis: verum
end;
A91: for p, q being Element of HP-WFF st ( p '&' q in uZ or p => q in uZ ) holds
( p in uZ & q in uZ )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( ( p '&' q in uZ or p => q in uZ ) implies ( p in uZ & q in uZ ) )
assume A92: ( p '&' q in uZ or p => q in uZ ) ; ::_thesis: ( p in uZ & q in uZ )
percases ( p '&' q in uZ or p => q in uZ ) by A92;
suppose p '&' q in uZ ; ::_thesis: ( p in uZ & q in uZ )
then consider Z0 being set such that
A93: p '&' q in Z0 and
A94: Z0 in Z by TARSKI:def_4;
Z0 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A19, A94;
then ex Y being Subset of HP-WFF st
( Z0 = Y & VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) ) ;
then ( p in Z0 & q in Z0 ) by A93;
hence ( p in uZ & q in uZ ) by A94, TARSKI:def_4; ::_thesis: verum
end;
suppose p => q in uZ ; ::_thesis: ( p in uZ & q in uZ )
then consider Z0 being set such that
A95: p => q in Z0 and
A96: Z0 in Z by TARSKI:def_4;
Z0 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A19, A96;
then ex Y being Subset of HP-WFF st
( Z0 = Y & VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) ) ;
then ( p in Z0 & q in Z0 ) by A95;
hence ( p in uZ & q in uZ ) by A96, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
Z0 c= uZ by A22, ZFMISC_1:74;
then A97: Y0 c= uZ by A74, XBOOLE_1:1;
A98: for n being Element of NAT holds prop n in uZ
proof
let n be Element of NAT ; ::_thesis: prop n in uZ
prop n in Y0 by A14;
hence prop n in uZ by A97; ::_thesis: verum
end;
M . VERUM = F1() by A16, A70, A71, A72, A77, GRFUNC_1:2;
hence union Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A16, A97, A98, A91, A78, A58, A79; ::_thesis: verum
end;
A99: for p, q being Element of HP-WFF st p => q in Y0 holds
for x, y, z being set st x = M0 . p & y = M0 . q & z = M0 . (p => q) holds
P2[p,q,x,y,z] by A11;
M0 . VERUM = F1() by A10, A16;
then Y0 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A16, A14, A15, A13, A99;
then consider H being set such that
A100: H in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } and
A101: for Z being set st Z in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } & Z <> H holds
not H c= Z by A17, ORDERS_1:67;
consider Y being Subset of HP-WFF such that
A102: Y = H and
A103: VERUM in Y and
A104: for n being Element of NAT holds prop n in Y and
A105: for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) and
A106: ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] ) ) by A100;
consider M being ManySortedSet of Y such that
A107: M . VERUM = F1() and
A108: for n being Element of NAT holds M . (prop n) = F2(n) and
A109: for p, q being Element of HP-WFF st p '&' q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p '&' q) holds
P1[p,q,x,y,z] and
A110: for p, q being Element of HP-WFF st p => q in Y holds
for x, y, z being set st x = M . p & y = M . q & z = M . (p => q) holds
P2[p,q,x,y,z] by A106;
A111: Y = HP-WFF
proof
defpred S2[ Element of HP-WFF ] means $1 in Y;
A112: for n being Element of NAT holds S2[ prop n] by A104;
A113: for r, s being Element of HP-WFF st S2[r] & S2[s] holds
( S2[r '&' s] & S2[r => s] )
proof
let r, s be Element of HP-WFF ; ::_thesis: ( S2[r] & S2[s] implies ( S2[r '&' s] & S2[r => s] ) )
assume A114: ( r in Y & s in Y ) ; ::_thesis: ( S2[r '&' s] & S2[r => s] )
assume A115: ( not S2[r '&' s] or not S2[r => s] ) ; ::_thesis: contradiction
percases ( not r '&' s in Y or not r => s in Y ) by A115;
supposeA116: not r '&' s in Y ; ::_thesis: contradiction
{(r '&' s)} c= HP-WFF by ZFMISC_1:31;
then reconsider Y9 = Y \/ {(r '&' s)} as Subset of HP-WFF by XBOOLE_1:8;
consider CMrMs being set such that
A117: P1[r,s,M . r,M . s,CMrMs] by A1;
set N = M +* ((r '&' s) .--> CMrMs);
A118: dom ((r '&' s) .--> CMrMs) = {(r '&' s)} by FUNCOP_1:13;
dom M = Y by PARTFUN1:def_2;
then dom (M +* ((r '&' s) .--> CMrMs)) = Y9 by A118, FUNCT_4:def_1;
then reconsider N = M +* ((r '&' s) .--> CMrMs) as ManySortedSet of Y9 by PARTFUN1:def_2, RELAT_1:def_18;
r '&' s in {(r '&' s)} by TARSKI:def_1;
then A119: r '&' s in Y9 by XBOOLE_0:def_3;
A120: for p, q being Element of HP-WFF st p => q in Y9 holds
for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z]
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p => q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z] )
assume A121: p => q in Y9 ; ::_thesis: for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z]
p => q <> r '&' s by Th22;
then A122: not p => q in {(r '&' s)} by TARSKI:def_1;
then A123: p => q in Y by A121, XBOOLE_0:def_3;
then p in Y by A105;
then not p in {(r '&' s)} by A116, TARSKI:def_1;
then A124: N . p = M . p by A118, FUNCT_4:11;
q in Y by A105, A123;
then not q in {(r '&' s)} by A116, TARSKI:def_1;
then A125: N . q = M . q by A118, FUNCT_4:11;
A126: N . (p => q) = M . (p => q) by A118, A122, FUNCT_4:11;
let x, y, z be set ; ::_thesis: ( x = N . p & y = N . q & z = N . (p => q) implies P2[p,q,x,y,z] )
assume ( x = N . p & y = N . q & z = N . (p => q) ) ; ::_thesis: P2[p,q,x,y,z]
hence P2[p,q,x,y,z] by A110, A123, A124, A125, A126; ::_thesis: verum
end;
A127: for n being Element of NAT holds N . (prop n) = F2(n)
proof
let n be Element of NAT ; ::_thesis: N . (prop n) = F2(n)
prop n <> r '&' s by Th24;
then not prop n in {(r '&' s)} by TARSKI:def_1;
hence N . (prop n) = M . (prop n) by A118, FUNCT_4:11
.= F2(n) by A108 ;
::_thesis: verum
end;
A128: for p, q being Element of HP-WFF st p '&' q in Y9 holds
for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z]
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z] )
assume A129: p '&' q in Y9 ; ::_thesis: for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z]
let x, y, z be set ; ::_thesis: ( x = N . p & y = N . q & z = N . (p '&' q) implies P1[p,q,x,y,z] )
assume A130: ( x = N . p & y = N . q & z = N . (p '&' q) ) ; ::_thesis: P1[p,q,x,y,z]
percases ( p '&' q = r '&' s or p '&' q <> r '&' s ) ;
supposeA131: p '&' q = r '&' s ; ::_thesis: P1[p,q,x,y,z]
q <> p '&' q by Th27;
then not q in {(r '&' s)} by A131, TARSKI:def_1;
then A132: N . q = M . q by A118, FUNCT_4:11;
p <> p '&' q by Th27;
then not p in {(r '&' s)} by A131, TARSKI:def_1;
then A133: N . p = M . p by A118, FUNCT_4:11;
p '&' q in {(r '&' s)} by A131, TARSKI:def_1;
then A134: N . (p '&' q) = ((r '&' s) .--> CMrMs) . (p '&' q) by A118, FUNCT_4:13;
( p = r & q = s ) by A131, Th19;
hence P1[p,q,x,y,z] by A117, A130, A133, A132, A134, FUNCOP_1:72; ::_thesis: verum
end;
suppose p '&' q <> r '&' s ; ::_thesis: P1[p,q,x,y,z]
then A135: not p '&' q in {(r '&' s)} by TARSKI:def_1;
then A136: p '&' q in Y by A129, XBOOLE_0:def_3;
then p in Y by A105;
then not p in {(r '&' s)} by A116, TARSKI:def_1;
then A137: N . p = M . p by A118, FUNCT_4:11;
q in Y by A105, A136;
then not q in {(r '&' s)} by A116, TARSKI:def_1;
then A138: N . q = M . q by A118, FUNCT_4:11;
N . (p '&' q) = M . (p '&' q) by A118, A135, FUNCT_4:11;
hence P1[p,q,x,y,z] by A109, A130, A136, A137, A138; ::_thesis: verum
end;
end;
end;
A139: Y c= Y9 by XBOOLE_1:7;
A140: now__::_thesis:_for_n_being_Element_of_NAT_holds_prop_n_in_Y9
let n be Element of NAT ; ::_thesis: prop n in Y9
prop n in Y by A104;
hence prop n in Y9 by A139; ::_thesis: verum
end;
A141: for p, q being Element of HP-WFF st ( p '&' q in Y9 or p => q in Y9 ) holds
( p in Y9 & q in Y9 )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( ( p '&' q in Y9 or p => q in Y9 ) implies ( p in Y9 & q in Y9 ) )
assume A142: ( p '&' q in Y9 or p => q in Y9 ) ; ::_thesis: ( p in Y9 & q in Y9 )
percases ( p '&' q = r '&' s or ( p '&' q in Y9 & p '&' q <> r '&' s ) or p => q in Y9 ) by A142;
suppose p '&' q = r '&' s ; ::_thesis: ( p in Y9 & q in Y9 )
then ( p = r & q = s ) by Th19;
hence ( p in Y9 & q in Y9 ) by A114, A139; ::_thesis: verum
end;
supposethat A143: p '&' q in Y9 and
A144: p '&' q <> r '&' s ; ::_thesis: ( p in Y9 & q in Y9 )
not p '&' q in {(r '&' s)} by A144, TARSKI:def_1;
then p '&' q in Y by A143, XBOOLE_0:def_3;
then ( p in Y & q in Y ) by A105;
hence ( p in Y9 & q in Y9 ) by A139; ::_thesis: verum
end;
supposeA145: p => q in Y9 ; ::_thesis: ( p in Y9 & q in Y9 )
p => q <> r '&' s by Th22;
then not p => q in {(r '&' s)} by TARSKI:def_1;
then p => q in Y by A145, XBOOLE_0:def_3;
then ( p in Y & q in Y ) by A105;
hence ( p in Y9 & q in Y9 ) by A139; ::_thesis: verum
end;
end;
end;
VERUM <> r '&' s by Th23;
then not VERUM in {(r '&' s)} by TARSKI:def_1;
then N . VERUM = F1() by A107, A118, FUNCT_4:11;
then Y9 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A103, A139, A140, A141, A127, A128, A120;
hence contradiction by A101, A102, A116, A119, XBOOLE_1:7; ::_thesis: verum
end;
supposeA146: not r => s in Y ; ::_thesis: contradiction
{(r => s)} c= HP-WFF by ZFMISC_1:31;
then reconsider Y9 = Y \/ {(r => s)} as Subset of HP-WFF by XBOOLE_1:8;
consider IMrMs being set such that
A147: P2[r,s,M . r,M . s,IMrMs] by A2;
set N = M +* ((r => s) .--> IMrMs);
A148: dom ((r => s) .--> IMrMs) = {(r => s)} by FUNCOP_1:13;
dom M = Y by PARTFUN1:def_2;
then dom (M +* ((r => s) .--> IMrMs)) = Y9 by A148, FUNCT_4:def_1;
then reconsider N = M +* ((r => s) .--> IMrMs) as ManySortedSet of Y9 by PARTFUN1:def_2, RELAT_1:def_18;
r => s in {(r => s)} by TARSKI:def_1;
then A149: r => s in Y9 by XBOOLE_0:def_3;
A150: for p, q being Element of HP-WFF st p '&' q in Y9 holds
for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z]
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z] )
assume A151: p '&' q in Y9 ; ::_thesis: for x, y, z being set st x = N . p & y = N . q & z = N . (p '&' q) holds
P1[p,q,x,y,z]
p '&' q <> r => s by Th22;
then A152: not p '&' q in {(r => s)} by TARSKI:def_1;
then A153: p '&' q in Y by A151, XBOOLE_0:def_3;
then p in Y by A105;
then not p in {(r => s)} by A146, TARSKI:def_1;
then A154: N . p = M . p by A148, FUNCT_4:11;
q in Y by A105, A153;
then not q in {(r => s)} by A146, TARSKI:def_1;
then A155: N . q = M . q by A148, FUNCT_4:11;
A156: N . (p '&' q) = M . (p '&' q) by A148, A152, FUNCT_4:11;
let x, y, z be set ; ::_thesis: ( x = N . p & y = N . q & z = N . (p '&' q) implies P1[p,q,x,y,z] )
assume ( x = N . p & y = N . q & z = N . (p '&' q) ) ; ::_thesis: P1[p,q,x,y,z]
hence P1[p,q,x,y,z] by A109, A153, A154, A155, A156; ::_thesis: verum
end;
A157: for n being Element of NAT holds N . (prop n) = F2(n)
proof
let n be Element of NAT ; ::_thesis: N . (prop n) = F2(n)
prop n <> r => s by Th26;
then not prop n in {(r => s)} by TARSKI:def_1;
hence N . (prop n) = M . (prop n) by A148, FUNCT_4:11
.= F2(n) by A108 ;
::_thesis: verum
end;
A158: for p, q being Element of HP-WFF st p => q in Y9 holds
for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z]
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p => q in Y9 implies for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z] )
assume A159: p => q in Y9 ; ::_thesis: for x, y, z being set st x = N . p & y = N . q & z = N . (p => q) holds
P2[p,q,x,y,z]
let x, y, z be set ; ::_thesis: ( x = N . p & y = N . q & z = N . (p => q) implies P2[p,q,x,y,z] )
assume A160: ( x = N . p & y = N . q & z = N . (p => q) ) ; ::_thesis: P2[p,q,x,y,z]
percases ( p => q = r => s or p => q <> r => s ) ;
supposeA161: p => q = r => s ; ::_thesis: P2[p,q,x,y,z]
q <> p => q by Th28;
then not q in {(r => s)} by A161, TARSKI:def_1;
then A162: N . q = M . q by A148, FUNCT_4:11;
p <> p => q by Th28;
then not p in {(r => s)} by A161, TARSKI:def_1;
then A163: N . p = M . p by A148, FUNCT_4:11;
p => q in {(r => s)} by A161, TARSKI:def_1;
then A164: N . (p => q) = ((r => s) .--> IMrMs) . (p => q) by A148, FUNCT_4:13;
( p = r & q = s ) by A161, Th20;
hence P2[p,q,x,y,z] by A147, A160, A163, A162, A164, FUNCOP_1:72; ::_thesis: verum
end;
suppose p => q <> r => s ; ::_thesis: P2[p,q,x,y,z]
then A165: not p => q in {(r => s)} by TARSKI:def_1;
then A166: p => q in Y by A159, XBOOLE_0:def_3;
then p in Y by A105;
then not p in {(r => s)} by A146, TARSKI:def_1;
then A167: N . p = M . p by A148, FUNCT_4:11;
q in Y by A105, A166;
then not q in {(r => s)} by A146, TARSKI:def_1;
then A168: N . q = M . q by A148, FUNCT_4:11;
N . (p => q) = M . (p => q) by A148, A165, FUNCT_4:11;
hence P2[p,q,x,y,z] by A110, A160, A166, A167, A168; ::_thesis: verum
end;
end;
end;
A169: Y c= Y9 by XBOOLE_1:7;
A170: now__::_thesis:_for_n_being_Element_of_NAT_holds_prop_n_in_Y9
let n be Element of NAT ; ::_thesis: prop n in Y9
prop n in Y by A104;
hence prop n in Y9 by A169; ::_thesis: verum
end;
A171: for p, q being Element of HP-WFF st ( p '&' q in Y9 or p => q in Y9 ) holds
( p in Y9 & q in Y9 )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( ( p '&' q in Y9 or p => q in Y9 ) implies ( p in Y9 & q in Y9 ) )
assume A172: ( p '&' q in Y9 or p => q in Y9 ) ; ::_thesis: ( p in Y9 & q in Y9 )
percases ( p => q = r => s or ( p => q in Y9 & p => q <> r => s ) or p '&' q in Y9 ) by A172;
suppose p => q = r => s ; ::_thesis: ( p in Y9 & q in Y9 )
then ( p = r & q = s ) by Th20;
hence ( p in Y9 & q in Y9 ) by A114, A169; ::_thesis: verum
end;
supposethat A173: p => q in Y9 and
A174: p => q <> r => s ; ::_thesis: ( p in Y9 & q in Y9 )
not p => q in {(r => s)} by A174, TARSKI:def_1;
then p => q in Y by A173, XBOOLE_0:def_3;
then ( p in Y & q in Y ) by A105;
hence ( p in Y9 & q in Y9 ) by A169; ::_thesis: verum
end;
supposeA175: p '&' q in Y9 ; ::_thesis: ( p in Y9 & q in Y9 )
p '&' q <> r => s by Th22;
then not p '&' q in {(r => s)} by TARSKI:def_1;
then p '&' q in Y by A175, XBOOLE_0:def_3;
then ( p in Y & q in Y ) by A105;
hence ( p in Y9 & q in Y9 ) by A169; ::_thesis: verum
end;
end;
end;
VERUM <> r => s by Th25;
then not VERUM in {(r => s)} by TARSKI:def_1;
then N . VERUM = F1() by A107, A148, FUNCT_4:11;
then Y9 in { Y where Y is Subset of HP-WFF : ( VERUM in Y & ( for n being Element of NAT holds prop n in Y ) & ( for p, q being Element of HP-WFF st ( p '&' q in Y or p => q in Y ) holds
( p in Y & q in Y ) ) & ex M being ManySortedSet of Y st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF st p '&' q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p '&' q) holds
P1[p,q,a,b,c] ) & ( for p, q being Element of HP-WFF st p => q in Y holds
for a, b, c being set st a = M . p & b = M . q & c = M . (p => q) holds
P2[p,q,a,b,c] ) ) ) } by A103, A169, A170, A171, A157, A158, A150;
hence contradiction by A101, A102, A146, A149, XBOOLE_1:7; ::_thesis: verum
end;
end;
end;
A176: S2[ VERUM ] by A103;
for s being Element of HP-WFF holds S2[s] from HILBERT2:sch_2(A176, A112, A113);
hence Y = HP-WFF by SUBSET_1:28; ::_thesis: verum
end;
then reconsider M = M as ManySortedSet of HP-WFF ;
take M ; ::_thesis: ( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( P1[p,q,M . p,M . q,M . (p '&' q)] & P2[p,q,M . p,M . q,M . (p => q)] ) ) )
thus ( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( P1[p,q,M . p,M . q,M . (p '&' q)] & P2[p,q,M . p,M . q,M . (p => q)] ) ) ) by A107, A108, A109, A110, A111; ::_thesis: verum
end;
scheme :: HILBERT2:sch 4
HPMSSLambda{ F1() -> set , F2( Element of NAT ) -> set , F3( set , set ) -> set , F4( set , set ) -> set } :
ex M being ManySortedSet of HP-WFF st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) ) ) )
proof
defpred S1[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means $5 = F4($3,$4);
defpred S2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means $5 = F3($3,$4);
A1: for p, q being Element of HP-WFF
for a, b being set ex d being set st S1[p,q,a,b,d] ;
A2: for p, q being Element of HP-WFF
for a, b, c, d being set st S2[p,q,a,b,c] & S2[p,q,a,b,d] holds
c = d ;
A3: for p, q being Element of HP-WFF
for a, b, c, d being set st S1[p,q,a,b,c] & S1[p,q,a,b,d] holds
c = d ;
A4: for p, q being Element of HP-WFF
for a, b being set ex c being set st S2[p,q,a,b,c] ;
consider M being ManySortedSet of HP-WFF such that
A5: M . VERUM = F1() and
A6: for n being Element of NAT holds M . (prop n) = F2(n) and
A7: for p, q being Element of HP-WFF holds
( S2[p,q,M . p,M . q,M . (p '&' q)] & S1[p,q,M . p,M . q,M . (p => q)] ) from HILBERT2:sch_3(A4, A1, A2, A3);
take M ; ::_thesis: ( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) ) ) )
thus M . VERUM = F1() by A5; ::_thesis: ( ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) ) ) )
thus for n being Element of NAT holds M . (prop n) = F2(n) by A6; ::_thesis: for p, q being Element of HP-WFF holds
( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) )
let p, q be Element of HP-WFF ; ::_thesis: ( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) )
set x = M . p;
set y = M . q;
thus M . (p '&' q) = F3((M . p),(M . q)) by A7; ::_thesis: M . (p => q) = F4((M . p),(M . q))
thus M . (p => q) = F4((M . p),(M . q)) by A7; ::_thesis: verum
end;
begin
definition
func HP-Subformulae -> ManySortedSet of HP-WFF means :Def9: :: HILBERT2:def 9
( it . VERUM = root-tree VERUM & ( for n being Element of NAT holds it . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = it . p & q9 = it . q & it . (p '&' q) = (p '&' q) -tree (p9,q9) & it . (p => q) = (p => q) -tree (p9,q9) ) ) );
existence
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) )
proof
deffunc H1( Element of NAT ) -> Element of FinTrees HP-WFF = root-tree (prop $1);
defpred S1[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is DecoratedTree of HP-WFF & $4 is DecoratedTree of HP-WFF implies ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = $3 & q9 = $4 & $5 = ($1 => $2) -tree (p9,q9) ) ) & ( ( not $3 is DecoratedTree of HP-WFF or not $4 is DecoratedTree of HP-WFF ) implies $5 = {} ) );
defpred S2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is DecoratedTree of HP-WFF & $4 is DecoratedTree of HP-WFF implies ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = $3 & q9 = $4 & $5 = ($1 '&' $2) -tree (p9,q9) ) ) & ( ( not $3 is DecoratedTree of HP-WFF or not $4 is DecoratedTree of HP-WFF ) implies $5 = {} ) );
A1: for p, q being Element of HP-WFF
for a, b being set ex c being set st S2[p,q,a,b,c]
proof
let p, q be Element of HP-WFF ; ::_thesis: for a, b being set ex c being set st S2[p,q,a,b,c]
let a, b be set ; ::_thesis: ex c being set st S2[p,q,a,b,c]
percases ( ( a is DecoratedTree of HP-WFF & b is DecoratedTree of HP-WFF ) or not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ) ;
supposethat A2: a is DecoratedTree of HP-WFF and
A3: b is DecoratedTree of HP-WFF ; ::_thesis: ex c being set st S2[p,q,a,b,c]
reconsider q9 = b as DecoratedTree of HP-WFF by A3;
reconsider p9 = a as DecoratedTree of HP-WFF by A2;
take (p '&' q) -tree (p9,q9) ; ::_thesis: S2[p,q,a,b,(p '&' q) -tree (p9,q9)]
thus S2[p,q,a,b,(p '&' q) -tree (p9,q9)] ; ::_thesis: verum
end;
suppose ( not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ) ; ::_thesis: ex c being set st S2[p,q,a,b,c]
hence ex c being set st S2[p,q,a,b,c] ; ::_thesis: verum
end;
end;
end;
A4: for p, q being Element of HP-WFF
for a, b being set ex d being set st S1[p,q,a,b,d]
proof
let p, q be Element of HP-WFF ; ::_thesis: for a, b being set ex d being set st S1[p,q,a,b,d]
let a, b be set ; ::_thesis: ex d being set st S1[p,q,a,b,d]
percases ( ( a is DecoratedTree of HP-WFF & b is DecoratedTree of HP-WFF ) or not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ) ;
supposethat A5: a is DecoratedTree of HP-WFF and
A6: b is DecoratedTree of HP-WFF ; ::_thesis: ex d being set st S1[p,q,a,b,d]
reconsider q9 = b as DecoratedTree of HP-WFF by A6;
reconsider p9 = a as DecoratedTree of HP-WFF by A5;
take (p => q) -tree (p9,q9) ; ::_thesis: S1[p,q,a,b,(p => q) -tree (p9,q9)]
thus S1[p,q,a,b,(p => q) -tree (p9,q9)] ; ::_thesis: verum
end;
suppose ( not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ) ; ::_thesis: ex d being set st S1[p,q,a,b,d]
hence ex d being set st S1[p,q,a,b,d] ; ::_thesis: verum
end;
end;
end;
A7: for p, q being Element of HP-WFF
for a, b, c, d being set st S1[p,q,a,b,c] & S1[p,q,a,b,d] holds
c = d ;
A8: for p, q being Element of HP-WFF
for a, b, c, d being set st S2[p,q,a,b,c] & S2[p,q,a,b,d] holds
c = d ;
consider M being ManySortedSet of HP-WFF such that
A9: M . VERUM = root-tree VERUM and
A10: for n being Element of NAT holds M . (prop n) = H1(n) and
A11: for p, q being Element of HP-WFF holds
( S2[p,q,M . p,M . q,M . (p '&' q)] & S1[p,q,M . p,M . q,M . (p => q)] ) from HILBERT2:sch_3(A1, A4, A8, A7);
take M ; ::_thesis: ( M . VERUM = root-tree VERUM & ( for n being Element of NAT holds M . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) ) ) )
thus M . VERUM = root-tree VERUM by A9; ::_thesis: ( ( for n being Element of NAT holds M . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) ) ) )
thus for n being Element of NAT holds M . (prop n) = root-tree (prop n) by A10; ::_thesis: for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) )
let p, q be Element of HP-WFF ; ::_thesis: ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) )
A12: ( S2[p,q,M . p,M . q,M . (p '&' q)] & S1[p,q,M . p,M . q,M . (p => q)] ) by A11;
defpred S3[ Element of HP-WFF ] means M . $1 is DecoratedTree of HP-WFF ;
A13: for r, s being Element of HP-WFF st S3[r] & S3[s] holds
( S3[r '&' s] & S3[r => s] )
proof
let r, s be Element of HP-WFF ; ::_thesis: ( S3[r] & S3[s] implies ( S3[r '&' s] & S3[r => s] ) )
assume A14: ( M . r is DecoratedTree of HP-WFF & M . s is DecoratedTree of HP-WFF ) ; ::_thesis: ( S3[r '&' s] & S3[r => s] )
S2[r,s,M . r,M . s,M . (r '&' s)] by A11;
hence M . (r '&' s) is DecoratedTree of HP-WFF by A14; ::_thesis: S3[r => s]
S1[r,s,M . r,M . s,M . (r => s)] by A11;
hence S3[r => s] by A14; ::_thesis: verum
end;
A15: for n being Element of NAT holds S3[ prop n]
proof
let n be Element of NAT ; ::_thesis: S3[ prop n]
M . (prop n) = root-tree (prop n) by A10;
hence S3[ prop n] ; ::_thesis: verum
end;
A16: S3[ VERUM ] by A9;
for p being Element of HP-WFF holds S3[p] from HILBERT2:sch_2(A16, A15, A13);
hence ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) ) by A12; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) & b2 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b2 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b2 . p & q9 = b2 . q & b2 . (p '&' q) = (p '&' q) -tree (p9,q9) & b2 . (p => q) = (p => q) -tree (p9,q9) ) ) holds
b1 = b2
proof
let M1, M2 be ManySortedSet of HP-WFF ; ::_thesis: ( M1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds M1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = (p '&' q) -tree (p9,q9) & M1 . (p => q) = (p => q) -tree (p9,q9) ) ) & M2 . VERUM = root-tree VERUM & ( for n being Element of NAT holds M2 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = (p '&' q) -tree (p9,q9) & M2 . (p => q) = (p => q) -tree (p9,q9) ) ) implies M1 = M2 )
assume that
A17: M1 . VERUM = root-tree VERUM and
A18: for n being Element of NAT holds M1 . (prop n) = root-tree (prop n) and
A19: for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = (p '&' q) -tree (p9,q9) & M1 . (p => q) = (p => q) -tree (p9,q9) ) and
A20: M2 . VERUM = root-tree VERUM and
A21: for n being Element of NAT holds M2 . (prop n) = root-tree (prop n) and
A22: for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = (p '&' q) -tree (p9,q9) & M2 . (p => q) = (p => q) -tree (p9,q9) ) ; ::_thesis: M1 = M2
defpred S1[ Element of HP-WFF ] means M1 . $1 = M2 . $1;
A23: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; ::_thesis: S1[ prop n]
thus M1 . (prop n) = root-tree (prop n) by A18
.= M2 . (prop n) by A21 ; ::_thesis: verum
end;
A24: for r, s being Element of HP-WFF st S1[r] & S1[s] holds
( S1[r '&' s] & S1[r => s] )
proof
let r, s be Element of HP-WFF ; ::_thesis: ( S1[r] & S1[s] implies ( S1[r '&' s] & S1[r => s] ) )
assume A25: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; ::_thesis: ( S1[r '&' s] & S1[r => s] )
A26: ( ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M1 . r & q9 = M1 . s & M1 . (r '&' s) = (r '&' s) -tree (p9,q9) & M1 . (r => s) = (r => s) -tree (p9,q9) ) & ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M2 . r & q9 = M2 . s & M2 . (r '&' s) = (r '&' s) -tree (p9,q9) & M2 . (r => s) = (r => s) -tree (p9,q9) ) ) by A19, A22;
hence M1 . (r '&' s) = M2 . (r '&' s) by A25; ::_thesis: S1[r => s]
thus S1[r => s] by A25, A26; ::_thesis: verum
end;
A27: S1[ VERUM ] by A17, A20;
for r being Element of HP-WFF holds S1[r] from HILBERT2:sch_2(A27, A23, A24);
then for r being set st r in HP-WFF holds
M1 . r = M2 . r ;
hence M1 = M2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines HP-Subformulae HILBERT2:def_9_:_
for b1 being ManySortedSet of HP-WFF holds
( b1 = HP-Subformulae iff ( b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) ) );
definition
let p be Element of HP-WFF ;
func Subformulae p -> DecoratedTree of HP-WFF equals :: HILBERT2:def 10
HP-Subformulae . p;
correctness
coherence
HP-Subformulae . p is DecoratedTree of HP-WFF ;
proof
defpred S1[ Element of HP-WFF ] means HP-Subformulae . $1 is DecoratedTree of HP-WFF ;
A1: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; ::_thesis: S1[ prop n]
HP-Subformulae . (prop n) = root-tree (prop n) by Def9;
hence S1[ prop n] ; ::_thesis: verum
end;
A2: for r, s being Element of HP-WFF st S1[r] & S1[s] holds
( S1[r '&' s] & S1[r => s] )
proof
let r, s be Element of HP-WFF ; ::_thesis: ( S1[r] & S1[s] implies ( S1[r '&' s] & S1[r => s] ) )
ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = HP-Subformulae . r & q9 = HP-Subformulae . s & HP-Subformulae . (r '&' s) = (r '&' s) -tree (p9,q9) & HP-Subformulae . (r => s) = (r => s) -tree (p9,q9) ) by Def9;
hence ( S1[r] & S1[s] implies ( S1[r '&' s] & S1[r => s] ) ) ; ::_thesis: verum
end;
A3: S1[ VERUM ] by Def9;
for p being Element of HP-WFF holds S1[p] from HILBERT2:sch_2(A3, A1, A2);
hence HP-Subformulae . p is DecoratedTree of HP-WFF ; ::_thesis: verum
end;
end;
:: deftheorem defines Subformulae HILBERT2:def_10_:_
for p being Element of HP-WFF holds Subformulae p = HP-Subformulae . p;
theorem Th30: :: HILBERT2:30
Subformulae VERUM = root-tree VERUM by Def9;
theorem :: HILBERT2:31
for n being Element of NAT holds Subformulae (prop n) = root-tree (prop n) by Def9;
theorem Th32: :: HILBERT2:32
for p, q being Element of HP-WFF holds Subformulae (p '&' q) = (p '&' q) -tree ((Subformulae p),(Subformulae q))
proof
let p, q be Element of HP-WFF ; ::_thesis: Subformulae (p '&' q) = (p '&' q) -tree ((Subformulae p),(Subformulae q))
ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = HP-Subformulae . p & q9 = HP-Subformulae . q & HP-Subformulae . (p '&' q) = (p '&' q) -tree (p9,q9) & HP-Subformulae . (p => q) = (p => q) -tree (p9,q9) ) by Def9;
hence Subformulae (p '&' q) = (p '&' q) -tree ((Subformulae p),(Subformulae q)) ; ::_thesis: verum
end;
theorem Th33: :: HILBERT2:33
for p, q being Element of HP-WFF holds Subformulae (p => q) = (p => q) -tree ((Subformulae p),(Subformulae q))
proof
let p, q be Element of HP-WFF ; ::_thesis: Subformulae (p => q) = (p => q) -tree ((Subformulae p),(Subformulae q))
ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = HP-Subformulae . p & q9 = HP-Subformulae . q & HP-Subformulae . (p '&' q) = (p '&' q) -tree (p9,q9) & HP-Subformulae . (p => q) = (p => q) -tree (p9,q9) ) by Def9;
hence Subformulae (p => q) = (p => q) -tree ((Subformulae p),(Subformulae q)) ; ::_thesis: verum
end;
theorem Th34: :: HILBERT2:34
for p being Element of HP-WFF holds (Subformulae p) . {} = p
proof
let p be Element of HP-WFF ; ::_thesis: (Subformulae p) . {} = p
percases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;
suppose p is conjunctive ; ::_thesis: (Subformulae p) . {} = p
then consider r, s being Element of HP-WFF such that
A1: p = r '&' s by Def6;
Subformulae p = p -tree ((Subformulae r),(Subformulae s)) by A1, Th32;
hence (Subformulae p) . {} = p by Th6; ::_thesis: verum
end;
suppose p is conditional ; ::_thesis: (Subformulae p) . {} = p
then consider r, s being Element of HP-WFF such that
A2: p = r => s by Def7;
Subformulae p = p -tree ((Subformulae r),(Subformulae s)) by A2, Th33;
hence (Subformulae p) . {} = p by Th6; ::_thesis: verum
end;
suppose p is simple ; ::_thesis: (Subformulae p) . {} = p
then ex n being Element of NAT st p = prop n by Def8;
then Subformulae p = root-tree p by Def9;
hence (Subformulae p) . {} = p by TREES_4:3; ::_thesis: verum
end;
suppose p = VERUM ; ::_thesis: (Subformulae p) . {} = p
hence (Subformulae p) . {} = p by Th30, TREES_4:3; ::_thesis: verum
end;
end;
end;
theorem Th35: :: HILBERT2:35
for p being Element of HP-WFF
for f being Element of dom (Subformulae p) holds (Subformulae p) | f = Subformulae ((Subformulae p) . f)
proof
let p be Element of HP-WFF ; ::_thesis: for f being Element of dom (Subformulae p) holds (Subformulae p) | f = Subformulae ((Subformulae p) . f)
let f be Element of dom (Subformulae p); ::_thesis: (Subformulae p) | f = Subformulae ((Subformulae p) . f)
defpred S1[ FinSequence of NAT ] means ex q being Element of HP-WFF st
( q = (Subformulae p) . $1 & (Subformulae p) | $1 = Subformulae q );
A1: for f being Element of dom (Subformulae p) st S1[f] holds
for n being Element of NAT st f ^ <*n*> in dom (Subformulae p) holds
S1[f ^ <*n*>]
proof
let f be Element of dom (Subformulae p); ::_thesis: ( S1[f] implies for n being Element of NAT st f ^ <*n*> in dom (Subformulae p) holds
S1[f ^ <*n*>] )
given q being Element of HP-WFF such that q = (Subformulae p) . f and
A2: (Subformulae p) | f = Subformulae q ; ::_thesis: for n being Element of NAT st f ^ <*n*> in dom (Subformulae p) holds
S1[f ^ <*n*>]
let n be Element of NAT ; ::_thesis: ( f ^ <*n*> in dom (Subformulae p) implies S1[f ^ <*n*>] )
assume A3: f ^ <*n*> in dom (Subformulae p) ; ::_thesis: S1[f ^ <*n*>]
A4: (Subformulae p) | (f ^ <*n*>) = (Subformulae q) | <*n*> by A2, A3, TREES_9:3;
A5: (dom (Subformulae p)) | f = dom (Subformulae q) by A2, TREES_2:def_10;
then A6: <*n*> in dom (Subformulae q) by A3, TREES_1:def_6;
then A7: (Subformulae p) . (f ^ <*n*>) = (Subformulae q) . <*n*> by A2, A5, TREES_2:def_10;
percases ( q is conjunctive or q is conditional or q is simple or q = VERUM ) by Th9;
suppose q is conjunctive ; ::_thesis: S1[f ^ <*n*>]
then consider r, s being Element of HP-WFF such that
A8: q = r '&' s by Def6;
A9: Subformulae q = (r '&' s) -tree ((Subformulae r),(Subformulae s)) by A8, Th32;
then A10: dom (Subformulae q) = tree ((dom (Subformulae r)),(dom (Subformulae s))) by TREES_4:14;
now__::_thesis:_ex_r_being_Element_of_HP-WFF_st_
(_r_=_(Subformulae_p)_._(f_^_<*n*>)_&_(Subformulae_p)_|_(f_^_<*n*>)_=_Subformulae_r_)
percases ( n = 0 or n = 1 ) by A6, A10, Th5;
supposeA11: n = 0 ; ::_thesis: ex r being Element of HP-WFF st
( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )
take r = r; ::_thesis: ( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )
thus r = (Subformulae r) . {} by Th34
.= (Subformulae p) . (f ^ <*n*>) by A7, A9, A11, Th7 ; ::_thesis: (Subformulae p) | (f ^ <*n*>) = Subformulae r
thus (Subformulae p) | (f ^ <*n*>) = Subformulae r by A4, A9, A11, Th8; ::_thesis: verum
end;
supposeA12: n = 1 ; ::_thesis: ex s being Element of HP-WFF st
( s = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae s )
take s = s; ::_thesis: ( s = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae s )
thus s = (Subformulae s) . {} by Th34
.= (Subformulae p) . (f ^ <*n*>) by A7, A9, A12, Th7 ; ::_thesis: (Subformulae p) | (f ^ <*n*>) = Subformulae s
thus (Subformulae p) | (f ^ <*n*>) = Subformulae s by A4, A9, A12, Th8; ::_thesis: verum
end;
end;
end;
hence S1[f ^ <*n*>] ; ::_thesis: verum
end;
suppose q is conditional ; ::_thesis: S1[f ^ <*n*>]
then consider r, s being Element of HP-WFF such that
A13: q = r => s by Def7;
A14: Subformulae q = (r => s) -tree ((Subformulae r),(Subformulae s)) by A13, Th33;
then A15: dom (Subformulae q) = tree ((dom (Subformulae r)),(dom (Subformulae s))) by TREES_4:14;
now__::_thesis:_ex_r_being_Element_of_HP-WFF_st_
(_r_=_(Subformulae_p)_._(f_^_<*n*>)_&_(Subformulae_p)_|_(f_^_<*n*>)_=_Subformulae_r_)
percases ( n = 0 or n = 1 ) by A6, A15, Th5;
supposeA16: n = 0 ; ::_thesis: ex r being Element of HP-WFF st
( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )
take r = r; ::_thesis: ( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )
thus r = (Subformulae r) . {} by Th34
.= (Subformulae p) . (f ^ <*n*>) by A7, A14, A16, Th7 ; ::_thesis: (Subformulae p) | (f ^ <*n*>) = Subformulae r
thus (Subformulae p) | (f ^ <*n*>) = Subformulae r by A4, A14, A16, Th8; ::_thesis: verum
end;
supposeA17: n = 1 ; ::_thesis: ex s being Element of HP-WFF st
( s = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae s )
take s = s; ::_thesis: ( s = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae s )
thus s = (Subformulae s) . {} by Th34
.= (Subformulae p) . (f ^ <*n*>) by A7, A14, A17, Th7 ; ::_thesis: (Subformulae p) | (f ^ <*n*>) = Subformulae s
thus (Subformulae p) | (f ^ <*n*>) = Subformulae s by A4, A14, A17, Th8; ::_thesis: verum
end;
end;
end;
hence S1[f ^ <*n*>] ; ::_thesis: verum
end;
suppose q is simple ; ::_thesis: S1[f ^ <*n*>]
then consider k being Element of NAT such that
A18: q = prop k by Def8;
Subformulae q = root-tree (prop k) by A18, Def9;
then dom (Subformulae q) = {{}} by TREES_1:29, TREES_4:3;
hence S1[f ^ <*n*>] by A6, TARSKI:def_1; ::_thesis: verum
end;
suppose q = VERUM ; ::_thesis: S1[f ^ <*n*>]
then dom (Subformulae q) = {{}} by Th30, TREES_1:29, TREES_4:3;
hence S1[f ^ <*n*>] by A6, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
(Subformulae p) . {} = p by Th34;
then A19: S1[ <*> NAT] by TREES_9:1;
for f being Element of dom (Subformulae p) holds S1[f] from HILBERT2:sch_1(A19, A1);
then S1[f] ;
hence (Subformulae p) | f = Subformulae ((Subformulae p) . f) ; ::_thesis: verum
end;
theorem :: HILBERT2:36
for p, q being Element of HP-WFF holds
( not p in Leaves (Subformulae q) or p = VERUM or p is simple )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( not p in Leaves (Subformulae q) or p = VERUM or p is simple )
assume p in Leaves (Subformulae q) ; ::_thesis: ( p = VERUM or p is simple )
then p in (Subformulae q) .: (Leaves (dom (Subformulae q))) by TREES_2:def_9;
then consider x being set such that
A1: x in dom (Subformulae q) and
A2: x in Leaves (dom (Subformulae q)) and
A3: p = (Subformulae q) . x by FUNCT_1:def_6;
reconsider f = x as Element of dom (Subformulae q) by A1;
A4: (Subformulae q) | f = Subformulae p by A3, Th35;
A5: not p is conditional
proof
assume p is conditional ; ::_thesis: contradiction
then consider r, s being Element of HP-WFF such that
A6: p = r => s by Def7;
Subformulae p = p -tree ((Subformulae r),(Subformulae s)) by A6, Th33;
hence contradiction by A2, A4, TREES_9:6; ::_thesis: verum
end;
not p is conjunctive
proof
assume p is conjunctive ; ::_thesis: contradiction
then consider r, s being Element of HP-WFF such that
A7: p = r '&' s by Def6;
Subformulae p = p -tree ((Subformulae r),(Subformulae s)) by A7, Th32;
hence contradiction by A2, A4, TREES_9:6; ::_thesis: verum
end;
hence ( p = VERUM or p is simple ) by A5, Th9; ::_thesis: verum
end;