:: 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;