:: HILBERT3 semantic presentation begin registration let m, n be non zero Nat; cluster(0,n) --> (m,0) -> one-to-one ; coherence (0,n) --> (m,0) is one-to-one proof set f = (0,n) --> (m,0); let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom ((0,n) --> (m,0)) or not x2 in dom ((0,n) --> (m,0)) or not ((0,n) --> (m,0)) . x1 = ((0,n) --> (m,0)) . x2 or x1 = x2 ) assume that A1: x1 in dom ((0,n) --> (m,0)) and A2: x2 in dom ((0,n) --> (m,0)) ; ::_thesis: ( not ((0,n) --> (m,0)) . x1 = ((0,n) --> (m,0)) . x2 or x1 = x2 ) A3: dom ((0,n) --> (m,0)) = {0,n} by FUNCT_4:62; then A4: ( x2 = 0 or x2 = n ) by A2, TARSKI:def_2; A5: ((0,n) --> (m,0)) . 0 = m by FUNCT_4:63; ( x1 = 0 or x1 = n ) by A3, A1, TARSKI:def_2; hence ( not ((0,n) --> (m,0)) . x1 = ((0,n) --> (m,0)) . x2 or x1 = x2 ) by A4, A5, FUNCT_4:63; ::_thesis: verum end; cluster(n,0) --> (0,m) -> one-to-one ; coherence (n,0) --> (0,m) is one-to-one proof set f = (n,0) --> (0,m); let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom ((n,0) --> (0,m)) or not x2 in dom ((n,0) --> (0,m)) or not ((n,0) --> (0,m)) . x1 = ((n,0) --> (0,m)) . x2 or x1 = x2 ) assume that A6: x1 in dom ((n,0) --> (0,m)) and A7: x2 in dom ((n,0) --> (0,m)) ; ::_thesis: ( not ((n,0) --> (0,m)) . x1 = ((n,0) --> (0,m)) . x2 or x1 = x2 ) A8: dom ((n,0) --> (0,m)) = {0,n} by FUNCT_4:62; then A9: ( x2 = 0 or x2 = n ) by A7, TARSKI:def_2; A10: ((n,0) --> (0,m)) . 0 = m by FUNCT_4:63; ( x1 = 0 or x1 = n ) by A8, A6, TARSKI:def_2; hence ( not ((n,0) --> (0,m)) . x1 = ((n,0) --> (0,m)) . x2 or x1 = x2 ) by A9, A10, FUNCT_4:63; ::_thesis: verum end; end; theorem :: HILBERT3:1 for i being Integer holds ( i is even iff i - 1 is odd ) ; theorem :: HILBERT3:2 for i being Integer holds ( i is odd iff i - 1 is even ) ; theorem Th3: :: HILBERT3:3 for X being trivial set for x being set st x in X holds for f being Function of X,X holds x is_a_fixpoint_of f proof let X be trivial set ; ::_thesis: for x being set st x in X holds for f being Function of X,X holds x is_a_fixpoint_of f let x be set ; ::_thesis: ( x in X implies for f being Function of X,X holds x is_a_fixpoint_of f ) assume A1: x in X ; ::_thesis: for f being Function of X,X holds x is_a_fixpoint_of f then consider y being set such that A2: X = {y} by ZFMISC_1:131; let f be Function of X,X; ::_thesis: x is_a_fixpoint_of f thus x in dom f by A1, FUNCT_2:52; :: according to ABIAN:def_3 ::_thesis: x = f . x then A3: f . x in rng f by FUNCT_1:def_3; A4: rng f c= X by RELAT_1:def_19; thus x = y by A1, A2, TARSKI:def_1 .= f . x by A2, A3, A4, TARSKI:def_1 ; ::_thesis: verum end; theorem Th4: :: HILBERT3:4 for f being Function-yielding Function holds SubFuncs (rng f) = rng f proof let f be Function-yielding Function; ::_thesis: SubFuncs (rng f) = rng f for x being set st x in rng f holds x is Function proof let x be set ; ::_thesis: ( x in rng f implies x is Function ) assume x in rng f ; ::_thesis: x is Function then ex y being set st ( y in dom f & x = f . y ) by FUNCT_1:def_3; hence x is Function ; ::_thesis: verum end; then for x being set holds ( x in rng f iff ( x in rng f & x is Function ) ) ; hence SubFuncs (rng f) = rng f by FUNCT_6:def_1; ::_thesis: verum end; theorem Th5: :: HILBERT3:5 for A, B, x being set for f being Function st x in A & f in Funcs (A,B) holds f . x in B proof let A, B, x be set ; ::_thesis: for f being Function st x in A & f in Funcs (A,B) holds f . x in B let f be Function; ::_thesis: ( x in A & f in Funcs (A,B) implies f . x in B ) assume A1: x in A ; ::_thesis: ( not f in Funcs (A,B) or f . x in B ) assume A2: f in Funcs (A,B) ; ::_thesis: f . x in B then A3: f is Function of A,B by FUNCT_2:66; ( B = {} implies A = {} ) by A2; hence f . x in B by A1, A3, FUNCT_2:5; ::_thesis: verum end; theorem Th6: :: HILBERT3:6 for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds for f being Function of A,(Funcs (B,C)) holds doms f = A --> B proof let A, B, C be set ; ::_thesis: ( ( not C = {} or B = {} or A = {} ) implies for f being Function of A,(Funcs (B,C)) holds doms f = A --> B ) assume ( not C = {} or B = {} or A = {} ) ; ::_thesis: for f being Function of A,(Funcs (B,C)) holds doms f = A --> B then A1: ( Funcs (B,C) = {} implies A = {} ) by FUNCT_2:8; let f be Function of A,(Funcs (B,C)); ::_thesis: doms f = A --> B reconsider g = f as ManySortedFunction of A by A1; now__::_thesis:_for_i_being_set_st_i_in_A_holds_ (doms_g)_._i_=_(A_-->_B)_._i let i be set ; ::_thesis: ( i in A implies (doms g) . i = (A --> B) . i ) assume A2: i in A ; ::_thesis: (doms g) . i = (A --> B) . i then A3: g . i in Funcs (B,C) by A1, FUNCT_2:5; thus (doms g) . i = dom (g . i) by A2, MSSUBFAM:14 .= B by A3, FUNCT_2:92 .= (A --> B) . i by A2, FUNCOP_1:7 ; ::_thesis: verum end; hence doms f = A --> B by PBOOLE:3; ::_thesis: verum end; theorem :: HILBERT3:7 for x being set holds {} . x = {} ; theorem Th8: :: HILBERT3:8 for X being set for A being Subset of X holds ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X) proof let X be set ; ::_thesis: for A being Subset of X holds ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X) let A be Subset of X; ::_thesis: ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X) set f = ((0,1) --> (1,0)) * (chi (A,X)); A1: dom (chi (A,X)) = X by FUNCT_3:def_3; A2: for x being set st x in X holds ( ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) & ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 ) ) proof let x be set ; ::_thesis: ( x in X implies ( ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) & ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 ) ) ) assume A3: x in X ; ::_thesis: ( ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) & ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 ) ) thus ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) ::_thesis: ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 ) proof assume x in A ` ; ::_thesis: (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 then not x in A by XBOOLE_0:def_5; then (chi (A,X)) . x = 0 by A3, FUNCT_3:def_3; then (((0,1) --> (1,0)) * (chi (A,X))) . x = ((0,1) --> (1,0)) . 0 by A1, A3, FUNCT_1:13; hence (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 by FUNCT_4:63; ::_thesis: verum end; assume not x in A ` ; ::_thesis: (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 then x in A by A3, XBOOLE_0:def_5; then (chi (A,X)) . x = 1 by FUNCT_3:def_3; then (((0,1) --> (1,0)) * (chi (A,X))) . x = ((0,1) --> (1,0)) . 1 by A1, A3, FUNCT_1:13; hence (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 by FUNCT_4:63; ::_thesis: verum end; dom ((0,1) --> (1,0)) = {0,1} by FUNCT_4:62; then rng (chi (A,X)) c= dom ((0,1) --> (1,0)) by FUNCT_3:39; then dom (((0,1) --> (1,0)) * (chi (A,X))) = X by A1, RELAT_1:27; hence ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X) by A2, FUNCT_3:def_3; ::_thesis: verum end; theorem Th9: :: HILBERT3:9 for X being set for A being Subset of X holds ((0,1) --> (1,0)) * (chi ((A `),X)) = chi (A,X) proof let X be set ; ::_thesis: for A being Subset of X holds ((0,1) --> (1,0)) * (chi ((A `),X)) = chi (A,X) let A be Subset of X; ::_thesis: ((0,1) --> (1,0)) * (chi ((A `),X)) = chi (A,X) (A `) ` = A ; hence ((0,1) --> (1,0)) * (chi ((A `),X)) = chi (A,X) by Th8; ::_thesis: verum end; theorem Th10: :: HILBERT3:10 for a, b, x, y, x9, y9 being set st a <> b & (a,b) --> (x,y) = (a,b) --> (x9,y9) holds ( x = x9 & y = y9 ) proof let a, b, x, y, x9, y9 be set ; ::_thesis: ( a <> b & (a,b) --> (x,y) = (a,b) --> (x9,y9) implies ( x = x9 & y = y9 ) ) assume that A1: a <> b and A2: (a,b) --> (x,y) = (a,b) --> (x9,y9) ; ::_thesis: ( x = x9 & y = y9 ) thus x = ((a,b) --> (x,y)) . a by A1, FUNCT_4:63 .= x9 by A1, A2, FUNCT_4:63 ; ::_thesis: y = y9 thus y = ((a,b) --> (x,y)) . b by FUNCT_4:63 .= y9 by A2, FUNCT_4:63 ; ::_thesis: verum end; theorem Th11: :: HILBERT3:11 for a, b, x, y, X, Y being set st a <> b & x in X & y in Y holds (a,b) --> (x,y) in product ((a,b) --> (X,Y)) proof let a, b, x, y, X, Y be set ; ::_thesis: ( a <> b & x in X & y in Y implies (a,b) --> (x,y) in product ((a,b) --> (X,Y)) ) assume that A1: a <> b and A2: ( x in X & y in Y ) ; ::_thesis: (a,b) --> (x,y) in product ((a,b) --> (X,Y)) ( {x} c= X & {y} c= Y ) by A2, ZFMISC_1:31; then product ((a,b) --> ({x},{y})) c= product ((a,b) --> (X,Y)) by TOPREAL6:21; then {((a,b) --> (x,y))} c= product ((a,b) --> (X,Y)) by A1, CARD_3:47; hence (a,b) --> (x,y) in product ((a,b) --> (X,Y)) by ZFMISC_1:31; ::_thesis: verum end; theorem Th12: :: HILBERT3:12 for D being non empty set for f being Function of 2,D ex d1, d2 being Element of D st f = (0,1) --> (d1,d2) proof let D be non empty set ; ::_thesis: for f being Function of 2,D ex d1, d2 being Element of D st f = (0,1) --> (d1,d2) let f be Function of 2,D; ::_thesis: ex d1, d2 being Element of D st f = (0,1) --> (d1,d2) ( 0 in 2 & 1 in 2 ) by CARD_1:50, TARSKI:def_2; then reconsider d1 = f . 0, d2 = f . 1 as Element of D by FUNCT_2:5; take d1 ; ::_thesis: ex d2 being Element of D st f = (0,1) --> (d1,d2) take d2 ; ::_thesis: f = (0,1) --> (d1,d2) dom f = {0,1} by CARD_1:50, FUNCT_2:def_1; hence f = (0,1) --> (d1,d2) by FUNCT_4:66; ::_thesis: verum end; theorem Th13: :: HILBERT3:13 for a, b, c, d being set st a <> b holds ((a,b) --> (c,d)) * ((a,b) --> (b,a)) = (a,b) --> (d,c) proof let a, b, c, d be set ; ::_thesis: ( a <> b implies ((a,b) --> (c,d)) * ((a,b) --> (b,a)) = (a,b) --> (d,c) ) assume A1: a <> b ; ::_thesis: ((a,b) --> (c,d)) * ((a,b) --> (b,a)) = (a,b) --> (d,c) set f = ((a,b) --> (c,d)) * ((a,b) --> (b,a)); A2: dom ((a,b) --> (b,a)) = {a,b} by FUNCT_4:62; b in {a,b} by TARSKI:def_2; then A3: (((a,b) --> (c,d)) * ((a,b) --> (b,a))) . b = ((a,b) --> (c,d)) . (((a,b) --> (b,a)) . b) by A2, FUNCT_1:13 .= ((a,b) --> (c,d)) . a by FUNCT_4:63 .= c by A1, FUNCT_4:63 ; a in {a,b} by TARSKI:def_2; then A4: (((a,b) --> (c,d)) * ((a,b) --> (b,a))) . a = ((a,b) --> (c,d)) . (((a,b) --> (b,a)) . a) by A2, FUNCT_1:13 .= ((a,b) --> (c,d)) . b by A1, FUNCT_4:63 .= d by FUNCT_4:63 ; rng ((a,b) --> (b,a)) = {a,b} by A1, FUNCT_4:64 .= dom ((a,b) --> (c,d)) by FUNCT_4:62 ; then dom (((a,b) --> (c,d)) * ((a,b) --> (b,a))) = {a,b} by A2, RELAT_1:27; hence ((a,b) --> (c,d)) * ((a,b) --> (b,a)) = (a,b) --> (d,c) by A4, A3, FUNCT_4:66; ::_thesis: verum end; theorem Th14: :: HILBERT3:14 for a, b, c, d being set for f being Function st a <> b & c in dom f & d in dom f holds f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d)) proof let a, b, c, d be set ; ::_thesis: for f being Function st a <> b & c in dom f & d in dom f holds f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d)) let f be Function; ::_thesis: ( a <> b & c in dom f & d in dom f implies f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d)) ) assume that A1: a <> b and A2: ( c in dom f & d in dom f ) ; ::_thesis: f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d)) A3: dom ((a,b) --> (c,d)) = {a,b} by FUNCT_4:62; then a in dom ((a,b) --> (c,d)) by TARSKI:def_2; then A4: (f * ((a,b) --> (c,d))) . a = f . (((a,b) --> (c,d)) . a) by FUNCT_1:13 .= f . c by A1, FUNCT_4:63 ; b in dom ((a,b) --> (c,d)) by A3, TARSKI:def_2; then A5: (f * ((a,b) --> (c,d))) . b = f . (((a,b) --> (c,d)) . b) by FUNCT_1:13 .= f . d by FUNCT_4:63 ; A6: rng ((a,b) --> (c,d)) c= {c,d} by FUNCT_4:62; {c,d} c= dom f by A2, ZFMISC_1:32; then dom (f * ((a,b) --> (c,d))) = {a,b} by A3, A6, RELAT_1:27, XBOOLE_1:1; hence f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d)) by A4, A5, FUNCT_4:66; ::_thesis: verum end; theorem Th15: :: HILBERT3:15 (0,1) --> (1,0) is Permutation of 2 proof set f = (0,1) --> (1,0); A1: rng ((0,1) --> (1,0)) = 2 by CARD_1:50, FUNCT_4:64; dom ((0,1) --> (1,0)) = 2 by CARD_1:50, FUNCT_4:62; then (0,1) --> (1,0) is Function of 2,2 by A1, FUNCT_2:def_1, RELSET_1:4; hence (0,1) --> (1,0) is Permutation of 2 by A1, FUNCT_2:57; ::_thesis: verum end; begin registration let f, g be one-to-one Function; cluster[:f,g:] -> one-to-one ; coherence [:f,g:] is one-to-one proof let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom [:f,g:] or not y in dom [:f,g:] or not [:f,g:] . x = [:f,g:] . y or x = y ) assume that A1: x in dom [:f,g:] and A2: y in dom [:f,g:] and A3: [:f,g:] . x = [:f,g:] . y ; ::_thesis: x = y A4: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def_8; then consider x1, x2 being set such that A5: x1 in dom f and A6: x2 in dom g and A7: x = [x1,x2] by A1, ZFMISC_1:def_2; A8: [:f,g:] . (x1,x2) = [(f . x1),(g . x2)] by A5, A6, FUNCT_3:def_8; consider y1, y2 being set such that A9: y1 in dom f and A10: y2 in dom g and A11: y = [y1,y2] by A2, A4, ZFMISC_1:def_2; A12: [:f,g:] . (y1,y2) = [(f . y1),(g . y2)] by A9, A10, FUNCT_3:def_8; then f . x1 = f . y1 by A3, A7, A11, A8, XTUPLE_0:1; then A13: x1 = y1 by A5, A9, FUNCT_1:def_4; g . x2 = g . y2 by A3, A7, A11, A8, A12, XTUPLE_0:1; hence x = y by A6, A7, A10, A11, A13, FUNCT_1:def_4; ::_thesis: verum end; end; theorem Th16: :: HILBERT3:16 for A, B being non empty set for C, D being set for f being Function of C,A for g being Function of D,B holds (pr1 (A,B)) * [:f,g:] = f * (pr1 (C,D)) proof let A, B be non empty set ; ::_thesis: for C, D being set for f being Function of C,A for g being Function of D,B holds (pr1 (A,B)) * [:f,g:] = f * (pr1 (C,D)) let C, D be set ; ::_thesis: for f being Function of C,A for g being Function of D,B holds (pr1 (A,B)) * [:f,g:] = f * (pr1 (C,D)) let f be Function of C,A; ::_thesis: for g being Function of D,B holds (pr1 (A,B)) * [:f,g:] = f * (pr1 (C,D)) let g be Function of D,B; ::_thesis: (pr1 (A,B)) * [:f,g:] = f * (pr1 (C,D)) ( not C = {} or A = {} or [:C,D:] = {} ) ; then reconsider F = f * (pr1 (C,D)) as Function of [:C,D:],A ; ( not D = {} or A = {} or [:C,D:] = {} ) ; then reconsider G = g * (pr2 (C,D)) as Function of [:C,D:],B ; thus (pr1 (A,B)) * [:f,g:] = (pr1 (A,B)) * <:F,G:> by FUNCT_3:77 .= f * (pr1 (C,D)) by FUNCT_3:62 ; ::_thesis: verum end; theorem Th17: :: HILBERT3:17 for A, B being non empty set for C, D being set for f being Function of C,A for g being Function of D,B holds (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D)) proof let A, B be non empty set ; ::_thesis: for C, D being set for f being Function of C,A for g being Function of D,B holds (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D)) let C, D be set ; ::_thesis: for f being Function of C,A for g being Function of D,B holds (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D)) let f be Function of C,A; ::_thesis: for g being Function of D,B holds (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D)) let g be Function of D,B; ::_thesis: (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D)) ( not C = {} or A = {} or [:C,D:] = {} ) ; then reconsider F = f * (pr1 (C,D)) as Function of [:C,D:],A ; ( not D = {} or A = {} or [:C,D:] = {} ) ; then reconsider G = g * (pr2 (C,D)) as Function of [:C,D:],B ; thus (pr2 (A,B)) * [:f,g:] = (pr2 (A,B)) * <:F,G:> by FUNCT_3:77 .= g * (pr2 (C,D)) by FUNCT_3:62 ; ::_thesis: verum end; theorem :: HILBERT3:18 for g being Function holds {} .. g = {} proof let g be Function; ::_thesis: {} .. g = {} dom {} = {} ; then dom ({} .. g) = {} by PRALG_1:def_17; hence {} .. g = {} ; ::_thesis: verum end; theorem Th19: :: HILBERT3:19 for f being Function-yielding Function for g, h being Function holds (f .. g) * h = (f * h) .. (g * h) proof let f be Function-yielding Function; ::_thesis: for g, h being Function holds (f .. g) * h = (f * h) .. (g * h) let g, h be Function; ::_thesis: (f .. g) * h = (f * h) .. (g * h) A1: for x being set st x in dom (f * h) holds ((f .. g) * h) . x = ((f * h) . x) . ((g * h) . x) proof let x be set ; ::_thesis: ( x in dom (f * h) implies ((f .. g) * h) . x = ((f * h) . x) . ((g * h) . x) ) assume A2: x in dom (f * h) ; ::_thesis: ((f .. g) * h) . x = ((f * h) . x) . ((g * h) . x) then A3: x in dom h by FUNCT_1:11; A4: h . x in dom f by A2, FUNCT_1:11; thus ((f .. g) * h) . x = (f .. g) . (h . x) by A3, FUNCT_1:13 .= (f . (h . x)) . (g . (h . x)) by A4, PRALG_1:def_17 .= ((f * h) . x) . (g . (h . x)) by A3, FUNCT_1:13 .= ((f * h) . x) . ((g * h) . x) by A3, FUNCT_1:13 ; ::_thesis: verum end; dom (f .. g) = dom f by PRALG_1:def_17; then dom ((f .. g) * h) = dom (f * h) by RELAT_1:163; hence (f .. g) * h = (f * h) .. (g * h) by A1, PRALG_1:def_17; ::_thesis: verum end; theorem :: HILBERT3:20 for C being set for A being non empty set for f being Function of A,(Funcs ({},C)) for g being Function of A,{} holds rng (f .. g) = {{}} proof let C be set ; ::_thesis: for A being non empty set for f being Function of A,(Funcs ({},C)) for g being Function of A,{} holds rng (f .. g) = {{}} let A be non empty set ; ::_thesis: for f being Function of A,(Funcs ({},C)) for g being Function of A,{} holds rng (f .. g) = {{}} let f be Function of A,(Funcs ({},C)); ::_thesis: for g being Function of A,{} holds rng (f .. g) = {{}} let g be Function of A,{}; ::_thesis: rng (f .. g) = {{}} set a = the Element of A; A1: Funcs ({},C) = {{}} by FUNCT_5:57; then A2: dom f = A by FUNCT_2:def_1; A3: dom (f .. g) = dom f by PRALG_1:def_17; A4: rng (f .. g) c= {{}} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f .. g) or x in {{}} ) A5: rng f c= Funcs ({},C) by RELAT_1:def_19; assume x in rng (f .. g) ; ::_thesis: x in {{}} then consider y being set such that A6: y in dom (f .. g) and A7: (f .. g) . y = x by FUNCT_1:def_3; f . y in rng f by A3, A6, FUNCT_1:def_3; then A8: f . y = {} by A1, A5, TARSKI:def_1; x = (f . y) . (g . y) by A3, A6, A7, PRALG_1:def_17; then x = {} by A8; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; f . the Element of A = {} by A1, TARSKI:def_1; then (f .. g) . the Element of A = {} . (g . the Element of A) by A2, PRALG_1:def_17 .= {} ; then {} in rng (f .. g) by A3, A2, FUNCT_1:def_3; hence rng (f .. g) = {{}} by A4, ZFMISC_1:33; ::_thesis: verum end; theorem Th21: :: HILBERT3:21 for A, B, C being set st ( B = {} implies A = {} ) holds for f being Function of A,(Funcs (B,C)) for g being Function of A,B holds rng (f .. g) c= C proof let A, B, C be set ; ::_thesis: ( ( B = {} implies A = {} ) implies for f being Function of A,(Funcs (B,C)) for g being Function of A,B holds rng (f .. g) c= C ) assume A1: ( B = {} implies A = {} ) ; ::_thesis: for f being Function of A,(Funcs (B,C)) for g being Function of A,B holds rng (f .. g) c= C let f be Function of A,(Funcs (B,C)); ::_thesis: for g being Function of A,B holds rng (f .. g) c= C let g be Function of A,B; ::_thesis: rng (f .. g) c= C let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f .. g) or x in C ) assume x in rng (f .. g) ; ::_thesis: x in C then consider y being set such that A2: y in dom (f .. g) and A3: (f .. g) . y = x by FUNCT_1:def_3; A4: dom (f .. g) = dom f by PRALG_1:def_17; then A5: Funcs (B,C) <> {} by A2; then A6: dom f = A by FUNCT_2:def_1; then reconsider fy = f . y as Function of B,C by A2, A4, A5, FUNCT_2:5, FUNCT_2:66; A7: C <> {} by A1, A2, A6, PRALG_1:def_17; g . y in B by A1, A2, A4, A6, FUNCT_2:5; then fy . (g . y) in C by A7, FUNCT_2:5; hence x in C by A2, A3, A4, PRALG_1:def_17; ::_thesis: verum end; theorem Th22: :: HILBERT3:22 for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds for f being Function of A,(Funcs (B,C)) holds dom (Frege f) = Funcs (A,B) proof let A, B, C be set ; ::_thesis: ( ( not C = {} or B = {} or A = {} ) implies for f being Function of A,(Funcs (B,C)) holds dom (Frege f) = Funcs (A,B) ) assume A1: ( not C = {} or B = {} or A = {} ) ; ::_thesis: for f being Function of A,(Funcs (B,C)) holds dom (Frege f) = Funcs (A,B) let f be Function of A,(Funcs (B,C)); ::_thesis: dom (Frege f) = Funcs (A,B) thus dom (Frege f) = product (doms f) by PARTFUN1:def_2 .= product (A --> B) by A1, Th6 .= Funcs (A,B) by CARD_3:11 ; ::_thesis: verum end; theorem Th23: :: HILBERT3:23 for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds for f being Function of A,(Funcs (B,C)) holds rng (Frege f) c= Funcs (A,C) proof let A, B, C be set ; ::_thesis: ( ( not C = {} or B = {} or A = {} ) implies for f being Function of A,(Funcs (B,C)) holds rng (Frege f) c= Funcs (A,C) ) assume ( not C = {} or B = {} or A = {} ) ; ::_thesis: for f being Function of A,(Funcs (B,C)) holds rng (Frege f) c= Funcs (A,C) then A1: ( Funcs (B,C) = {} implies A = {} ) by FUNCT_2:8; let f be Function of A,(Funcs (B,C)); ::_thesis: rng (Frege f) c= Funcs (A,C) A2: SubFuncs (rng f) = rng f by Th4; then A3: dom (rngs f) = f " (rng f) by FUNCT_6:def_3; then A4: dom (rngs f) = dom f by RELAT_1:134 .= A by A1, FUNCT_2:def_1 ; A5: for x being set st x in dom (rngs f) holds (rngs f) . x c= (A --> C) . x proof let x be set ; ::_thesis: ( x in dom (rngs f) implies (rngs f) . x c= (A --> C) . x ) assume A6: x in dom (rngs f) ; ::_thesis: (rngs f) . x c= (A --> C) . x A7: (rngs f) . x = rng (f . x) by A2, A3, A6, FUNCT_6:def_3; f . x in Funcs (B,C) by A1, A4, A6, FUNCT_2:5; then (rngs f) . x c= C by A7, FUNCT_2:92; hence (rngs f) . x c= (A --> C) . x by A4, A6, FUNCOP_1:7; ::_thesis: verum end; dom (rngs f) = dom (A --> C) by A4, FUNCOP_1:13; then product (rngs f) c= product (A --> C) by A5, CARD_3:27; then product (rngs f) c= Funcs (A,C) by CARD_3:11; hence rng (Frege f) c= Funcs (A,C) by FUNCT_6:38; ::_thesis: verum end; theorem Th24: :: HILBERT3:24 for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds for f being Function of A,(Funcs (B,C)) holds Frege f is Function of (Funcs (A,B)),(Funcs (A,C)) proof let A, B, C be set ; ::_thesis: ( ( not C = {} or B = {} or A = {} ) implies for f being Function of A,(Funcs (B,C)) holds Frege f is Function of (Funcs (A,B)),(Funcs (A,C)) ) assume A1: ( not C = {} or B = {} or A = {} ) ; ::_thesis: for f being Function of A,(Funcs (B,C)) holds Frege f is Function of (Funcs (A,B)),(Funcs (A,C)) then A2: ( Funcs (A,C) = {} implies Funcs (A,B) = {} ) by FUNCT_2:8; let f be Function of A,(Funcs (B,C)); ::_thesis: Frege f is Function of (Funcs (A,B)),(Funcs (A,C)) ( dom (Frege f) = Funcs (A,B) & rng (Frege f) c= Funcs (A,C) ) by A1, Th22, Th23; hence Frege f is Function of (Funcs (A,B)),(Funcs (A,C)) by A2, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; begin registration let A, B be set ; let P be Permutation of A; let Q be Permutation of B; cluster[:P,Q:] -> bijective for Function of [:A,B:],[:A,B:]; coherence for b1 being Function of [:A,B:],[:A,B:] st b1 = [:P,Q:] holds b1 is bijective proof [:P,Q:] is bijective proof thus [:P,Q:] is one-to-one ; :: according to FUNCT_2:def_4 ::_thesis: [:P,Q:] is onto ( rng P = A & rng Q = B ) by FUNCT_2:def_3; hence rng [:P,Q:] = [:A,B:] by FUNCT_3:67; :: according to FUNCT_2:def_3 ::_thesis: verum end; hence for b1 being Function of [:A,B:],[:A,B:] st b1 = [:P,Q:] holds b1 is bijective ; ::_thesis: verum end; end; theorem :: HILBERT3:25 for A, B being set for P being Permutation of A for Q being Permutation of B holds [:P,Q:] is bijective ; definition let A, B be non empty set ; let P be Permutation of A; let Q be Function of B,B; funcP => Q -> Function of (Funcs (A,B)),(Funcs (A,B)) means :Def1: :: HILBERT3:def 1 for f being Function of A,B holds it . f = (Q * f) * (P "); existence ex b1 being Function of (Funcs (A,B)),(Funcs (A,B)) st for f being Function of A,B holds b1 . f = (Q * f) * (P ") proof deffunc H1( Element of Funcs (A,B)) -> Element of bool [:A,B:] = (Q * \$1) * (P "); A1: for f being Element of Funcs (A,B) holds H1(f) in Funcs (A,B) by FUNCT_2:8; consider F being Function of (Funcs (A,B)),(Funcs (A,B)) such that A2: for f being Element of Funcs (A,B) holds F . f = H1(f) from FUNCT_2:sch_8(A1); take F ; ::_thesis: for f being Function of A,B holds F . f = (Q * f) * (P ") let f be Function of A,B; ::_thesis: F . f = (Q * f) * (P ") f in Funcs (A,B) by FUNCT_2:8; hence F . f = (Q * f) * (P ") by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Funcs (A,B)),(Funcs (A,B)) st ( for f being Function of A,B holds b1 . f = (Q * f) * (P ") ) & ( for f being Function of A,B holds b2 . f = (Q * f) * (P ") ) holds b1 = b2 proof let F, G be Function of (Funcs (A,B)),(Funcs (A,B)); ::_thesis: ( ( for f being Function of A,B holds F . f = (Q * f) * (P ") ) & ( for f being Function of A,B holds G . f = (Q * f) * (P ") ) implies F = G ) assume that A3: for f being Function of A,B holds F . f = (Q * f) * (P ") and A4: for f being Function of A,B holds G . f = (Q * f) * (P ") ; ::_thesis: F = G now__::_thesis:_for_f_being_Element_of_Funcs_(A,B)_holds_F_._f_=_G_._f let f be Element of Funcs (A,B); ::_thesis: F . f = G . f thus F . f = (Q * f) * (P ") by A3 .= G . f by A4 ; ::_thesis: verum end; hence F = G by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines => HILBERT3:def_1_:_ for A, B being non empty set for P being Permutation of A for Q being Function of B,B for b5 being Function of (Funcs (A,B)),(Funcs (A,B)) holds ( b5 = P => Q iff for f being Function of A,B holds b5 . f = (Q * f) * (P ") ); registration let A, B be non empty set ; let P be Permutation of A; let Q be Permutation of B; clusterP => Q -> bijective ; coherence P => Q is bijective proof thus P => Q is one-to-one :: according to FUNCT_2:def_4 ::_thesis: P => Q is onto proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (P => Q) or not x2 in dom (P => Q) or not (P => Q) . x1 = (P => Q) . x2 or x1 = x2 ) assume ( x1 in dom (P => Q) & x2 in dom (P => Q) ) ; ::_thesis: ( not (P => Q) . x1 = (P => Q) . x2 or x1 = x2 ) then reconsider f1 = x1, f2 = x2 as Element of Funcs (A,B) by FUNCT_2:def_1; assume (P => Q) . x1 = (P => Q) . x2 ; ::_thesis: x1 = x2 then A1: (Q * f1) * (P ") = (P => Q) . f2 by Def1 .= (Q * f2) * (P ") by Def1 ; A2: Q * f1 = (Q * f1) * (id A) by FUNCT_2:17 .= (Q * f1) * ((P ") * P) by FUNCT_2:61 .= ((Q * f2) * (P ")) * P by A1, RELAT_1:36 .= (Q * f2) * ((P ") * P) by RELAT_1:36 .= (Q * f2) * (id A) by FUNCT_2:61 .= Q * f2 by FUNCT_2:17 ; f1 = (id B) * f1 by FUNCT_2:17 .= ((Q ") * Q) * f1 by FUNCT_2:61 .= (Q ") * (Q * f2) by A2, RELAT_1:36 .= ((Q ") * Q) * f2 by RELAT_1:36 .= (id B) * f2 by FUNCT_2:61 .= f2 by FUNCT_2:17 ; hence x1 = x2 ; ::_thesis: verum end; thus rng (P => Q) c= Funcs (A,B) by RELAT_1:def_19; :: according to FUNCT_2:def_3,XBOOLE_0:def_10 ::_thesis: Funcs (A,B) c= K451((Funcs (A,B)),(P => Q)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (A,B) or x in K451((Funcs (A,B)),(P => Q)) ) assume x in Funcs (A,B) ; ::_thesis: x in K451((Funcs (A,B)),(P => Q)) then x is Element of Funcs (A,B) ; then reconsider f = x as Function of A,B ; dom (P => Q) = Funcs (A,B) by FUNCT_2:def_1; then A3: ((Q ") * f) * P in dom (P => Q) by FUNCT_2:8; (P => Q) . (((Q ") * f) * P) = (Q * (((Q ") * f) * P)) * (P ") by Def1 .= ((Q * ((Q ") * f)) * P) * (P ") by RELAT_1:36 .= (((Q * (Q ")) * f) * P) * (P ") by RELAT_1:36 .= (((id B) * f) * P) * (P ") by FUNCT_2:61 .= (f * P) * (P ") by FUNCT_2:17 .= f * (P * (P ")) by RELAT_1:36 .= f * (id A) by FUNCT_2:61 .= f by FUNCT_2:17 ; hence x in rng (P => Q) by A3, FUNCT_1:def_3; ::_thesis: verum end; end; theorem Th26: :: HILBERT3:26 for A, B being non empty set for P being Permutation of A for Q being Permutation of B for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P proof let A, B be non empty set ; ::_thesis: for P being Permutation of A for Q being Permutation of B for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P let P be Permutation of A; ::_thesis: for Q being Permutation of B for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P let Q be Permutation of B; ::_thesis: for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P let f be Function of A,B; ::_thesis: ((P => Q) ") . f = ((Q ") * f) * P reconsider h = f as Element of Funcs (A,B) by FUNCT_2:8; reconsider g = ((Q ") * f) * P as Function of A,B ; f in Funcs (A,B) by FUNCT_2:8; then A1: (((P => Q) ") ") . (((P => Q) ") . f) = f by FUNCT_2:26 .= f * (id A) by FUNCT_2:17 .= f * (P * (P ")) by FUNCT_2:61 .= (f * P) * (P ") by RELAT_1:36 .= (((id B) * f) * P) * (P ") by FUNCT_2:17 .= (((Q * (Q ")) * f) * P) * (P ") by FUNCT_2:61 .= ((Q * ((Q ") * f)) * P) * (P ") by RELAT_1:36 .= (Q * (((Q ") * f) * P)) * (P ") by RELAT_1:36 .= (P => Q) . g by Def1 .= (((P => Q) ") ") . (((Q ") * f) * P) by FUNCT_1:43 ; ( ((P => Q) ") . h in Funcs (A,B) & g in Funcs (A,B) ) by FUNCT_2:8; hence ((P => Q) ") . f = ((Q ") * f) * P by A1, FUNCT_2:19; ::_thesis: verum end; theorem Th27: :: HILBERT3:27 for A, B being non empty set for P being Permutation of A for Q being Permutation of B holds (P => Q) " = (P ") => (Q ") proof let A, B be non empty set ; ::_thesis: for P being Permutation of A for Q being Permutation of B holds (P => Q) " = (P ") => (Q ") let P be Permutation of A; ::_thesis: for Q being Permutation of B holds (P => Q) " = (P ") => (Q ") let Q be Permutation of B; ::_thesis: (P => Q) " = (P ") => (Q ") now__::_thesis:_for_f_being_Element_of_Funcs_(A,B)_holds_((P_=>_Q)_")_._f_=_((P_")_=>_(Q_"))_._f let f be Element of Funcs (A,B); ::_thesis: ((P => Q) ") . f = ((P ") => (Q ")) . f thus ((P => Q) ") . f = ((Q ") * f) * P by Th26 .= ((Q ") * f) * ((P ") ") by FUNCT_1:43 .= ((P ") => (Q ")) . f by Def1 ; ::_thesis: verum end; hence (P => Q) " = (P ") => (Q ") by FUNCT_2:63; ::_thesis: verum end; theorem Th28: :: HILBERT3:28 for A, B, C being non empty set for f being Function of A,(Funcs (B,C)) for g being Function of A,B for P being Permutation of B for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g) proof let A, B, C be non empty set ; ::_thesis: for f being Function of A,(Funcs (B,C)) for g being Function of A,B for P being Permutation of B for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g) let f be Function of A,(Funcs (B,C)); ::_thesis: for g being Function of A,B for P being Permutation of B for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g) let g be Function of A,B; ::_thesis: for P being Permutation of B for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g) let P be Permutation of B; ::_thesis: for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g) let Q be Permutation of C; ::_thesis: ((P => Q) * f) .. (P * g) = Q * (f .. g) A1: dom ((P => Q) * f) = A by FUNCT_2:def_1; A2: ( dom Q = C & rng (f .. g) c= C ) by Th21, FUNCT_2:def_1; A3: dom f = A by FUNCT_2:def_1; then dom (f .. g) = A by PRALG_1:def_17; then A4: dom (Q * (f .. g)) = A by A2, RELAT_1:27; for x being set st x in dom ((P => Q) * f) holds (Q * (f .. g)) . x = (((P => Q) * f) . x) . ((P * g) . x) proof let x be set ; ::_thesis: ( x in dom ((P => Q) * f) implies (Q * (f .. g)) . x = (((P => Q) * f) . x) . ((P * g) . x) ) assume A5: x in dom ((P => Q) * f) ; ::_thesis: (Q * (f .. g)) . x = (((P => Q) * f) . x) . ((P * g) . x) reconsider fx = f . x as Function of B,C by A1, A5, FUNCT_2:5, FUNCT_2:66; g . x in B by A1, A5, FUNCT_2:5; then A6: g . x in dom fx by FUNCT_2:def_1; (P * g) . x in B by A1, A5, FUNCT_2:5; then A7: (P * g) . x in dom (P ") by FUNCT_2:def_1; thus (Q * (f .. g)) . x = Q . ((f .. g) . x) by A4, A1, A5, FUNCT_1:12 .= Q . (fx . (g . x)) by A3, A1, A5, PRALG_1:def_17 .= (Q * fx) . (g . x) by A6, FUNCT_1:13 .= (Q * fx) . (((id B) * g) . x) by FUNCT_2:17 .= (Q * fx) . ((((P ") * P) * g) . x) by FUNCT_2:61 .= (Q * fx) . (((P ") * (P * g)) . x) by RELAT_1:36 .= (Q * fx) . ((P ") . ((P * g) . x)) by A1, A5, FUNCT_2:15 .= ((Q * fx) * (P ")) . ((P * g) . x) by A7, FUNCT_1:13 .= ((P => Q) . fx) . ((P * g) . x) by Def1 .= (((P => Q) * f) . x) . ((P * g) . x) by A1, A5, FUNCT_2:15 ; ::_thesis: verum end; hence ((P => Q) * f) .. (P * g) = Q * (f .. g) by A4, A1, PRALG_1:def_17; ::_thesis: verum end; begin definition mode SetValuation is V19() ManySortedSet of NAT ; end; definition let V be SetValuation; func SetVal V -> ManySortedSet of HP-WFF means :Def2: :: HILBERT3:def 2 ( it . VERUM = 1 & ( for n being Element of NAT holds it . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds ( it . (p '&' q) = [:(it . p),(it . q):] & it . (p => q) = Funcs ((it . p),(it . q)) ) ) ); existence ex b1 being ManySortedSet of HP-WFF st ( b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds ( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) ) proof deffunc H1( Element of NAT ) -> set = V . \$1; consider M being ManySortedSet of HP-WFF such that A1: ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = H1(n) ) & ( for p, q being Element of HP-WFF holds ( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) ) from HILBERT2:sch_4(); take M ; ::_thesis: ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds ( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) ) thus ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds ( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds ( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) & b2 . VERUM = 1 & ( for n being Element of NAT holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds ( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs ((b2 . p),(b2 . q)) ) ) holds b1 = b2 proof let M1, M2 be ManySortedSet of HP-WFF ; ::_thesis: ( M1 . VERUM = 1 & ( for n being Element of NAT holds M1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds ( M1 . (p '&' q) = [:(M1 . p),(M1 . q):] & M1 . (p => q) = Funcs ((M1 . p),(M1 . q)) ) ) & M2 . VERUM = 1 & ( for n being Element of NAT holds M2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds ( M2 . (p '&' q) = [:(M2 . p),(M2 . q):] & M2 . (p => q) = Funcs ((M2 . p),(M2 . q)) ) ) implies M1 = M2 ) assume that A2: M1 . VERUM = 1 and A3: for n being Element of NAT holds M1 . (prop n) = V . n and A4: for p, q being Element of HP-WFF holds ( M1 . (p '&' q) = [:(M1 . p),(M1 . q):] & M1 . (p => q) = Funcs ((M1 . p),(M1 . q)) ) and A5: M2 . VERUM = 1 and A6: for n being Element of NAT holds M2 . (prop n) = V . n and A7: for p, q being Element of HP-WFF holds ( M2 . (p '&' q) = [:(M2 . p),(M2 . q):] & M2 . (p => q) = Funcs ((M2 . p),(M2 . q)) ) ; ::_thesis: M1 = M2 defpred S1[ Element of HP-WFF ] means M1 . \$1 = M2 . \$1; A8: 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 A9: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; ::_thesis: ( S1[r '&' s] & S1[r => s] ) thus M1 . (r '&' s) = [:(M2 . r),(M2 . s):] by A4, A9 .= M2 . (r '&' s) by A7 ; ::_thesis: S1[r => s] thus M1 . (r => s) = Funcs ((M2 . r),(M2 . s)) by A4, A9 .= M2 . (r => s) by A7 ; ::_thesis: verum end; A10: 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) = V . n by A3 .= M2 . (prop n) by A6 ; ::_thesis: verum end; A11: S1[ VERUM ] by A2, A5; for r being Element of HP-WFF holds S1[r] from HILBERT2:sch_2(A11, A10, A8); 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 Def2 defines SetVal HILBERT3:def_2_:_ for V being SetValuation for b2 being ManySortedSet of HP-WFF holds ( b2 = SetVal V iff ( b2 . VERUM = 1 & ( for n being Element of NAT holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds ( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs ((b2 . p),(b2 . q)) ) ) ) ); definition let V be SetValuation; let p be Element of HP-WFF ; func SetVal (V,p) -> set equals :: HILBERT3:def 3 (SetVal V) . p; correctness coherence (SetVal V) . p is set ; ; end; :: deftheorem defines SetVal HILBERT3:def_3_:_ for V being SetValuation for p being Element of HP-WFF holds SetVal (V,p) = (SetVal V) . p; registration let V be SetValuation; let p be Element of HP-WFF ; cluster SetVal (V,p) -> non empty ; coherence not SetVal (V,p) is empty proof defpred S1[ Element of HP-WFF ] means not (SetVal V) . V is empty ; A1: for n being Element of NAT holds S1[ prop n] proof let n be Element of NAT ; ::_thesis: S1[ prop n] (SetVal V) . (prop n) = V . n by Def2; 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] ) ) assume that A3: not (SetVal V) . r is empty and A4: not (SetVal V) . s is empty ; ::_thesis: ( S1[r '&' s] & S1[r => s] ) (SetVal V) . (r '&' s) = [:((SetVal V) . r),((SetVal V) . s):] by Def2; hence not (SetVal V) . (r '&' s) is empty by A3, A4; ::_thesis: S1[r => s] (SetVal V) . (r => s) = Funcs (((SetVal V) . r),((SetVal V) . s)) by Def2; hence S1[r => s] by A4; ::_thesis: verum end; A5: S1[ VERUM ] by Def2; for r being Element of HP-WFF holds S1[r] from HILBERT2:sch_2(A5, A1, A2); hence not SetVal (V,p) is empty ; ::_thesis: verum end; end; theorem :: HILBERT3:29 for V being SetValuation holds SetVal (V,VERUM) = 1 by Def2; theorem :: HILBERT3:30 for n being Element of NAT for V being SetValuation holds SetVal (V,(prop n)) = V . n by Def2; theorem :: HILBERT3:31 for p, q being Element of HP-WFF for V being SetValuation holds SetVal (V,(p '&' q)) = [:(SetVal (V,p)),(SetVal (V,q)):] by Def2; theorem :: HILBERT3:32 for p, q being Element of HP-WFF for V being SetValuation holds SetVal (V,(p => q)) = Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2; registration let V be SetValuation; let p, q be Element of HP-WFF ; cluster SetVal (V,(p => q)) -> functional ; coherence SetVal (V,(p => q)) is functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in SetVal (V,(p => q)) or x is set ) assume x in SetVal (V,(p => q)) ; ::_thesis: x is set then x in Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2; hence x is set ; ::_thesis: verum end; end; registration let V be SetValuation; let p, q, r be Element of HP-WFF ; cluster -> Function-yielding for Element of SetVal (V,(p => (q => r))); coherence for b1 being Element of SetVal (V,(p => (q => r))) holds b1 is Function-yielding proof let e be Element of SetVal (V,(p => (q => r))); ::_thesis: e is Function-yielding let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom e or e . x is set ) assume x in dom e ; ::_thesis: e . x is set e in SetVal (V,(p => (q => r))) ; then e in Funcs ((SetVal (V,p)),(SetVal (V,(q => r)))) by Def2; then e is Function of (SetVal (V,p)),(SetVal (V,(q => r))) by FUNCT_2:66; hence e . x is set ; ::_thesis: verum end; end; registration let V be SetValuation; let p, q, r be Element of HP-WFF ; cluster non empty Relation-like SetVal (V,(p => q)) -defined SetVal (V,(p => r)) -valued Function-like total quasi_total Function-yielding V55() for Element of bool [:(SetVal (V,(p => q))),(SetVal (V,(p => r))):]; existence ex b1 being Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))) st b1 is Function-yielding proof set e = the Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))); the Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))) is Function-yielding ; hence ex b1 being Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))) st b1 is Function-yielding ; ::_thesis: verum end; cluster Relation-like Function-like Function-yielding V55() for Element of SetVal (V,(p => (q => r))); existence ex b1 being Element of SetVal (V,(p => (q => r))) st b1 is Function-yielding proof set e = the Element of SetVal (V,(p => (q => r))); the Element of SetVal (V,(p => (q => r))) is Function-yielding ; hence ex b1 being Element of SetVal (V,(p => (q => r))) st b1 is Function-yielding ; ::_thesis: verum end; end; begin definition let V be SetValuation; mode Permutation of V -> Function means :Def4: :: HILBERT3:def 4 ( dom it = NAT & ( for n being Element of NAT holds it . n is Permutation of (V . n) ) ); existence ex b1 being Function st ( dom b1 = NAT & ( for n being Element of NAT holds b1 . n is Permutation of (V . n) ) ) proof take id V ; ::_thesis: ( dom (id V) = NAT & ( for n being Element of NAT holds (id V) . n is Permutation of (V . n) ) ) thus dom (id V) = NAT by PARTFUN1:def_2; ::_thesis: for n being Element of NAT holds (id V) . n is Permutation of (V . n) let n be Element of NAT ; ::_thesis: (id V) . n is Permutation of (V . n) (id V) . n = id (V . n) by MSUALG_3:def_1; hence (id V) . n is Permutation of (V . n) ; ::_thesis: verum end; end; :: deftheorem Def4 defines Permutation HILBERT3:def_4_:_ for V being SetValuation for b2 being Function holds ( b2 is Permutation of V iff ( dom b2 = NAT & ( for n being Element of NAT holds b2 . n is Permutation of (V . n) ) ) ); definition let V be SetValuation; let P be Permutation of V; func Perm P -> ManySortedFunction of SetVal V, SetVal V means :Def5: :: HILBERT3:def 5 ( it . VERUM = id 1 & ( for n being Element of NAT holds it . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = it . p & q9 = it . q & it . (p '&' q) = [:p9,q9:] & it . (p => q) = p9 => q9 ) ) ); existence ex b1 being ManySortedFunction of SetVal V, SetVal V st ( b1 . VERUM = id 1 & ( for n being Element of NAT holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = [:p9,q9:] & b1 . (p => q) = p9 => q9 ) ) ) proof deffunc H1( Element of NAT ) -> set = P . \$1; defpred S1[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( \$3 is Permutation of (SetVal (V,\$1)) & \$4 is Permutation of (SetVal (V,\$2)) implies ex p9 being Permutation of (SetVal (V,\$1)) ex q9 being Permutation of (SetVal (V,\$2)) st ( p9 = \$3 & q9 = \$4 & \$5 = p9 => q9 ) ) & ( ( not \$3 is Permutation of (SetVal (V,\$1)) or not \$4 is Permutation of (SetVal (V,\$2)) ) implies \$5 = {} ) ); defpred S2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( \$3 is Permutation of (SetVal (V,\$1)) & \$4 is Permutation of (SetVal (V,\$2)) implies ex p9 being Permutation of (SetVal (V,\$1)) ex q9 being Permutation of (SetVal (V,\$2)) st ( p9 = \$3 & q9 = \$4 & \$5 = [:p9,q9:] ) ) & ( ( not \$3 is Permutation of (SetVal (V,\$1)) or not \$4 is Permutation of (SetVal (V,\$2)) ) 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 Permutation of (SetVal (V,p)) & b is Permutation of (SetVal (V,q)) ) or not a is Permutation of (SetVal (V,p)) or not b is Permutation of (SetVal (V,q)) ) ; supposethat A2: a is Permutation of (SetVal (V,p)) and A3: b is Permutation of (SetVal (V,q)) ; ::_thesis: ex c being set st S2[p,q,a,b,c] reconsider q9 = b as Permutation of (SetVal (V,q)) by A3; reconsider p9 = a as Permutation of (SetVal (V,p)) by A2; take [:p9,q9:] ; ::_thesis: S2[p,q,a,b,[:p9,q9:]] thus S2[p,q,a,b,[:p9,q9:]] ; ::_thesis: verum end; suppose ( not a is Permutation of (SetVal (V,p)) or not b is Permutation of (SetVal (V,q)) ) ; ::_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 Permutation of (SetVal (V,p)) & b is Permutation of (SetVal (V,q)) ) or not a is Permutation of (SetVal (V,p)) or not b is Permutation of (SetVal (V,q)) ) ; supposethat A5: a is Permutation of (SetVal (V,p)) and A6: b is Permutation of (SetVal (V,q)) ; ::_thesis: ex d being set st S1[p,q,a,b,d] reconsider q9 = b as Permutation of (SetVal (V,q)) by A6; reconsider p9 = a as Permutation of (SetVal (V,p)) by A5; take p9 => q9 ; ::_thesis: S1[p,q,a,b,p9 => q9] thus S1[p,q,a,b,p9 => q9] ; ::_thesis: verum end; suppose ( not a is Permutation of (SetVal (V,p)) or not b is Permutation of (SetVal (V,q)) ) ; ::_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 = id 1 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); defpred S3[ Element of HP-WFF ] means M . \$1 is Permutation of ((SetVal V) . \$1); A12: 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 A13: ( M . r is Permutation of ((SetVal V) . r) & M . s is Permutation of ((SetVal V) . s) ) ; ::_thesis: ( S3[r '&' s] & S3[r => s] ) A14: (SetVal V) . (r '&' s) = [:(SetVal (V,r)),(SetVal (V,s)):] by Def2; ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st ( p9 = M . r & q9 = M . s & M . (r '&' s) = [:p9,q9:] ) by A11, A13; hence M . (r '&' s) is Permutation of ((SetVal V) . (r '&' s)) by A14; ::_thesis: S3[r => s] A15: (SetVal V) . (r => s) = Funcs ((SetVal (V,r)),(SetVal (V,s))) by Def2; ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st ( p9 = M . r & q9 = M . s & M . (r => s) = p9 => q9 ) by A11, A13; hence S3[r => s] by A15; ::_thesis: verum end; take M ; ::_thesis: ( M is ManySortedFunction of SetVal V, SetVal V & M . VERUM = id 1 & ( for n being Element of NAT holds M . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) ) ) A16: for n being Element of NAT holds S3[ prop n] proof let n be Element of NAT ; ::_thesis: S3[ prop n] ( M . (prop n) = P . n & (SetVal V) . (prop n) = V . n ) by A10, Def2; hence S3[ prop n] by Def4; ::_thesis: verum end; (SetVal V) . VERUM = 1 by Def2; then A17: S3[ VERUM ] by A9; A18: for p being Element of HP-WFF holds S3[p] from HILBERT2:sch_2(A17, A16, A12); thus M is ManySortedFunction of SetVal V, SetVal V ::_thesis: ( M . VERUM = id 1 & ( for n being Element of NAT holds M . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) ) ) proof let p be set ; :: according to PBOOLE:def_15 ::_thesis: ( not p in HP-WFF or M . p is Element of bool [:((SetVal V) . p),((SetVal V) . p):] ) thus ( not p in HP-WFF or M . p is Element of bool [:((SetVal V) . p),((SetVal V) . p):] ) by A18; ::_thesis: verum end; thus M . VERUM = id 1 by A9; ::_thesis: ( ( for n being Element of NAT holds M . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) ) ) thus for n being Element of NAT holds M . (prop n) = P . n by A10; ::_thesis: for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) let p, q be Element of HP-WFF ; ::_thesis: ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) A19: ( M . p is Permutation of ((SetVal V) . p) & M . q is Permutation of ((SetVal V) . q) ) by A18; then consider p9 being Permutation of (SetVal (V,p)), q9 being Permutation of (SetVal (V,q)) such that A20: ( p9 = M . p & q9 = M . q ) and A21: M . (p '&' q) = [:p9,q9:] by A11; take p9 ; ::_thesis: ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) take q9 ; ::_thesis: ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) thus ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] ) by A20, A21; ::_thesis: M . (p => q) = p9 => q9 ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M . p & q9 = M . q & M . (p => q) = p9 => q9 ) by A11, A19; hence M . (p => q) = p9 => q9 by A20; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of SetVal V, SetVal V st b1 . VERUM = id 1 & ( for n being Element of NAT holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = [:p9,q9:] & b1 . (p => q) = p9 => q9 ) ) & b2 . VERUM = id 1 & ( for n being Element of NAT holds b2 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = b2 . p & q9 = b2 . q & b2 . (p '&' q) = [:p9,q9:] & b2 . (p => q) = p9 => q9 ) ) holds b1 = b2 proof let M1, M2 be ManySortedFunction of SetVal V, SetVal V; ::_thesis: ( M1 . VERUM = id 1 & ( for n being Element of NAT holds M1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = [:p9,q9:] & M1 . (p => q) = p9 => q9 ) ) & M2 . VERUM = id 1 & ( for n being Element of NAT holds M2 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = [:p9,q9:] & M2 . (p => q) = p9 => q9 ) ) implies M1 = M2 ) assume that A22: M1 . VERUM = id 1 and A23: for n being Element of NAT holds M1 . (prop n) = P . n and A24: for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M1 . p & q9 = M1 . q & M1 . (p '&' q) = [:p9,q9:] & M1 . (p => q) = p9 => q9 ) and A25: M2 . VERUM = id 1 and A26: for n being Element of NAT holds M2 . (prop n) = P . n and A27: for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = M2 . p & q9 = M2 . q & M2 . (p '&' q) = [:p9,q9:] & M2 . (p => q) = p9 => q9 ) ; ::_thesis: M1 = M2 defpred S1[ Element of HP-WFF ] means M1 . \$1 = M2 . \$1; A28: 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) = P . n by A23 .= M2 . (prop n) by A26 ; ::_thesis: verum end; A29: 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 A30: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; ::_thesis: ( S1[r '&' s] & S1[r => s] ) A31: ( ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st ( p9 = M1 . r & q9 = M1 . s & M1 . (r '&' s) = [:p9,q9:] & M1 . (r => s) = p9 => q9 ) & ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st ( p9 = M2 . r & q9 = M2 . s & M2 . (r '&' s) = [:p9,q9:] & M2 . (r => s) = p9 => q9 ) ) by A24, A27; hence M1 . (r '&' s) = M2 . (r '&' s) by A30; ::_thesis: S1[r => s] thus S1[r => s] by A30, A31; ::_thesis: verum end; A32: S1[ VERUM ] by A22, A25; for r being Element of HP-WFF holds S1[r] from HILBERT2:sch_2(A32, A28, A29); 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 Def5 defines Perm HILBERT3:def_5_:_ for V being SetValuation for P being Permutation of V for b3 being ManySortedFunction of SetVal V, SetVal V holds ( b3 = Perm P iff ( b3 . VERUM = id 1 & ( for n being Element of NAT holds b3 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = b3 . p & q9 = b3 . q & b3 . (p '&' q) = [:p9,q9:] & b3 . (p => q) = p9 => q9 ) ) ) ); definition let V be SetValuation; let P be Permutation of V; let p be Element of HP-WFF ; func Perm (P,p) -> Function of (SetVal (V,p)),(SetVal (V,p)) equals :: HILBERT3:def 6 (Perm P) . p; correctness coherence (Perm P) . p is Function of (SetVal (V,p)),(SetVal (V,p)); ; end; :: deftheorem defines Perm HILBERT3:def_6_:_ for V being SetValuation for P being Permutation of V for p being Element of HP-WFF holds Perm (P,p) = (Perm P) . p; theorem Th33: :: HILBERT3:33 for V being SetValuation for P being Permutation of V holds Perm (P,VERUM) = id (SetVal (V,VERUM)) proof let V be SetValuation; ::_thesis: for P being Permutation of V holds Perm (P,VERUM) = id (SetVal (V,VERUM)) let P be Permutation of V; ::_thesis: Perm (P,VERUM) = id (SetVal (V,VERUM)) thus Perm (P,VERUM) = id 1 by Def5 .= id (SetVal (V,VERUM)) by Def2 ; ::_thesis: verum end; theorem :: HILBERT3:34 for n being Element of NAT for V being SetValuation for P being Permutation of V holds Perm (P,(prop n)) = P . n by Def5; theorem Th35: :: HILBERT3:35 for p, q being Element of HP-WFF for V being SetValuation for P being Permutation of V holds Perm (P,(p '&' q)) = [:(Perm (P,p)),(Perm (P,q)):] proof let p, q be Element of HP-WFF ; ::_thesis: for V being SetValuation for P being Permutation of V holds Perm (P,(p '&' q)) = [:(Perm (P,p)),(Perm (P,q)):] let V be SetValuation; ::_thesis: for P being Permutation of V holds Perm (P,(p '&' q)) = [:(Perm (P,p)),(Perm (P,q)):] let P be Permutation of V; ::_thesis: Perm (P,(p '&' q)) = [:(Perm (P,p)),(Perm (P,q)):] ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = (Perm P) . p & q9 = (Perm P) . q & (Perm P) . (p '&' q) = [:p9,q9:] & (Perm P) . (p => q) = p9 => q9 ) by Def5; hence Perm (P,(p '&' q)) = [:(Perm (P,p)),(Perm (P,q)):] ; ::_thesis: verum end; theorem Th36: :: HILBERT3:36 for p, q being Element of HP-WFF for V being SetValuation for P being Permutation of V for p9 being Permutation of (SetVal (V,p)) for q9 being Permutation of (SetVal (V,q)) st p9 = Perm (P,p) & q9 = Perm (P,q) holds Perm (P,(p => q)) = p9 => q9 proof let p, q be Element of HP-WFF ; ::_thesis: for V being SetValuation for P being Permutation of V for p9 being Permutation of (SetVal (V,p)) for q9 being Permutation of (SetVal (V,q)) st p9 = Perm (P,p) & q9 = Perm (P,q) holds Perm (P,(p => q)) = p9 => q9 let V be SetValuation; ::_thesis: for P being Permutation of V for p9 being Permutation of (SetVal (V,p)) for q9 being Permutation of (SetVal (V,q)) st p9 = Perm (P,p) & q9 = Perm (P,q) holds Perm (P,(p => q)) = p9 => q9 let P be Permutation of V; ::_thesis: for p9 being Permutation of (SetVal (V,p)) for q9 being Permutation of (SetVal (V,q)) st p9 = Perm (P,p) & q9 = Perm (P,q) holds Perm (P,(p => q)) = p9 => q9 A1: ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st ( p9 = (Perm P) . p & q9 = (Perm P) . q & (Perm P) . (p '&' q) = [:p9,q9:] & (Perm P) . (p => q) = p9 => q9 ) by Def5; let p9 be Permutation of (SetVal (V,p)); ::_thesis: for q9 being Permutation of (SetVal (V,q)) st p9 = Perm (P,p) & q9 = Perm (P,q) holds Perm (P,(p => q)) = p9 => q9 let q9 be Permutation of (SetVal (V,q)); ::_thesis: ( p9 = Perm (P,p) & q9 = Perm (P,q) implies Perm (P,(p => q)) = p9 => q9 ) assume ( p9 = Perm (P,p) & q9 = Perm (P,q) ) ; ::_thesis: Perm (P,(p => q)) = p9 => q9 hence Perm (P,(p => q)) = p9 => q9 by A1; ::_thesis: verum end; registration let V be SetValuation; let P be Permutation of V; let p be Element of HP-WFF ; cluster Perm (P,p) -> bijective ; coherence Perm (P,p) is bijective proof defpred S1[ Element of HP-WFF ] means Perm (P,V) is bijective ; A1: for n being Element of NAT holds S1[ prop n] proof let n be Element of NAT ; ::_thesis: S1[ prop n] ( SetVal (V,(prop n)) = V . n & Perm (P,(prop n)) = P . n ) by Def2, Def5; hence S1[ prop n] by Def4; ::_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] ) ) assume Perm (P,r) is bijective ; ::_thesis: ( not S1[s] or ( S1[r '&' s] & S1[r => s] ) ) then reconsider r9 = Perm (P,r) as Permutation of (SetVal (V,r)) ; assume Perm (P,s) is bijective ; ::_thesis: ( S1[r '&' s] & S1[r => s] ) then reconsider s9 = Perm (P,s) as Permutation of (SetVal (V,s)) ; ( SetVal (V,(r '&' s)) = [:(SetVal (V,r)),(SetVal (V,s)):] & Perm (P,(r '&' s)) = [:r9,s9:] ) by Def2, Th35; hence Perm (P,(r '&' s)) is bijective ; ::_thesis: S1[r => s] ( SetVal (V,(r => s)) = Funcs ((SetVal (V,r)),(SetVal (V,s))) & Perm (P,(r => s)) = r9 => s9 ) by Def2, Th36; hence S1[r => s] ; ::_thesis: verum end; Perm (P,VERUM) = id (SetVal (V,VERUM)) by Th33; then A3: S1[ VERUM ] ; for p being Element of HP-WFF holds S1[p] from HILBERT2:sch_2(A3, A1, A2); hence Perm (P,p) is bijective ; ::_thesis: verum end; end; theorem Th37: :: HILBERT3:37 for p, q being Element of HP-WFF for V being SetValuation for P being Permutation of V for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds (Perm (P,(p => q))) . g = ((Perm (P,q)) * g) * ((Perm (P,p)) ") proof let p, q be Element of HP-WFF ; ::_thesis: for V being SetValuation for P being Permutation of V for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds (Perm (P,(p => q))) . g = ((Perm (P,q)) * g) * ((Perm (P,p)) ") let V be SetValuation; ::_thesis: for P being Permutation of V for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds (Perm (P,(p => q))) . g = ((Perm (P,q)) * g) * ((Perm (P,p)) ") let P be Permutation of V; ::_thesis: for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds (Perm (P,(p => q))) . g = ((Perm (P,q)) * g) * ((Perm (P,p)) ") let g be Function of (SetVal (V,p)),(SetVal (V,q)); ::_thesis: (Perm (P,(p => q))) . g = ((Perm (P,q)) * g) * ((Perm (P,p)) ") thus (Perm (P,(p => q))) . g = ((Perm (P,p)) => (Perm (P,q))) . g by Th36 .= ((Perm (P,q)) * g) * ((Perm (P,p)) ") by Def1 ; ::_thesis: verum end; theorem Th38: :: HILBERT3:38 for p, q being Element of HP-WFF for V being SetValuation for P being Permutation of V for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds ((Perm (P,(p => q))) ") . g = (((Perm (P,q)) ") * g) * (Perm (P,p)) proof let p, q be Element of HP-WFF ; ::_thesis: for V being SetValuation for P being Permutation of V for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds ((Perm (P,(p => q))) ") . g = (((Perm (P,q)) ") * g) * (Perm (P,p)) let V be SetValuation; ::_thesis: for P being Permutation of V for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds ((Perm (P,(p => q))) ") . g = (((Perm (P,q)) ") * g) * (Perm (P,p)) let P be Permutation of V; ::_thesis: for g being Function of (SetVal (V,p)),(SetVal (V,q)) holds ((Perm (P,(p => q))) ") . g = (((Perm (P,q)) ") * g) * (Perm (P,p)) let g be Function of (SetVal (V,p)),(SetVal (V,q)); ::_thesis: ((Perm (P,(p => q))) ") . g = (((Perm (P,q)) ") * g) * (Perm (P,p)) thus ((Perm (P,(p => q))) ") . g = (((Perm (P,p)) => (Perm (P,q))) ") . g by Th36 .= (((Perm (P,q)) ") * g) * (Perm (P,p)) by Th26 ; ::_thesis: verum end; theorem Th39: :: HILBERT3:39 for p, q being Element of HP-WFF for V being SetValuation for P being Permutation of V for f, g being Function of (SetVal (V,p)),(SetVal (V,q)) st f = (Perm (P,(p => q))) . g holds (Perm (P,q)) * g = f * (Perm (P,p)) proof let p, q be Element of HP-WFF ; ::_thesis: for V being SetValuation for P being Permutation of V for f, g being Function of (SetVal (V,p)),(SetVal (V,q)) st f = (Perm (P,(p => q))) . g holds (Perm (P,q)) * g = f * (Perm (P,p)) let V be SetValuation; ::_thesis: for P being Permutation of V for f, g being Function of (SetVal (V,p)),(SetVal (V,q)) st f = (Perm (P,(p => q))) . g holds (Perm (P,q)) * g = f * (Perm (P,p)) let P be Permutation of V; ::_thesis: for f, g being Function of (SetVal (V,p)),(SetVal (V,q)) st f = (Perm (P,(p => q))) . g holds (Perm (P,q)) * g = f * (Perm (P,p)) let f, g be Function of (SetVal (V,p)),(SetVal (V,q)); ::_thesis: ( f = (Perm (P,(p => q))) . g implies (Perm (P,q)) * g = f * (Perm (P,p)) ) assume A1: f = (Perm (P,(p => q))) . g ; ::_thesis: (Perm (P,q)) * g = f * (Perm (P,p)) thus (Perm (P,q)) * g = ((Perm (P,q)) * g) * (id (SetVal (V,p))) by FUNCT_2:17 .= ((Perm (P,q)) * g) * (((Perm (P,p)) ") * (Perm (P,p))) by FUNCT_2:61 .= (((Perm (P,q)) * g) * ((Perm (P,p)) ")) * (Perm (P,p)) by RELAT_1:36 .= f * (Perm (P,p)) by A1, Th37 ; ::_thesis: verum end; theorem Th40: :: HILBERT3:40 for p, q being Element of HP-WFF for V being SetValuation for P being Permutation of V for x being set st x is_a_fixpoint_of Perm (P,p) holds for f being Function st f is_a_fixpoint_of Perm (P,(p => q)) holds f . x is_a_fixpoint_of Perm (P,q) proof let p, q be Element of HP-WFF ; ::_thesis: for V being SetValuation for P being Permutation of V for x being set st x is_a_fixpoint_of Perm (P,p) holds for f being Function st f is_a_fixpoint_of Perm (P,(p => q)) holds f . x is_a_fixpoint_of Perm (P,q) let V be SetValuation; ::_thesis: for P being Permutation of V for x being set st x is_a_fixpoint_of Perm (P,p) holds for f being Function st f is_a_fixpoint_of Perm (P,(p => q)) holds f . x is_a_fixpoint_of Perm (P,q) let P be Permutation of V; ::_thesis: for x being set st x is_a_fixpoint_of Perm (P,p) holds for f being Function st f is_a_fixpoint_of Perm (P,(p => q)) holds f . x is_a_fixpoint_of Perm (P,q) let x be set ; ::_thesis: ( x is_a_fixpoint_of Perm (P,p) implies for f being Function st f is_a_fixpoint_of Perm (P,(p => q)) holds f . x is_a_fixpoint_of Perm (P,q) ) assume A1: x is_a_fixpoint_of Perm (P,p) ; ::_thesis: for f being Function st f is_a_fixpoint_of Perm (P,(p => q)) holds f . x is_a_fixpoint_of Perm (P,q) let f be Function; ::_thesis: ( f is_a_fixpoint_of Perm (P,(p => q)) implies f . x is_a_fixpoint_of Perm (P,q) ) assume A2: f is_a_fixpoint_of Perm (P,(p => q)) ; ::_thesis: f . x is_a_fixpoint_of Perm (P,q) dom (Perm (P,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:52 .= Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2 ; then f in Funcs ((SetVal (V,p)),(SetVal (V,q))) by A2, ABIAN:def_3; then reconsider g = f as Function of (SetVal (V,p)),(SetVal (V,q)) by FUNCT_2:66; set h = (Perm (P,(p => q))) . f; (Perm (P,(p => q))) . f = ((Perm (P,q)) * g) * ((Perm (P,p)) ") by Th37; then reconsider h = (Perm (P,(p => q))) . f as Function of (SetVal (V,p)),(SetVal (V,q)) ; A3: h = f by A2, ABIAN:def_3; dom (Perm (P,p)) = SetVal (V,p) by FUNCT_2:52; then A4: x in SetVal (V,p) by A1, ABIAN:def_3; dom (Perm (P,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:52 .= Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2 ; then f in Funcs ((SetVal (V,p)),(SetVal (V,q))) by A2, ABIAN:def_3; then f . x in SetVal (V,q) by A4, Th5; hence f . x in dom (Perm (P,q)) by FUNCT_2:52; :: according to ABIAN:def_3 ::_thesis: f . x = (Perm (P,q)) . (f . x) thus (Perm (P,q)) . (f . x) = ((Perm (P,q)) * g) . x by A4, FUNCT_2:15 .= (f * (Perm (P,p))) . x by A3, Th39 .= f . ((Perm (P,p)) . x) by A4, FUNCT_2:15 .= f . x by A1, ABIAN:def_3 ; ::_thesis: verum end; begin definition let p be Element of HP-WFF ; attrp is canonical means :Def7: :: HILBERT3:def 7 for V being SetValuation ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p); end; :: deftheorem Def7 defines canonical HILBERT3:def_7_:_ for p being Element of HP-WFF holds ( p is canonical iff for V being SetValuation ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p) ); registration cluster VERUM -> canonical ; coherence VERUM is canonical proof let V be SetValuation; :: according to HILBERT3:def_7 ::_thesis: ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm (P,VERUM) take 0 ; ::_thesis: for P being Permutation of V holds 0 is_a_fixpoint_of Perm (P,VERUM) let P be Permutation of V; ::_thesis: 0 is_a_fixpoint_of Perm (P,VERUM) ( SetVal (V,VERUM) = 1 & 0 in 1 ) by Def2, CARD_1:49, TARSKI:def_1; hence 0 is_a_fixpoint_of Perm (P,VERUM) by Th3, CARD_1:49; ::_thesis: verum end; end; registration let p, q be Element of HP-WFF ; clusterp => (q => p) -> canonical ; coherence p => (q => p) is canonical proof let V be SetValuation; :: according to HILBERT3:def_7 ::_thesis: ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm (P,(p => (q => p))) deffunc H1( set ) -> Element of bool [:(SetVal (V,q)),{p}:] = (SetVal (V,q)) --> p; A1: for x being Element of SetVal (V,p) holds H1(x) in SetVal (V,(q => p)) proof let x be Element of SetVal (V,p); ::_thesis: H1(x) in SetVal (V,(q => p)) (SetVal (V,q)) --> x in Funcs ((SetVal (V,q)),(SetVal (V,p))) by FUNCT_2:8; hence H1(x) in SetVal (V,(q => p)) by Def2; ::_thesis: verum end; consider f being Function of (SetVal (V,p)),(SetVal (V,(q => p))) such that A2: for x being Element of SetVal (V,p) holds f . x = H1(x) from FUNCT_2:sch_8(A1); take f ; ::_thesis: for P being Permutation of V holds f is_a_fixpoint_of Perm (P,(p => (q => p))) let P be Permutation of V; ::_thesis: f is_a_fixpoint_of Perm (P,(p => (q => p))) f in Funcs ((SetVal (V,p)),(SetVal (V,(q => p)))) by FUNCT_2:8; then f in SetVal (V,(p => (q => p))) by Def2; hence f in dom (Perm (P,(p => (q => p)))) by FUNCT_2:def_1; :: according to ABIAN:def_3 ::_thesis: f = (Perm (P,(p => (q => p)))) . f now__::_thesis:_for_x_being_Element_of_SetVal_(V,p)_holds_f_._x_=_(((Perm_(P,(q_=>_p)))_*_f)_*_((Perm_(P,p))_"))_._x let x be Element of SetVal (V,p); ::_thesis: f . x = (((Perm (P,(q => p))) * f) * ((Perm (P,p)) ")) . x reconsider g = (SetVal (V,q)) --> (((Perm (P,p)) ") . x) as Function of (SetVal (V,q)),(SetVal (V,p)) ; x in SetVal (V,p) ; then x in rng (Perm (P,p)) by FUNCT_2:def_3; then A3: ((Perm (P,p)) ") . x in dom (Perm (P,p)) by PARTFUN2:60; thus f . x = (SetVal (V,q)) --> x by A2 .= (SetVal (V,q)) --> ((id (SetVal (V,p))) . x) by FUNCT_1:17 .= (SetVal (V,q)) --> (((Perm (P,p)) * ((Perm (P,p)) ")) . x) by FUNCT_2:61 .= (SetVal (V,q)) --> ((Perm (P,p)) . (((Perm (P,p)) ") . x)) by FUNCT_2:15 .= (Perm (P,p)) * ((SetVal (V,q)) --> (((Perm (P,p)) ") . x)) by A3, FUNCOP_1:17 .= (Perm (P,p)) * ((((Perm (P,q)) ") " (SetVal (V,q))) --> (((Perm (P,p)) ") . x)) by FUNCT_2:40 .= (Perm (P,p)) * (g * ((Perm (P,q)) ")) by FUNCOP_1:19 .= ((Perm (P,p)) * g) * ((Perm (P,q)) ") by RELAT_1:36 .= (Perm (P,(q => p))) . g by Th37 .= (Perm (P,(q => p))) . (f . (((Perm (P,p)) ") . x)) by A2 .= ((Perm (P,(q => p))) * f) . (((Perm (P,p)) ") . x) by FUNCT_2:15 .= (((Perm (P,(q => p))) * f) * ((Perm (P,p)) ")) . x by FUNCT_2:15 ; ::_thesis: verum end; hence f = ((Perm (P,(q => p))) * f) * ((Perm (P,p)) ") by FUNCT_2:63 .= (Perm (P,(p => (q => p)))) . f by Th37 ; ::_thesis: verum end; cluster(p '&' q) => p -> canonical ; coherence (p '&' q) => p is canonical proof let V be SetValuation; :: according to HILBERT3:def_7 ::_thesis: ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm (P,((p '&' q) => p)) take f = pr1 ((SetVal (V,p)),(SetVal (V,q))); ::_thesis: for P being Permutation of V holds f is_a_fixpoint_of Perm (P,((p '&' q) => p)) let P be Permutation of V; ::_thesis: f is_a_fixpoint_of Perm (P,((p '&' q) => p)) A4: dom (Perm (P,((p '&' q) => p))) = SetVal (V,((p '&' q) => p)) by FUNCT_2:def_1 .= Funcs ((SetVal (V,(p '&' q))),(SetVal (V,p))) by Def2 .= Funcs ([:(SetVal (V,p)),(SetVal (V,q)):],(SetVal (V,p))) by Def2 ; hence f in dom (Perm (P,((p '&' q) => p))) by FUNCT_2:8; :: according to ABIAN:def_3 ::_thesis: f = (Perm (P,((p '&' q) => p))) . f then f in Funcs ((SetVal (V,(p '&' q))),(SetVal (V,p))) by A4, Def2; then reconsider F = f as Function of (SetVal (V,(p '&' q))),(SetVal (V,p)) by FUNCT_2:66; thus (Perm (P,((p '&' q) => p))) . f = ((Perm (P,p)) * F) * ((Perm (P,(p '&' q))) ") by Th37 .= ((Perm (P,p)) * F) * ([:(Perm (P,p)),(Perm (P,q)):] ") by Th35 .= ((Perm (P,p)) * F) * [:((Perm (P,p)) "),((Perm (P,q)) "):] by FUNCTOR0:6 .= (Perm (P,p)) * (F * [:((Perm (P,p)) "),((Perm (P,q)) "):]) by RELAT_1:36 .= (Perm (P,p)) * (((Perm (P,p)) ") * F) by Th16 .= ((Perm (P,p)) * ((Perm (P,p)) ")) * F by RELAT_1:36 .= (id (SetVal (V,p))) * F by FUNCT_2:61 .= f by FUNCT_2:17 ; ::_thesis: verum end; cluster(p '&' q) => q -> canonical ; coherence (p '&' q) => q is canonical proof let V be SetValuation; :: according to HILBERT3:def_7 ::_thesis: ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm (P,((p '&' q) => q)) take f = pr2 ((SetVal (V,p)),(SetVal (V,q))); ::_thesis: for P being Permutation of V holds f is_a_fixpoint_of Perm (P,((p '&' q) => q)) let P be Permutation of V; ::_thesis: f is_a_fixpoint_of Perm (P,((p '&' q) => q)) A5: dom (Perm (P,((p '&' q) => q))) = SetVal (V,((p '&' q) => q)) by FUNCT_2:def_1 .= Funcs ((SetVal (V,(p '&' q))),(SetVal (V,q))) by Def2 .= Funcs ([:(SetVal (V,p)),(SetVal (V,q)):],(SetVal (V,q))) by Def2 ; hence f in dom (Perm (P,((p '&' q) => q))) by FUNCT_2:8; :: according to ABIAN:def_3 ::_thesis: f = (Perm (P,((p '&' q) => q))) . f then f in Funcs ((SetVal (V,(p '&' q))),(SetVal (V,q))) by A5, Def2; then reconsider F = f as Function of (SetVal (V,(p '&' q))),(SetVal (V,q)) by FUNCT_2:66; thus (Perm (P,((p '&' q) => q))) . f = ((Perm (P,q)) * F) * ((Perm (P,(p '&' q))) ") by Th37 .= ((Perm (P,q)) * F) * ([:(Perm (P,p)),(Perm (P,q)):] ") by Th35 .= ((Perm (P,q)) * F) * [:((Perm (P,p)) "),((Perm (P,q)) "):] by FUNCTOR0:6 .= (Perm (P,q)) * (F * [:((Perm (P,p)) "),((Perm (P,q)) "):]) by RELAT_1:36 .= (Perm (P,q)) * (((Perm (P,q)) ") * F) by Th17 .= ((Perm (P,q)) * ((Perm (P,q)) ")) * F by RELAT_1:36 .= (id (SetVal (V,q))) * F by FUNCT_2:61 .= f by FUNCT_2:17 ; ::_thesis: verum end; clusterp => (q => (p '&' q)) -> canonical ; coherence p => (q => (p '&' q)) is canonical proof let V be SetValuation; :: according to HILBERT3:def_7 ::_thesis: ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm (P,(p => (q => (p '&' q)))) take f = curry [:(id (SetVal (V,p))),(id (SetVal (V,q))):]; ::_thesis: for P being Permutation of V holds f is_a_fixpoint_of Perm (P,(p => (q => (p '&' q)))) let P be Permutation of V; ::_thesis: f is_a_fixpoint_of Perm (P,(p => (q => (p '&' q)))) f in Funcs ((SetVal (V,p)),(Funcs ((SetVal (V,q)),[:(SetVal (V,p)),(SetVal (V,q)):]))) by FUNCT_2:8; then f in Funcs ((SetVal (V,p)),(Funcs ((SetVal (V,q)),(SetVal (V,(p '&' q)))))) by Def2; then A6: f in Funcs ((SetVal (V,p)),(SetVal (V,(q => (p '&' q))))) by Def2; then reconsider F = f as Function of (SetVal (V,p)),(SetVal (V,(q => (p '&' q)))) by FUNCT_2:66; f in SetVal (V,(p => (q => (p '&' q)))) by A6, Def2; hence f in dom (Perm (P,(p => (q => (p '&' q))))) by FUNCT_2:def_1; :: according to ABIAN:def_3 ::_thesis: f = (Perm (P,(p => (q => (p '&' q))))) . f A7: now__::_thesis:_for_x_being_Element_of_SetVal_(V,p)_holds_f_._x_=_(((Perm_(P,(q_=>_(p_'&'_q))))_*_F)_*_((Perm_(P,p))_"))_._x let x be Element of SetVal (V,p); ::_thesis: f . x = (((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ")) . x set fx = f . x; F . x in SetVal (V,(q => (p '&' q))) ; then f . x in Funcs ((SetVal (V,q)),(SetVal (V,(p '&' q)))) by Def2; then reconsider fx = f . x as Function of (SetVal (V,q)),(SetVal (V,(p '&' q))) by FUNCT_2:66; set Fx = F . (((Perm (P,p)) ") . x); F . (((Perm (P,p)) ") . x) in SetVal (V,(q => (p '&' q))) ; then F . (((Perm (P,p)) ") . x) in Funcs ((SetVal (V,q)),(SetVal (V,(p '&' q)))) by Def2; then reconsider Fx = F . (((Perm (P,p)) ") . x) as Function of (SetVal (V,q)),(SetVal (V,(p '&' q))) by FUNCT_2:66; now__::_thesis:_for_y_being_Element_of_SetVal_(V,q)_holds_fx_._y_=_(((Perm_(P,(p_'&'_q)))_*_Fx)_*_((Perm_(P,q))_"))_._y let y be Element of SetVal (V,q); ::_thesis: fx . y = (((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ")) . y thus fx . y = [:(id (SetVal (V,p))),(id (SetVal (V,q))):] . (x,y) by FUNCT_5:69 .= [((id (SetVal (V,p))) . x),((id (SetVal (V,q))) . y)] by FUNCT_3:75 .= [((id (SetVal (V,p))) . x),(((Perm (P,q)) * ((Perm (P,q)) ")) . y)] by FUNCT_2:61 .= [((id (SetVal (V,p))) . x),((Perm (P,q)) . (((Perm (P,q)) ") . y))] by FUNCT_2:15 .= [(((Perm (P,p)) * ((Perm (P,p)) ")) . x),((Perm (P,q)) . (((Perm (P,q)) ") . y))] by FUNCT_2:61 .= [((Perm (P,p)) . (((Perm (P,p)) ") . x)),((Perm (P,q)) . (((Perm (P,q)) ") . y))] by FUNCT_2:15 .= [:(Perm (P,p)),(Perm (P,q)):] . ((((Perm (P,p)) ") . x),(((Perm (P,q)) ") . y)) by FUNCT_3:75 .= (Perm (P,(p '&' q))) . [(((Perm (P,p)) ") . x),(((Perm (P,q)) ") . y)] by Th35 .= (Perm (P,(p '&' q))) . [(((Perm (P,p)) ") . x),((id (SetVal (V,q))) . (((Perm (P,q)) ") . y))] by FUNCT_1:18 .= (Perm (P,(p '&' q))) . [((id (SetVal (V,p))) . (((Perm (P,p)) ") . x)),((id (SetVal (V,q))) . (((Perm (P,q)) ") . y))] by FUNCT_1:18 .= (Perm (P,(p '&' q))) . ([:(id (SetVal (V,p))),(id (SetVal (V,q))):] . ((((Perm (P,p)) ") . x),(((Perm (P,q)) ") . y))) by FUNCT_3:75 .= (Perm (P,(p '&' q))) . (Fx . (((Perm (P,q)) ") . y)) by FUNCT_5:69 .= ((Perm (P,(p '&' q))) * Fx) . (((Perm (P,q)) ") . y) by FUNCT_2:15 .= (((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ")) . y by FUNCT_2:15 ; ::_thesis: verum end; hence f . x = ((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ") by FUNCT_2:63 .= (Perm (P,(q => (p '&' q)))) . (F . (((Perm (P,p)) ") . x)) by Th37 .= ((Perm (P,(q => (p '&' q)))) * F) . (((Perm (P,p)) ") . x) by FUNCT_2:15 .= (((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ")) . x by FUNCT_2:15 ; ::_thesis: verum end; thus (Perm (P,(p => (q => (p '&' q))))) . f = ((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ") by Th37 .= f by A7, FUNCT_2:63 ; ::_thesis: verum end; end; registration let p, q, r be Element of HP-WFF ; cluster(p => (q => r)) => ((p => q) => (p => r)) -> canonical ; coherence (p => (q => r)) => ((p => q) => (p => r)) is canonical proof deffunc H1( Function) -> set = Frege p; let V be SetValuation; :: according to HILBERT3:def_7 ::_thesis: ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r)))) A1: ( SetVal (V,(p => q)) = Funcs ((SetVal (V,p)),(SetVal (V,q))) & SetVal (V,(p => r)) = Funcs ((SetVal (V,p)),(SetVal (V,r))) ) by Def2; A2: for x being Element of SetVal (V,(p => (q => r))) holds H1(x) in SetVal (V,((p => q) => (p => r))) proof let x be Element of SetVal (V,(p => (q => r))); ::_thesis: H1(x) in SetVal (V,((p => q) => (p => r))) x is Element of Funcs ((SetVal (V,p)),(SetVal (V,(q => r)))) by Def2; then x is Element of Funcs ((SetVal (V,p)),(Funcs ((SetVal (V,q)),(SetVal (V,r))))) by Def2; then Frege x is Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))) by A1, Th24; then Frege x in Funcs ((SetVal (V,(p => q))),(SetVal (V,(p => r)))) by FUNCT_2:8; hence Frege x in SetVal (V,((p => q) => (p => r))) by Def2; ::_thesis: verum end; consider F being Function of (SetVal (V,(p => (q => r)))),(SetVal (V,((p => q) => (p => r)))) such that A3: for x being Element of SetVal (V,(p => (q => r))) holds F . x = H1(x) from FUNCT_2:sch_8(A2); take F ; ::_thesis: for P being Permutation of V holds F is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r)))) let P be Permutation of V; ::_thesis: F is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r)))) F in Funcs ((SetVal (V,(p => (q => r)))),(SetVal (V,((p => q) => (p => r))))) by FUNCT_2:8; then F in SetVal (V,((p => (q => r)) => ((p => q) => (p => r)))) by Def2; hence F in dom (Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) by FUNCT_2:def_1; :: according to ABIAN:def_3 ::_thesis: F = (Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) . F now__::_thesis:_for_f_being_Element_of_SetVal_(V,(p_=>_(q_=>_r)))_holds_F_._f_=_(((Perm_(P,((p_=>_q)_=>_(p_=>_r))))_*_F)_*_((Perm_(P,(p_=>_(q_=>_r))))_"))_._f reconsider X = (Perm (P,(q => r))) " as Function of (SetVal (V,(q => r))),(SetVal (V,(q => r))) ; let f be Element of SetVal (V,(p => (q => r))); ::_thesis: F . f = (((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")) . f set Yf = ((Perm (P,(p => (q => r)))) ") . f; A4: SetVal (V,(q => r)) = Funcs ((SetVal (V,q)),(SetVal (V,r))) by Def2; f in SetVal (V,(p => (q => r))) ; then f in Funcs ((SetVal (V,p)),(SetVal (V,(q => r)))) by Def2; then reconsider ff = f as Function of (SetVal (V,p)),(SetVal (V,(q => r))) by FUNCT_2:66; ((Perm (P,(p => (q => r)))) ") . f = (((Perm (P,(q => r))) ") * ff) * (Perm (P,p)) by Th38; then reconsider h = Frege (((Perm (P,(p => (q => r)))) ") . f) as Function-yielding Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))) by A1, A4, Th24; set M = ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) "); A5: product (doms ff) = product ((SetVal (V,p)) --> (SetVal (V,q))) by A4, Th6 .= Funcs ((SetVal (V,p)),(SetVal (V,q))) by CARD_3:11 ; then A6: product (doms ff) = SetVal (V,(p => q)) by Def2; then reconsider M = ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) ") as ManySortedFunction of product (doms f) ; A7: for g being Function st g in product (doms f) holds M . g = f .. g proof ((Perm (P,(p => (q => r)))) ") . f in SetVal (V,(p => (q => r))) ; then ((Perm (P,(p => (q => r)))) ") . f in Funcs ((SetVal (V,p)),(SetVal (V,(q => r)))) by Def2; then ((Perm (P,(p => (q => r)))) ") . f is Function of (SetVal (V,p)),(Funcs ((SetVal (V,q)),(SetVal (V,r)))) by A4, FUNCT_2:66; then A8: product (doms (((Perm (P,(p => (q => r)))) ") . f)) = product ((SetVal (V,p)) --> (SetVal (V,q))) by Th6 .= Funcs ((SetVal (V,p)),(SetVal (V,q))) by CARD_3:11 .= SetVal (V,(p => q)) by Def2 ; reconsider FF = ff as Function of (SetVal (V,p)),(Funcs ((SetVal (V,q)),(SetVal (V,r)))) by Def2; let g be Function; ::_thesis: ( g in product (doms f) implies M . g = f .. g ) assume A9: g in product (doms f) ; ::_thesis: M . g = f .. g reconsider G = g as Function of (SetVal (V,p)),(SetVal (V,q)) by A5, A9, FUNCT_2:66; dom FF = SetVal (V,p) by FUNCT_2:def_1; then A10: dom (FF .. G) = SetVal (V,p) by PRALG_1:def_17; A11: rng (FF .. G) c= SetVal (V,r) by Th21; then reconsider GG = FF .. G as Function of (SetVal (V,p)),(SetVal (V,r)) by A10, FUNCT_2:def_1, RELSET_1:4; FF .. G is Function of (SetVal (V,p)),(SetVal (V,r)) by A10, A11, FUNCT_2:def_1, RELSET_1:4; then FF .. G in Funcs ((SetVal (V,p)),(SetVal (V,r))) by FUNCT_2:8; then A12: FF .. G in SetVal (V,(p => r)) by Def2; (((Perm (P,q)) ") * G) * (Perm (P,p)) in Funcs ((SetVal (V,p)),(SetVal (V,q))) by FUNCT_2:8; then A13: (((Perm (P,q)) ") * g) * (Perm (P,p)) in product (doms (((Perm (P,(p => (q => r)))) ") . f)) by A8, Def2; then A14: ((Perm (P,(p => q))) ") . G in SetVal (V,(p => q)) by A8, Th38; A15: X = ((Perm (P,q)) => (Perm (P,r))) " by Th36 .= ((Perm (P,q)) ") => ((Perm (P,r)) ") by Th27 ; A16: h . (((Perm (P,(p => q))) ") . g) = h . ((((Perm (P,q)) ") * G) * (Perm (P,p))) by Th38 .= (((Perm (P,(p => (q => r)))) ") . f) .. ((((Perm (P,q)) ") * g) * (Perm (P,p))) by A13, PRALG_2:def_2 .= ((X * ff) * (Perm (P,p))) .. ((((Perm (P,q)) ") * g) * (Perm (P,p))) by Th38 .= ((X * FF) .. (((Perm (P,q)) ") * g)) * (Perm (P,p)) by Th19 .= (((Perm (P,r)) ") * (FF .. G)) * (Perm (P,p)) by A15, Th28 .= ((Perm (P,(p => r))) ") . GG by Th38 ; thus M . g = ((Perm (P,(p => r))) * h) . (((Perm (P,(p => q))) ") . g) by A6, A9, FUNCT_2:15 .= (Perm (P,(p => r))) . (((Perm (P,(p => r))) ") . GG) by A14, A16, FUNCT_2:15 .= ((Perm (P,(p => r))) * ((Perm (P,(p => r))) ")) . GG by A12, FUNCT_2:15 .= (id (SetVal (V,(p => r)))) . GG by FUNCT_2:61 .= f .. g by A12, FUNCT_1:18 ; ::_thesis: verum end; thus F . f = Frege f by A3 .= ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) ") by A7, PRALG_2:def_2 .= (Perm (P,((p => q) => (p => r)))) . h by Th37 .= (Perm (P,((p => q) => (p => r)))) . (F . (((Perm (P,(p => (q => r)))) ") . f)) by A3 .= ((Perm (P,((p => q) => (p => r)))) * F) . (((Perm (P,(p => (q => r)))) ") . f) by FUNCT_2:15 .= (((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")) . f by FUNCT_2:15 ; ::_thesis: verum end; hence F = ((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ") by FUNCT_2:63 .= (Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) . F by Th37 ; ::_thesis: verum end; end; theorem Th41: :: HILBERT3:41 for p, q being Element of HP-WFF st p is canonical & p => q is canonical holds q is canonical proof let p, q be Element of HP-WFF ; ::_thesis: ( p is canonical & p => q is canonical implies q is canonical ) assume that A1: p is canonical and A2: p => q is canonical ; ::_thesis: q is canonical let V be SetValuation; :: according to HILBERT3:def_7 ::_thesis: ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm (P,q) consider x being set such that A3: for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p) by A1, Def7; set P = the Permutation of V; A4: dom (Perm ( the Permutation of V,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:52 .= Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2 ; consider f being set such that A5: for P being Permutation of V holds f is_a_fixpoint_of Perm (P,(p => q)) by A2, Def7; f is_a_fixpoint_of Perm ( the Permutation of V,(p => q)) by A5; then f in Funcs ((SetVal (V,p)),(SetVal (V,q))) by A4, ABIAN:def_3; then reconsider f = f as Function of (SetVal (V,p)),(SetVal (V,q)) by FUNCT_2:66; take f . x ; ::_thesis: for P being Permutation of V holds f . x is_a_fixpoint_of Perm (P,q) let P be Permutation of V; ::_thesis: f . x is_a_fixpoint_of Perm (P,q) A6: f is_a_fixpoint_of Perm (P,(p => q)) by A5; x is_a_fixpoint_of Perm (P,p) by A3; hence f . x is_a_fixpoint_of Perm (P,q) by A6, Th40; ::_thesis: verum end; theorem :: HILBERT3:42 for p being Element of HP-WFF st p in HP_TAUT holds p is canonical proof let p be Element of HP-WFF ; ::_thesis: ( p in HP_TAUT implies p is canonical ) set X = { q where q is Element of HP-WFF : q is canonical } ; { q where q is Element of HP-WFF : q is canonical } c= HP-WFF proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Element of HP-WFF : q is canonical } or x in HP-WFF ) assume x in { q where q is Element of HP-WFF : q is canonical } ; ::_thesis: x in HP-WFF then ex p being Element of HP-WFF st ( p = x & p is canonical ) ; hence x in HP-WFF ; ::_thesis: verum end; then reconsider X = { q where q is Element of HP-WFF : q is canonical } as Subset of HP-WFF ; X is Hilbert_theory proof thus VERUM in X ; :: according to HILBERT1:def_10 ::_thesis: for b1, b2, b3 being Element of HP-WFF holds ( b1 => (b2 => b1) in X & (b1 => (b2 => b3)) => ((b1 => b2) => (b1 => b3)) in X & (b1 '&' b2) => b1 in X & (b1 '&' b2) => b2 in X & b1 => (b2 => (b1 '&' b2)) in X & ( not b1 in X or not b1 => b2 in X or b2 in X ) ) let p, q, r be Element of HP-WFF ; ::_thesis: ( p => (q => p) in X & (p => (q => r)) => ((p => q) => (p => r)) in X & (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) ) thus p => (q => p) in X ; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in X & (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) ) thus (p => (q => r)) => ((p => q) => (p => r)) in X ; ::_thesis: ( (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) ) thus (p '&' q) => p in X ; ::_thesis: ( (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) ) thus (p '&' q) => q in X ; ::_thesis: ( p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) ) thus p => (q => (p '&' q)) in X ; ::_thesis: ( not p in X or not p => q in X or q in X ) assume p in X ; ::_thesis: ( not p => q in X or q in X ) then A1: ex s being Element of HP-WFF st ( s = p & s is canonical ) ; assume p => q in X ; ::_thesis: q in X then ex s being Element of HP-WFF st ( s = p => q & s is canonical ) ; then q is canonical by A1, Th41; hence q in X ; ::_thesis: verum end; then A2: HP_TAUT c= X by HILBERT1:13; assume p in HP_TAUT ; ::_thesis: p is canonical then p in X by A2; then ex q being Element of HP-WFF st ( p = q & q is canonical ) ; hence p is canonical ; ::_thesis: verum end; registration cluster Relation-like Function-like V51() canonical for Element of HP-WFF ; existence ex b1 being Element of HP-WFF st b1 is canonical proof take VERUM ; ::_thesis: VERUM is canonical thus VERUM is canonical ; ::_thesis: verum end; end; begin definition let p be Element of HP-WFF ; attrp is pseudo-canonical means :Def8: :: HILBERT3:def 8 for V being SetValuation for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,p); end; :: deftheorem Def8 defines pseudo-canonical HILBERT3:def_8_:_ for p being Element of HP-WFF holds ( p is pseudo-canonical iff for V being SetValuation for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,p) ); registration cluster canonical -> pseudo-canonical for Element of HP-WFF ; coherence for b1 being Element of HP-WFF st b1 is canonical holds b1 is pseudo-canonical proof let p be Element of HP-WFF ; ::_thesis: ( p is canonical implies p is pseudo-canonical ) assume A1: p is canonical ; ::_thesis: p is pseudo-canonical let V be SetValuation; :: according to HILBERT3:def_8 ::_thesis: for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,p) consider x being set such that A2: for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p) by A1, Def7; let P be Permutation of V; ::_thesis: ex x being set st x is_a_fixpoint_of Perm (P,p) take x ; ::_thesis: x is_a_fixpoint_of Perm (P,p) thus x is_a_fixpoint_of Perm (P,p) by A2; ::_thesis: verum end; end; theorem :: HILBERT3:43 for p, q being Element of HP-WFF st p is pseudo-canonical & p => q is pseudo-canonical holds q is pseudo-canonical proof let p, q be Element of HP-WFF ; ::_thesis: ( p is pseudo-canonical & p => q is pseudo-canonical implies q is pseudo-canonical ) assume that A1: p is pseudo-canonical and A2: p => q is pseudo-canonical ; ::_thesis: q is pseudo-canonical let V be SetValuation; :: according to HILBERT3:def_8 ::_thesis: for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,q) let P be Permutation of V; ::_thesis: ex x being set st x is_a_fixpoint_of Perm (P,q) consider x being set such that A3: x is_a_fixpoint_of Perm (P,p) by A1, Def8; consider f being set such that A4: f is_a_fixpoint_of Perm (P,(p => q)) by A2, Def8; dom (Perm (P,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:52 .= Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2 ; then f in Funcs ((SetVal (V,p)),(SetVal (V,q))) by A4, ABIAN:def_3; then reconsider f = f as Function of (SetVal (V,p)),(SetVal (V,q)) by FUNCT_2:66; take f . x ; ::_thesis: f . x is_a_fixpoint_of Perm (P,q) thus f . x is_a_fixpoint_of Perm (P,q) by A3, A4, Th40; ::_thesis: verum end; theorem Th44: :: HILBERT3:44 for p, q being Element of HP-WFF for V being SetValuation for P being Permutation of V st ex f being set st f is_a_fixpoint_of Perm (P,p) & ( for f being set holds not f is_a_fixpoint_of Perm (P,q) ) holds not p => q is pseudo-canonical proof let p, q be Element of HP-WFF ; ::_thesis: for V being SetValuation for P being Permutation of V st ex f being set st f is_a_fixpoint_of Perm (P,p) & ( for f being set holds not f is_a_fixpoint_of Perm (P,q) ) holds not p => q is pseudo-canonical let V be SetValuation; ::_thesis: for P being Permutation of V st ex f being set st f is_a_fixpoint_of Perm (P,p) & ( for f being set holds not f is_a_fixpoint_of Perm (P,q) ) holds not p => q is pseudo-canonical let P be Permutation of V; ::_thesis: ( ex f being set st f is_a_fixpoint_of Perm (P,p) & ( for f being set holds not f is_a_fixpoint_of Perm (P,q) ) implies not p => q is pseudo-canonical ) given x being set such that A1: x is_a_fixpoint_of Perm (P,p) ; ::_thesis: ( ex f being set st f is_a_fixpoint_of Perm (P,q) or not p => q is pseudo-canonical ) assume A2: for x being set holds not x is_a_fixpoint_of Perm (P,q) ; ::_thesis: not p => q is pseudo-canonical assume p => q is pseudo-canonical ; ::_thesis: contradiction then consider f being set such that A3: f is_a_fixpoint_of Perm (P,(p => q)) by Def8; f in dom (Perm (P,(p => q))) by A3, ABIAN:def_3; then f in SetVal (V,(p => q)) by FUNCT_2:def_1; then reconsider f = f as Function ; f . x is_a_fixpoint_of Perm (P,q) by A1, A3, Th40; hence contradiction by A2; ::_thesis: verum end; theorem :: HILBERT3:45 for a, b being Element of NAT st a <> b holds not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical proof let a, b be Element of NAT ; ::_thesis: ( a <> b implies not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical ) assume A1: a <> b ; ::_thesis: not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical set A = { ((0,1) --> (i,j)) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } ; set X = product ((0,1) --> (INT,INT)); { ((0,1) --> (i,j)) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } c= product ((0,1) --> (INT,INT)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((0,1) --> (i,j)) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } or x in product ((0,1) --> (INT,INT)) ) assume x in { ((0,1) --> (i,j)) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } ; ::_thesis: x in product ((0,1) --> (INT,INT)) then ex i, j being Element of INT st ( x = (0,1) --> (i,j) & ( i < j or ( i is even & i = j ) ) ) ; hence x in product ((0,1) --> (INT,INT)) by Th11; ::_thesis: verum end; then reconsider A = { ((0,1) --> (i,j)) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } as Subset of (product ((0,1) --> (INT,INT))) ; set p1 = (0,1) --> (1,0); A2: not b in dom (a .--> 2) by A1, FUNCOP_1:75; reconsider p1 = (0,1) --> (1,0) as Permutation of 2 by Th15; defpred S1[ set , set ] means ex i being Integer st ( \$1 = i & \$2 = i + 1 ); set V = (NAT --> INT) +* (a .--> 2); reconsider V = (NAT --> INT) +* (a .--> 2) as SetValuation ; A3: a in dom (a .--> 2) by FUNCOP_1:74; A4: 2 = (a .--> 2) . a by FUNCOP_1:72 .= V . a by A3, FUNCT_4:13 .= SetVal (V,(prop a)) by Def2 ; A5: for e being Element of INT ex u being Element of INT st S1[e,u] proof let e be Element of INT ; ::_thesis: ex u being Element of INT st S1[e,u] reconsider e = e as Integer ; reconsider u = e + 1 as Element of INT by INT_1:def_2; take u ; ::_thesis: S1[e,u] thus S1[e,u] ; ::_thesis: verum end; consider p0 being Function of INT,INT such that A6: for e being Element of INT holds S1[e,p0 . e] from FUNCT_2:sch_3(A5); A7: dom p0 = INT by FUNCT_2:def_1; for y being set holds ( y in INT iff ex x being set st ( x in dom p0 & y = p0 . x ) ) proof let y be set ; ::_thesis: ( y in INT iff ex x being set st ( x in dom p0 & y = p0 . x ) ) hereby ::_thesis: ( ex x being set st ( x in dom p0 & y = p0 . x ) implies y in INT ) assume y in INT ; ::_thesis: ex x being set st ( x in dom p0 & y = p0 . x ) then reconsider i = y as Integer ; reconsider x = i - 1 as set ; take x = x; ::_thesis: ( x in dom p0 & y = p0 . x ) thus x in dom p0 by A7, INT_1:def_2; ::_thesis: y = p0 . x then ex j being Integer st ( x = j & p0 . x = j + 1 ) by A6, A7; hence y = p0 . x by XCMPLX_1:27; ::_thesis: verum end; given x being set such that A8: x in dom p0 and A9: y = p0 . x ; ::_thesis: y in INT ex i being Integer st ( x = i & p0 . x = i + 1 ) by A6, A7, A8; hence y in INT by A9, INT_1:def_2; ::_thesis: verum end; then A10: rng p0 = INT by FUNCT_1:def_3; A11: p0 is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom p0 or not x2 in dom p0 or not p0 . x1 = p0 . x2 or x1 = x2 ) assume ( x1 in dom p0 & x2 in dom p0 ) ; ::_thesis: ( not p0 . x1 = p0 . x2 or x1 = x2 ) then reconsider I1 = x1, I2 = x2 as Element of INT by FUNCT_2:def_1; assume A12: p0 . x1 = p0 . x2 ; ::_thesis: x1 = x2 ( ex i1 being Integer st ( I1 = i1 & p0 . I1 = i1 + 1 ) & ex i2 being Integer st ( I2 = i2 & p0 . I2 = i2 + 1 ) ) by A6; hence x1 = x2 by A12, XCMPLX_1:2; ::_thesis: verum end; A13: SetVal (V,(prop b)) = V . b by Def2 .= (NAT --> INT) . b by A2, FUNCT_4:11 .= INT by FUNCOP_1:7 ; A14: product ((0,1) --> (INT,INT)) = product (2 --> INT) by CARD_1:50, FUNCT_4:65 .= Funcs (2,INT) by CARD_3:11 .= SetVal (V,((prop a) => (prop b))) by A4, A13, Def2 ; then reconsider f = chi (A,(product ((0,1) --> (INT,INT)))) as Function of (SetVal (V,((prop a) => (prop b)))),(SetVal (V,(prop a))) by A4, CARD_1:50; A15: a in dom (a .--> p1) by FUNCOP_1:74; reconsider p0 = p0 as Permutation of INT by A11, A10, FUNCT_2:57; set P = (NAT --> p0) +* (a .--> p1); A16: dom ((NAT --> p0) +* (a .--> p1)) = (dom (NAT --> p0)) \/ (dom (a .--> p1)) by FUNCT_4:def_1 .= (dom (NAT --> p0)) \/ {a} by FUNCOP_1:13 .= NAT \/ {a} by FUNCOP_1:13 .= NAT by ZFMISC_1:40 ; for n being Element of NAT holds ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n) proof let n be Element of NAT ; ::_thesis: ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n) percases ( n = a or n <> a ) ; supposeA17: n = a ; ::_thesis: ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n) then n in dom (a .--> 2) by FUNCOP_1:74; then A18: V . n = (a .--> 2) . a by A17, FUNCT_4:13 .= 2 by FUNCOP_1:72 ; n in dom (a .--> p1) by A17, FUNCOP_1:74; then ((NAT --> p0) +* (a .--> p1)) . n = (a .--> p1) . a by A17, FUNCT_4:13 .= p1 by FUNCOP_1:72 ; hence ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n) by A18; ::_thesis: verum end; supposeA19: n <> a ; ::_thesis: ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n) then not n in dom (a .--> 2) by FUNCOP_1:75; then A20: V . n = (NAT --> INT) . n by FUNCT_4:11 .= INT by FUNCOP_1:7 ; not n in dom (a .--> p1) by A19, FUNCOP_1:75; then ((NAT --> p0) +* (a .--> p1)) . n = (NAT --> p0) . n by FUNCT_4:11 .= p0 by FUNCOP_1:7 ; hence ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n) by A20; ::_thesis: verum end; end; end; then reconsider P = (NAT --> p0) +* (a .--> p1) as Permutation of V by A16, Def4; A21: Perm (P,(prop a)) = P . a by Def5 .= (a .--> p1) . a by A15, FUNCT_4:13 .= p1 by FUNCOP_1:72 ; A22: f is_a_fixpoint_of Perm (P,(((prop a) => (prop b)) => (prop a))) proof set Q = Perm (P,(((prop a) => (prop b)) => (prop a))); f in Funcs ((SetVal (V,((prop a) => (prop b)))),(SetVal (V,(prop a)))) by FUNCT_2:8; then f in SetVal (V,(((prop a) => (prop b)) => (prop a))) by Def2; hence f in dom (Perm (P,(((prop a) => (prop b)) => (prop a)))) by FUNCT_2:def_1; :: according to ABIAN:def_3 ::_thesis: f = (Perm (P,(((prop a) => (prop b)) => (prop a)))) . f rng ((Perm (P,((prop a) => (prop b)))) ") = dom (((Perm (P,((prop a) => (prop b)))) ") ") by FUNCT_1:32 .= product ((0,1) --> (INT,INT)) by A14, FUNCT_2:def_1 .= dom f by FUNCT_2:def_1 ; then A23: dom (f * ((Perm (P,((prop a) => (prop b)))) ")) = dom ((Perm (P,((prop a) => (prop b)))) ") by RELAT_1:27 .= rng (Perm (P,((prop a) => (prop b)))) by FUNCT_1:32 .= product ((0,1) --> (INT,INT)) by A14, FUNCT_2:def_3 .= dom (chi ((A `),(product ((0,1) --> (INT,INT))))) by FUNCT_3:def_3 ; for x being set st x in dom (chi ((A `),(product ((0,1) --> (INT,INT))))) holds (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = (chi ((A `),(product ((0,1) --> (INT,INT))))) . x proof A24: dom (p0 ") = INT by A10, FUNCT_1:32; let x be set ; ::_thesis: ( x in dom (chi ((A `),(product ((0,1) --> (INT,INT))))) implies (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = (chi ((A `),(product ((0,1) --> (INT,INT))))) . x ) A25: not b in dom (a .--> p1) by A1, FUNCOP_1:75; assume A26: x in dom (chi ((A `),(product ((0,1) --> (INT,INT))))) ; ::_thesis: (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = (chi ((A `),(product ((0,1) --> (INT,INT))))) . x then x in product ((0,1) --> (INT,INT)) by FUNCT_3:def_3; then x in Funcs ((SetVal (V,(prop a))),(SetVal (V,(prop b)))) by A14, Def2; then reconsider g = x as Function of (SetVal (V,(prop a))),(SetVal (V,(prop b))) by FUNCT_2:66; consider i0, j0 being Element of INT such that A27: g = (0,1) --> (i0,j0) by A4, A13, Th12; reconsider i0 = i0, j0 = j0 as Integer ; A28: j0 - 1 in dom p0 by A7, INT_1:def_2; then ex i being Integer st ( j0 - 1 = i & p0 . (j0 - 1) = i + 1 ) by A6, A7; then A29: p0 . (j0 - 1) = j0 by XCMPLX_1:27; A30: i0 - 1 in dom p0 by A7, INT_1:def_2; then ex i being Integer st ( i0 - 1 = i & p0 . (i0 - 1) = i + 1 ) by A6, A7; then p0 . (i0 - 1) = i0 by XCMPLX_1:27; then A31: (p0 ") . i0 = i0 - 1 by A30, FUNCT_1:34; Perm (P,(prop b)) = P . b by Def5 .= (NAT --> p0) . b by A25, FUNCT_4:11 .= p0 by FUNCOP_1:7 ; then A32: ((Perm (P,(prop b))) ") * g = (0,1) --> (((p0 ") . i0),((p0 ") . j0)) by A27, A24, Th14 .= (0,1) --> ((i0 - 1),(j0 - 1)) by A31, A28, A29, FUNCT_1:34 ; A33: (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = f . (((Perm (P,((prop a) => (prop b)))) ") . x) by A23, A26, FUNCT_1:12 .= f . ((((Perm (P,(prop b))) ") * g) * (Perm (P,(prop a)))) by Th38 .= f . ((0,1) --> ((j0 - 1),(i0 - 1))) by A21, A32, Th13 ; percases ( x in A or not x in A ) ; supposeA34: x in A ; ::_thesis: (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = (chi ((A `),(product ((0,1) --> (INT,INT))))) . x then consider i, j being Element of INT such that A35: x = (0,1) --> (i,j) and A36: ( i < j or ( i is even & i = j ) ) ; A37: ( i = i0 & j = j0 ) by A27, A35, Th10; A38: now__::_thesis:_not_(0,1)_-->_((j0_-_1),(i0_-_1))_in_A assume (0,1) --> ((j0 - 1),(i0 - 1)) in A ; ::_thesis: contradiction then consider i, j being Element of INT such that A39: (0,1) --> ((j0 - 1),(i0 - 1)) = (0,1) --> (i,j) and A40: ( i < j or ( i is even & i = j ) ) ; A41: ( i = j0 - 1 & j = i0 - 1 ) by A39, Th10; percases ( i < j or ( i is even & i = j ) ) by A40; suppose i < j ; ::_thesis: contradiction hence contradiction by A36, A37, A41, XREAL_1:9; ::_thesis: verum end; suppose ( i is even & i = j ) ; ::_thesis: contradiction hence contradiction by A36, A37, A41, XCMPLX_1:19; ::_thesis: verum end; end; end; A42: x in (A `) ` by A34; ( j0 - 1 in INT & i0 - 1 in INT ) by INT_1:def_2; then (0,1) --> ((j0 - 1),(i0 - 1)) in product ((0,1) --> (INT,INT)) by Th11; then (0,1) --> ((j0 - 1),(i0 - 1)) in (product ((0,1) --> (INT,INT))) \ A by A38, XBOOLE_0:def_5; hence (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = 0 by A33, FUNCT_3:37 .= (chi ((A `),(product ((0,1) --> (INT,INT))))) . x by A42, FUNCT_3:37 ; ::_thesis: verum end; supposeA43: not x in A ; ::_thesis: (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = (chi ((A `),(product ((0,1) --> (INT,INT))))) . x x in product ((0,1) --> (INT,INT)) by A27, Th11; then A44: x in (product ((0,1) --> (INT,INT))) \ A by A43, XBOOLE_0:def_5; A45: j0 - 1 is Element of INT by INT_1:def_2; A46: ( i0 is odd or i0 <> j0 ) by A27, A43; A47: i0 - 1 is Element of INT by INT_1:def_2; A48: i0 >= j0 by A27, A43; now__::_thesis:_(0,1)_-->_((j0_-_1),(i0_-_1))_in_A percases ( i0 > j0 or ( i0 = j0 & i0 is odd ) ) by A48, A46, XXREAL_0:1; suppose i0 > j0 ; ::_thesis: (0,1) --> ((j0 - 1),(i0 - 1)) in A then j0 - 1 < i0 - 1 by XREAL_1:9; hence (0,1) --> ((j0 - 1),(i0 - 1)) in A by A45, A47; ::_thesis: verum end; suppose ( i0 = j0 & i0 is odd ) ; ::_thesis: (0,1) --> ((j0 - 1),(i0 - 1)) in A hence (0,1) --> ((j0 - 1),(i0 - 1)) in A by A45; ::_thesis: verum end; end; end; hence (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = 1 by A33, FUNCT_3:def_3 .= (chi ((A `),(product ((0,1) --> (INT,INT))))) . x by A44, FUNCT_3:def_3 ; ::_thesis: verum end; end; end; then f * ((Perm (P,((prop a) => (prop b)))) ") = chi ((A `),(product ((0,1) --> (INT,INT)))) by A23, FUNCT_1:2; hence f = (Perm (P,(prop a))) * (f * ((Perm (P,((prop a) => (prop b)))) ")) by A21, Th9 .= ((Perm (P,(prop a))) * f) * ((Perm (P,((prop a) => (prop b)))) ") by RELAT_1:36 .= (Perm (P,(((prop a) => (prop b)) => (prop a)))) . f by Th37 ; ::_thesis: verum end; for x being set holds not x is_a_fixpoint_of Perm (P,(prop a)) proof let x be set ; ::_thesis: not x is_a_fixpoint_of Perm (P,(prop a)) a in dom (a .--> 2) by FUNCOP_1:74; then V . a = (a .--> 2) . a by FUNCT_4:13; then A49: V . a = 2 by FUNCOP_1:72; assume x in dom (Perm (P,(prop a))) ; :: according to ABIAN:def_3 ::_thesis: not x = (Perm (P,(prop a))) . x then x in SetVal (V,(prop a)) by FUNCT_2:def_1; then x in V . a by Def2; then ( x = 0 or x = 1 ) by A49, CARD_1:50, TARSKI:def_2; hence not x = (Perm (P,(prop a))) . x by A21, FUNCT_4:63; ::_thesis: verum end; hence not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical by A22, Th44; ::_thesis: verum end;