:: by Andrzej Trybulec

::

:: Received July 4, 2000

:: Copyright (c) 2000-2021 Association of Mizar Users

registration

let m, n be non zero Nat;

coherence

(0,n) --> (m,0) is one-to-one

(n,0) --> (0,m) is one-to-one

end;
coherence

(0,n) --> (m,0) is one-to-one

proof end;

coherence (n,0) --> (0,m) is one-to-one

proof end;

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

for x being set st x in X holds

for f being Function of X,X holds x is_a_fixpoint_of f

proof end;

::$CT

theorem Th5: :: 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

for f being Function of A,(Funcs (B,C)) holds doms f = A --> B

proof end;

theorem Th9: :: 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 )

( x = x9 & y = y9 )

proof end;

theorem Th10: :: 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))

(a,b) --> (x,y) in product ((a,b) --> (X,Y))

proof end;

theorem Th11: :: 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)

for f being Function of 2,D ex d1, d2 being Element of D st f = (0,1) --> (d1,d2)

proof end;

theorem Th13: :: 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))

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

theorem Th15: :: 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))

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

theorem Th16: :: 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))

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

theorem Th18: :: HILBERT3:19

for f being Function-yielding Function

for g, h being Function st dom f = dom g holds

(f .. g) * h = (f * h) .. (g * h)

for g, h being Function st dom f = dom g holds

(f .. g) * h = (f * h) .. (g * h)

proof 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) = {}

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

theorem Th20: :: HILBERT3:21

for A, B, C being set st ( B = {} implies A = {} ) & ( C = {} implies B = {} ) holds

for f being Function of A,(Funcs (B,C))

for g being Function of A,B holds rng (f .. g) c= C

for f being Function of A,(Funcs (B,C))

for g being Function of A,B holds rng (f .. g) c= C

proof end;

theorem Th21: :: 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)

for f being Function of A,(Funcs (B,C)) holds dom (Frege f) = Funcs (A,B)

proof end;

theorem Th22: :: 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)

for f being Function of A,(Funcs (B,C)) holds rng (Frege f) c= Funcs (A,C)

proof end;

theorem Th23: :: 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))

for f being Function of A,(Funcs (B,C)) holds Frege f is Function of (Funcs (A,B)),(Funcs (A,C))

proof end;

registration

let A, B be set ;

let P be Permutation of A;

let Q be Permutation of B;

coherence

for b_{1} being Function of [:A,B:],[:A,B:] st b_{1} = [:P,Q:] holds

b_{1} is bijective

end;
let P be Permutation of A;

let Q be Permutation of B;

coherence

for b

b

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

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;

ex b_{1} being Function of (Funcs (A,B)),(Funcs (A,B)) st

for f being Function of A,B holds b_{1} . f = (Q * f) * (P ")

for b_{1}, b_{2} being Function of (Funcs (A,B)),(Funcs (A,B)) st ( for f being Function of A,B holds b_{1} . f = (Q * f) * (P ") ) & ( for f being Function of A,B holds b_{2} . f = (Q * f) * (P ") ) holds

b_{1} = b_{2}

end;
let P be Permutation of A;

let Q be Function of B,B;

func P => 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 for f being Function of A,B holds it . f = (Q * f) * (P ");

ex b

for f being Function of A,B holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being Function of (Funcs (A,B)),(Funcs (A,B)) holds

( b_{5} = P => Q iff for f being Function of A,B holds b_{5} . f = (Q * f) * (P ") );

for A, B being non empty set

for P being Permutation of A

for Q being Function of B,B

for b

( b

registration

let A, B be non empty set ;

let P be Permutation of A;

let Q be Permutation of B;

coherence

P => Q is bijective

end;
let P be Permutation of A;

let Q be Permutation of B;

coherence

P => Q is bijective

proof end;

theorem Th25: :: 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

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

theorem Th26: :: 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 ")

for P being Permutation of A

for Q being Permutation of B holds (P => Q) " = (P ") => (Q ")

proof end;

theorem Th27: :: 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)

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

definition

let V be SetValuation;

ex b_{1} being ManySortedSet of HP-WFF st

( b_{1} . VERUM = 1 & ( for n being Element of NAT holds b_{1} . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( b_{1} . (p '&' q) = [:(b_{1} . p),(b_{1} . q):] & b_{1} . (p => q) = Funcs ((b_{1} . p),(b_{1} . q)) ) ) )

for b_{1}, b_{2} being ManySortedSet of HP-WFF st b_{1} . VERUM = 1 & ( for n being Element of NAT holds b_{1} . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( b_{1} . (p '&' q) = [:(b_{1} . p),(b_{1} . q):] & b_{1} . (p => q) = Funcs ((b_{1} . p),(b_{1} . q)) ) ) & b_{2} . VERUM = 1 & ( for n being Element of NAT holds b_{2} . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( b_{2} . (p '&' q) = [:(b_{2} . p),(b_{2} . q):] & b_{2} . (p => q) = Funcs ((b_{2} . p),(b_{2} . q)) ) ) holds

b_{1} = b_{2}

end;
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 ( 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)) ) ) );

