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