ex b

( b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def2 defines SetVal HILBERT3:def 2 :

for V being SetValuation

for b_{2} being ManySortedSet of HP-WFF holds

( b_{2} = SetVal V iff ( b_{2} . VERUM = 1 & ( for n being Element of NAT holds b_{2} . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( b_{2} . (p '&' q) = [:(b_{2} . p),(b_{2} . q):] & b_{2} . (p => q) = Funcs ((b_{2} . p),(b_{2} . q)) ) ) ) );

for V being SetValuation

for b

( b

( b

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

for V being SetValuation

for p being Element of HP-WFF holds SetVal (V,p) = (SetVal V) . p;

registration
end;

theorem :: HILBERT3:30

theorem :: HILBERT3:31

theorem :: HILBERT3:32

registration

let V be SetValuation;

let p, q be Element of HP-WFF ;

coherence

SetVal (V,(p => q)) is functional

end;
let p, q be Element of HP-WFF ;

coherence

SetVal (V,(p => q)) is functional

proof end;

registration

let V be SetValuation;

let p, q, r be Element of HP-WFF ;

coherence

for b_{1} being Element of SetVal (V,(p => (q => r))) holds b_{1} is Function-yielding

end;
let p, q, r be Element of HP-WFF ;

coherence

for b

proof end;

registration

let V be SetValuation;

let p, q, r be Element of HP-WFF ;

ex b_{1} being Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))) st b_{1} is Function-yielding

ex b_{1} being Element of SetVal (V,(p => (q => r))) st b_{1} is Function-yielding

end;
let p, q, r be Element of HP-WFF ;

cluster Relation-like SetVal (V,(p => q)) -defined SetVal (V,(p => r)) -valued non empty Function-like total quasi_total Function-yielding V59() for Element of bool [:(SetVal (V,(p => q))),(SetVal (V,(p => r))):];

existence ex b

proof end;

cluster Relation-like Function-like Function-yielding V59() for Element of SetVal (V,(p => (q => r)));

existence ex b

proof end;

definition

let V be SetValuation;

ex b_{1} being Function st

( dom b_{1} = NAT & ( for n being Element of NAT holds b_{1} . n is Permutation of (V . n) ) )

end;
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 ( dom it = NAT & ( for n being Element of NAT holds it . n is Permutation of (V . n) ) );

ex b

( dom b

proof end;

:: deftheorem Def4 defines Permutation HILBERT3:def 4 :

for V being SetValuation

for b_{2} being Function holds

( b_{2} is Permutation of V iff ( dom b_{2} = NAT & ( for n being Element of NAT holds b_{2} . n is Permutation of (V . n) ) ) );

for V being SetValuation

for b

( b

definition

let V be SetValuation;

let P be Permutation of V;

ex b_{1} being ManySortedFunction of SetVal V, SetVal V st

( b_{1} . VERUM = id 1 & ( for n being Element of NAT holds b_{1} . (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 = b_{1} . p & q9 = b_{1} . q & b_{1} . (p '&' q) = [:p9,q9:] & b_{1} . (p => q) = p9 => q9 ) ) )

for b_{1}, b_{2} being ManySortedFunction of SetVal V, SetVal V st b_{1} . VERUM = id 1 & ( for n being Element of NAT holds b_{1} . (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 = b_{1} . p & q9 = b_{1} . q & b_{1} . (p '&' q) = [:p9,q9:] & b_{1} . (p => q) = p9 => q9 ) ) & b_{2} . VERUM = id 1 & ( for n being Element of NAT holds b_{2} . (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 = b_{2} . p & q9 = b_{2} . q & b_{2} . (p '&' q) = [:p9,q9:] & b_{2} . (p => q) = p9 => q9 ) ) holds

b_{1} = b_{2}

end;
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 ( 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 ) ) );

ex b

( b

( p9 = b

proof end;

uniqueness for b

( p9 = b

( p9 = b

b

proof end;

:: deftheorem Def5 defines Perm HILBERT3:def 5 :

for V being SetValuation

for P being Permutation of V

for b_{3} being ManySortedFunction of SetVal V, SetVal V holds

( b_{3} = Perm P iff ( b_{3} . VERUM = id 1 & ( for n being Element of NAT holds b_{3} . (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 = b_{3} . p & q9 = b_{3} . q & b_{3} . (p '&' q) = [:p9,q9:] & b_{3} . (p => q) = p9 => q9 ) ) ) );

for V being SetValuation

for P being Permutation of V

for b

( b

( p9 = b

definition

let V be SetValuation;

let P be Permutation of V;

let p be Element of HP-WFF ;

correctness

coherence

(Perm P) . p is Function of (SetVal (V,p)),(SetVal (V,p));

;

end;
let P be Permutation of V;

let p be Element of HP-WFF ;

correctness

coherence

(Perm P) . p is Function of (SetVal (V,p)),(SetVal (V,p));

;

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

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

for V being SetValuation

for P being Permutation of V holds Perm (P,(prop n)) = P . n by Def5;

theorem Th34: :: 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)):]

for V being SetValuation

for P being Permutation of V holds Perm (P,(p '&' q)) = [:(Perm (P,p)),(Perm (P,q)):]

proof end;

theorem Th35: :: 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

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

registration

let V be SetValuation;

let P be Permutation of V;

let p be Element of HP-WFF ;

coherence

Perm (P,p) is bijective

end;
let P be Permutation of V;

let p be Element of HP-WFF ;

coherence

Perm (P,p) is bijective

proof end;

theorem Th36: :: 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)) ")

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

theorem Th37: :: 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))

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

theorem Th38: :: 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))

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

theorem Th39: :: 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)

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

definition

let p be Element of HP-WFF ;

end;
attr p is canonical means :: 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);

for V being SetValuation ex x being set st

for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p);

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

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

let p, q be Element of HP-WFF ;

coherence

p => (q => p) is canonical

(p '&' q) => p is canonical

(p '&' q) => q is canonical

p => (q => (p '&' q)) is canonical

end;
coherence

p => (q => p) is canonical

proof end;

coherence (p '&' q) => p is canonical

proof end;

coherence (p '&' q) => q is canonical

proof end;

coherence p => (q => (p '&' q)) is canonical

proof end;

registration

let p, q, r be Element of HP-WFF ;

coherence

(p => (q => r)) => ((p => q) => (p => r)) is canonical

end;
coherence

(p => (q => r)) => ((p => q) => (p => r)) is canonical

proof end;

definition

let p be Element of HP-WFF ;

end;
attr p is pseudo-canonical means :: 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);

for V being SetValuation

for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,p);

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

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

coherence

for b_{1} being Element of HP-WFF st b_{1} is canonical holds

b_{1} is pseudo-canonical

end;
for b

b

proof 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

q is pseudo-canonical

proof end;

theorem Th43: :: 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

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

not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical

proof end;