:: The canonical formulae
:: by Andrzej Trybulec
::
:: Received July 4, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies INT_1, ABIAN, ARYTM_1, ZFMISC_1, FUNCT_1, RELAT_1, TARSKI,
FUNCOP_1, FUNCT_2, FUNCT_6, XBOOLE_0, PBOOLE, SUBSET_1, NUMBERS, NAT_1,
HILBERT1, CARD_1, FUNCT_3, CARD_3, MCART_1, PARTFUN1, FINSEQ_4, XBOOLEAN,
QC_LANG1, HILBERT2, FUNCT_5, ARYTM_3, FUNCT_4, XXREAL_0, HILBERT3,
XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
INT_1, RELAT_1, FUNCT_1, PBOOLE, CARD_1, CARD_3, ABIAN, PARTFUN1,
FUNCT_2, BINOP_1, XXREAL_0, FUNCT_3, FUNCOP_1, FUNCT_4, FUNCT_5, FUNCT_6,
PRALG_1, PRALG_2, MSUALG_3, HILBERT1, HILBERT2;
constructors XXREAL_0, NAT_D, ABIAN, CAT_2, PRALG_1, PRALG_2, MSUALG_3,
HILBERT2, RELSET_1, FUNCT_5, FUNCT_4;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
FUNCT_2, FUNCOP_1, FUNCT_4, NUMBERS, XREAL_0, INT_1, PBOOLE, ABIAN,
HILBERT1, RELSET_1, ZFMISC_1, MSSUBFAM, CARD_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions PBOOLE, FUNCT_1, FUNCT_2, TARSKI, HILBERT1, ABIAN, FUNCOP_1,
XBOOLE_0;
equalities HILBERT1, FUNCOP_1, BINOP_1, SUBSET_1, ORDINAL1;
expansions PBOOLE, FUNCT_1, ABIAN;
theorems PBOOLE, ZFMISC_1, MSUALG_3, FUNCT_2, RELAT_1, RELSET_1, FUNCT_1,
FUNCT_3, TARSKI, FUNCOP_1, PARTFUN2, PRALG_2, CARD_3, FUNCT_6, MSSUBFAM,
FUNCT_5, FUNCTOR0, HILBERT1, FUNCT_4, INT_1, TOPREAL6, PRALG_1, XBOOLE_0,
XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, CARD_1, PARTFUN1, XTUPLE_0;
schemes HILBERT2, FUNCT_2;
begin :: Preliminaries
registration
let m,n be non zero Nat;
cluster (0,n)-->(m,0) -> one-to-one;
coherence
proof
set f = (0,n)-->(m,0);
let x1,x2 be object;
assume that
A1: x1 in dom f and
A2: x2 in dom f;
A3: dom f = {0,n} by FUNCT_4:62;
then
A4: x2 = 0 or x2 = n by A2,TARSKI:def 2;
A5: f.0 = m by FUNCT_4:63;
x1 = 0 or x1 = n by A3,A1,TARSKI:def 2;
hence thesis by A4,A5,FUNCT_4:63;
end;
cluster (n,0)-->(0,m) -> one-to-one;
coherence
proof
set f = (n,0)-->(0,m);
let x1,x2 be object;
assume that
A6: x1 in dom f and
A7: x2 in dom f;
A8: dom f = {0,n} by FUNCT_4:62;
then
A9: x2 = 0 or x2 = n by A7,TARSKI:def 2;
A10: f.0 = m by FUNCT_4:63;
x1 = 0 or x1 = n by A8,A6,TARSKI:def 2;
hence thesis by A9,A10,FUNCT_4:63;
end;
end;
theorem
for i being Integer holds i is even iff i-1 is odd;
theorem
for i being Integer holds i is odd iff i-1 is even;
theorem Th3:
for X being trivial set, x being set st x in X for f being
Function of X,X holds x is_a_fixpoint_of f
proof
let X be trivial set, x be set;
assume
A1: x in X;
then consider y being object such that
A2: X = {y} by ZFMISC_1:131;
let f be Function of X,X;
thus x in dom f by A1,FUNCT_2:52;
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;
end;
::$CT
theorem Th4:
for A,B,x being set, f being Function st x in A & f in Funcs(A,B)
holds f.x in B
proof
let A,B,x be set, f be Function such that
A1: x in A;
assume
A2: f in Funcs(A,B);
then
A3: f is Function of A,B by FUNCT_2:66;
B = {} implies A = {} by A2;
hence thesis by A1,A3,FUNCT_2:5;
end;
theorem Th5:
for A,B,C being set st C = {} implies B = {} or A = {}
for f being Function of A, Funcs(B,C) holds doms f = A --> B
proof
let A,B,C be set;
assume C = {} implies B = {} or A = {};
then
A1: Funcs(B,C) = {} implies A = {} by FUNCT_2:8;
let f be Function of A, Funcs(B,C);
reconsider g = f as ManySortedFunction of A by A1;
now
let i be object;
assume
A2: i in A;
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;
end;
hence thesis by PBOOLE:3;
end;
reserve n for Element of NAT,
p,q,r,s for Element of HP-WFF;
theorem
for x being set holds {}.x = {};
theorem Th7:
for X being set, A being Subset of X holds
((0,1) --> (1,0))*chi(A,X) = chi(A`,X)
proof
let X be set, A be Subset of 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 object st x in X holds (x in A` implies f.x = 1) &
(not x in A` implies f.x = 0)
proof
let x be object such that
A3: x in X;
thus x in A` implies f.x = 1
proof
assume x in A`;
then not x in A by XBOOLE_0:def 5;
then chi(A,X).x = 0 by A3,FUNCT_3:def 3;
then f.x = ((0,1) --> (1,0)).0 by A1,A3,FUNCT_1:13;
hence thesis by FUNCT_4:63;
end;
assume not x in A`;
then x in A by A3,XBOOLE_0:def 5;
then chi(A,X).x = 1 by FUNCT_3:def 3;
then f.x = ((0,1) --> (1,0)).1 by A1,A3,FUNCT_1:13;
hence thesis by FUNCT_4:63;
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;
hence thesis by A2,FUNCT_3:def 3,A1,RELAT_1:27;
end;
theorem Th8:
for X being set, A being Subset of X holds
((0,1) --> (1,0))*chi(A`,X) = chi(A,X)
proof
let X be set, A be Subset of X;
A`` = A;
hence thesis by Th7;
end;
theorem Th9:
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 such that
A1: a <> b and
A2: (a,b) --> (x,y) = (a,b) --> (x9,y9);
thus x = ((a,b) --> (x,y)).a by A1,FUNCT_4:63
.= x9 by A1,A2,FUNCT_4:63;
thus y = ((a,b) --> (x,y)).b by FUNCT_4:63
.= y9 by A2,FUNCT_4:63;
end;
theorem Th10:
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 such that
A1: a<>b and
A2: x in X & y in 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 thesis by ZFMISC_1:31;
end;
theorem Th11:
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;
let f be Function of 2, D;
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,d2;
dom f = {0,1} by CARD_1:50,FUNCT_2:def 1;
hence thesis by FUNCT_4:66;
end;
theorem Th12:
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 such that
A1: a <> b;
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: f.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: f.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;
hence thesis by A4,A3,FUNCT_4:66,A2,RELAT_1:27;
end;
theorem Th13:
for a,b,c,d being set, 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, f be Function such that
A1: a <> b and
A2: c in dom f & d in dom f;
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 thesis by A4,A5,FUNCT_4:66;
end;
theorem Th14:
(0,1) --> (1,0) is Permutation of 2
proof
set f = (0,1) --> (1,0);
A1: rng f = 2 by CARD_1:50,FUNCT_4:64;
dom f = 2 by CARD_1:50,FUNCT_4:62;
then f is Function of 2,2 by A1,FUNCT_2:def 1,RELSET_1:4;
hence thesis by A1,FUNCT_2:57;
end;
begin :: the Cartesian product of functions and the Frege function
registration
let f,g be one-to-one Function;
cluster [:f,g:] -> one-to-one;
coherence
proof
let x,y be object such that
A1: x in dom[:f,g:] and
A2: y in dom[:f,g:] and
A3: [:f,g:].x = [:f,g:].y;
A4: dom[:f,g:] = [:dom f, dom g:] by FUNCT_3:def 8;
then consider x1,x2 being object 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 object 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 thesis by A6,A7,A10,A11,A13,FUNCT_1:def 4;
end;
end;
theorem Th15:
for A,B being non empty set, C,D being set,
f being Function of C,A,
g being Function of D,B holds pr1(A,B)*[:f,g:] = f*pr1(C,D)
proof
let A,B be non empty set, C,D be set;
let f be Function of C,A, g be Function of D,B;
C = {} implies A = {} or [:C,D:] = {};
then reconsider F = f*pr1(C,D) as Function of [:C,D:], A;
D = {} implies 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;
end;
theorem Th16:
for A,B being non empty set, C,D being set, f being Function of C,A,
g being Function of D,B holds pr2(A,B)*[:f,g:] = g*pr2(C,D)
proof
let A,B be non empty set, C,D be set;
let f be Function of C,A, g be Function of D,B;
C = {} implies A = {} or [:C,D:] = {};
then reconsider F = f*pr1(C,D) as Function of [:C,D:], A;
D = {} implies 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;
end;
theorem
for g being Function holds ({})..g = {}
proof
let g be Function;
dom (({})..g) = dom {} /\ dom g by PRALG_1:def 19
.= dom {};
hence thesis;
end;
theorem Th18:
for f being Function-yielding Function, g,h being Function
st dom f = dom g holds (f..g)*h = (f*h)..(g*h)
proof
let f be Function-yielding Function, g,h be Function;
assume
AA: dom f = dom g;
A0: dom((f*h)..(g*h)) = dom (f*h) /\ dom (g*h) by PRALG_1:def 19;
A1: for x being set st x in dom((f*h)..(g*h))
holds ((f..g)*h).x = ((f*h).x).((g*h).x)
proof
let x be set;
assume x in dom((f*h)..(g*h)); then
x in dom (f*h) /\ dom (g*h) by PRALG_1:def 19; then
a3: x in dom (f*h) & x in dom (g*h) by XBOOLE_0:def 4; then
A3: x in dom h by FUNCT_1:11;
h.x in dom f & h.x in dom g by a3,FUNCT_1:11; then
h.x in dom f /\ dom g by XBOOLE_0:def 4; then
a4: h.x in dom (f..g) by PRALG_1:def 19;
thus ((f..g)*h).x = (f..g).(h.x) by A3,FUNCT_1:13
.= (f.(h.x)).(g.(h.x)) by PRALG_1:def 19,a4
.= ((f*h).x).(g.(h.x)) by A3,FUNCT_1:13
.= (f*h).x .((g*h).x) by A3,FUNCT_1:13;
end;
a1: dom (f*h) = dom (g*h) by AA,RELAT_1:163;
dom (f..g) = dom f /\ dom g by PRALG_1:def 19
.= dom f by AA; then
dom((f..g)*h) = dom(f*h) by RELAT_1:163;
hence thesis by A1,A0,PRALG_1:def 19,a1;
end;
theorem
for C being set, A being non empty set
for f being Function of A,Funcs({} qua set,C),
g being Function of A,{} holds rng (f..g) = {}
proof
let C be set, A be non empty set;
let f be Function of A, Funcs({} qua set,C), g be Function of A,{};
set a = the Element of A;
dom(f..g) = dom f /\ dom g by PRALG_1:def 19 .= {};
hence thesis by RELAT_1:42;
end;
theorem Th20:
for A,B,C being set st (B = {} implies A = {}) & (C = {} implies B = {})
for f being Function of A, Funcs(B,C),
g being Function of A,B holds rng(f..g) c= C
proof
let A,B,C be set such that
A1: B = {} implies A = {} and
a1: C = {} implies B = {};
let f be Function of A, Funcs(B,C), g be Function of A,B;
let x be object;
assume x in rng(f..g);
then consider y being object such that
A2: y in dom(f..g) and
A3: (f..g).y = x by FUNCT_1:def 3;
S1: dom f = dom g
proof
per cases;
suppose B <> {}; then
C1: dom g = A by FUNCT_2:def 1;
Funcs(B,C) <> {} by a1,FUNCT_2:8;
hence thesis by C1,FUNCT_2:def 1;
end;
suppose B = {};
hence thesis by A1;
end;
end;
A4: dom(f..g) = dom f /\ dom g by PRALG_1:def 19 .= dom f by S1; 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,66;
A7: C <> {} by A1,A2,A4;
g.y in B by A1,A2,A4,A6,FUNCT_2:5;
then fy.(g.y) in C by A7,FUNCT_2:5;
hence thesis by A2,A3,PRALG_1:def 19;
end;
theorem Th21:
for A,B,C being set st C = {} implies B = {} or A = {}
for f being Function of A, Funcs(B,C) holds dom Frege f = Funcs(A,B)
proof
let A,B,C be set such that
A1: C = {} implies B = {} or A = {};
let f be Function of A, Funcs(B,C);
thus dom Frege f = product doms f by PARTFUN1:def 2
.= product(A --> B) by A1,Th5
.= Funcs(A,B) by CARD_3:11;
end;
theorem Th22:
for A,B,C being set st C = {} implies B = {} or A = {}
for f being Function of A, Funcs(B,C) holds rng Frege f c= Funcs(A,C)
proof
let A,B,C be set;
assume C = {} implies B = {} or A = {};
then
A1: Funcs(B,C) = {} implies A = {} by FUNCT_2:8;
let f be Function of A, Funcs(B,C);
A2: dom rngs f = dom f by FUNCT_6:def 3; then
A3: dom rngs f = A by A1,FUNCT_2:def 1;
A4: for x being object st x in dom rngs f holds (rngs f).x c= (A-->C).x
proof
let x be object such that
A5: x in dom rngs f;
A6: (rngs f).x = rng(f.x) by A2,A5,FUNCT_6:def 3;
f.x in Funcs(B,C) by A1,A3,A5,FUNCT_2:5;
then (rngs f).x c= C by A6,FUNCT_2:92;
hence thesis by A3,A5,FUNCOP_1:7;
end;
dom rngs f = dom(A-->C) by A3;
then product rngs f c= product(A --> C) by A4,CARD_3:27;
then product rngs f c= Funcs(A,C) by CARD_3:11;
hence thesis by FUNCT_6:38;
end;
theorem Th23:
for A,B,C being set st C = {} implies B = {} or A = {}
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;
assume
A1: C = {} implies B = {} or A = {}; then
A2: Funcs(A,C) = {} implies Funcs(A,B) = {} by FUNCT_2:8;
let f be Function of A, Funcs(B,C);
dom Frege f = Funcs(A,B) & rng Frege f c= Funcs(A,C) by A1,Th21,Th22;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:4;
end;
begin :: about permutations
registration
let A,B be set, P be Permutation of A, Q be Permutation of B;
cluster [:P,Q:] -> bijective for Function of [:A,B:],[:A,B:];
coherence
proof
[:P,Q:] is bijective
proof
thus [:P,Q:] is one-to-one;
rng P = A & rng Q = B by FUNCT_2:def 3;
hence rng [:P,Q:] = [:A,B:] by FUNCT_3:67;
end;
hence thesis;
end;
end;
theorem
for A,B being set, P being Permutation of A, Q being Permutation of B holds
[:P,Q:] is bijective;
definition
let A,B be non empty set;
let P be Permutation of A, Q be Function of B,B;
func P => Q -> Function of Funcs(A,B), Funcs(A,B) means
:Def1:
for f being Function of A,B holds it.f = Q*f*P";
existence
proof
deffunc F1(Element of Funcs(A,B))=Q*$1*P";
A1: for f being Element of Funcs(A,B) holds F1(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 = F1(f) from FUNCT_2:
sch 8(A1);
take F;
let f be Function of A,B;
f in Funcs(A,B) by FUNCT_2:8;
hence thesis by A2;
end;
uniqueness
proof
let F,G be Function of Funcs(A,B), Funcs(A,B) such 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";
now
let f be Element of Funcs(A,B);
thus F.f = Q*f*P" by A3
.= G.f by A4;
end;
hence F = G;
end;
end;
registration
let A,B be non empty set;
let P be Permutation of A, Q be Permutation of B;
cluster P => Q -> bijective;
coherence
proof
thus P => Q is one-to-one
proof
let x1,x2 be object;
assume x1 in dom(P => Q) & x2 in dom(P => Q);
then reconsider f1 = x1, f2 = x2 as Element of Funcs(A,B) by
FUNCT_2:def 1;
assume (P => Q).x1 = (P => Q).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 thesis;
end;
thus rng(P => Q) c= Funcs(A,B) by RELAT_1:def 19;
let x be object;
assume x in Funcs(A,B);
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;
end;
end;
theorem Th25:
for A,B being non empty set for P being Permutation of A,
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;
let P be Permutation of A, Q be Permutation of B;
let f be Function of A,B;
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 thesis by A1,FUNCT_2:19;
end;
theorem Th26:
for A,B being non empty set for P being Permutation of A,
Q being Permutation of B holds (P => Q)" = P" => (Q")
proof
let A,B be non empty set;
let P be Permutation of A, Q be Permutation of B;
now
let f be Element of Funcs(A,B);
thus (P => Q)".f = Q"*f*P by Th25
.= Q"*f*P"" by FUNCT_1:43
.= (P" => (Q")).f by Def1;
end;
hence thesis;
end;
theorem Th27:
for A,B,C being non empty set, f being Function of A, Funcs(B,C),
g being Function of A,B,
P being Permutation of B, Q being Permutation of C
holds ((P => Q)*f)..(P*g) = Q*(f..g)
proof
let A,B,C be non empty set;
let f be Function of A, Funcs(B,C), g be Function of A,B, P be Permutation
of B, Q be Permutation of C;
A1: dom((P => Q)*f) = A by FUNCT_2:def 1;
A2: dom Q = C & rng(f..g) c= C by Th20,FUNCT_2:def 1;
A3: dom f = A by FUNCT_2:def 1;
a4: dom g = A by FUNCT_2:def 1;
B2: dom(f..g) = dom f /\ dom g by PRALG_1:def 19 .= A by A3,a4; then
A4: dom(Q*(f..g)) = A by A2,RELAT_1:27;
set gg = Q*(f..g);
dom (P*g) = A by FUNCT_2:def 1; then
S1: dom gg = dom ((P => Q)*f) /\ dom (P*g) by A4,A1;
for x be set st x in dom gg holds gg.x = (((P => Q)*f).x).((P*g).x)
proof
let x be set such that
a5: x in dom (Q*(f..g));
A5: x in dom((P => Q)*f) by a5,A4,A1;
reconsider fx = f.x as Function of B,C by A1,A5,FUNCT_2:5,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;
B1: x in dom (f..g) by B2,A5,A1;
thus (Q*(f..g)).x = Q.((f..g).x) by A4,A1,A5,FUNCT_1:12
.= Q.(fx.(g.x)) by B1,PRALG_1:def 19
.= (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;
end;
hence thesis by S1,PRALG_1:def 19;
end;
begin :: set valuations
definition
mode SetValuation is non-empty ManySortedSet of NAT;
end;
reserve V for SetValuation;
definition
let V;
func SetVal V -> ManySortedSet of HP-WFF means
:Def2:
it.VERUM = 1 & (for n holds it.prop n = V.n) &
for p,q holds it.(p '&' q) = [:it.p, it.q:] & it.(p =>q) = Funcs(it.p,it.q);
existence
proof
deffunc F(Element of NAT)=V.$1;
consider M being ManySortedSet of HP-WFF such that
A1: ( M.VERUM = 1 & for n holds M.prop n = F(n) )& for p,q holds M.(p
'&' q) = [:M.p,M.q:] & M.(p => q) = Funcs(M.p,M.q) from HILBERT2:sch 4;
take M;
thus thesis by A1;
end;
uniqueness
proof
let M1,M2 be ManySortedSet of HP-WFF such that
A2: M1.VERUM = 1 and
A3: for n holds M1.prop n = V.n and
A4: for p,q 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 holds M2.prop n = V.n and
A7: for p,q holds M2.(p '&' q) = [:M2.p, M2.q:] & M2.(p => q) = Funcs(
M2.p,M2.q);
defpred P[Element of HP-WFF] means M1.$1 = M2.$1;
A8: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
let r,s such that
A9: M1.r=M2.r & M1.s = M2.s;
thus M1.(r '&' s) = [:M2.r, M2.s:] by A4,A9
.= M2.(r '&' s) by A7;
thus M1.(r => s) = Funcs(M2.r,M2.s) by A4,A9
.= M2.(r => s) by A7;
end;
A10: for n holds P[prop n]
proof
let n;
thus M1.prop n = V.n by A3
.= M2.prop n by A6;
end;
A11: P[VERUM] by A2,A5;
for r holds P[r] from HILBERT2:sch 2(A11,A10,A8);
hence M1 = M2;
end;
end;
definition
let V,p;
func SetVal(V,p) -> set equals
(SetVal V).p;
correctness;
end;
registration
let V,p;
cluster SetVal(V,p) -> non empty;
coherence
proof
defpred P[Element of HP-WFF] means (SetVal V).$1 is non empty;
A1: for n holds P[prop n]
proof
let n;
(SetVal V).prop n = V.n by Def2;
hence thesis;
end;
A2: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
let r,s such that
A3: (SetVal V).r is non empty and
A4: (SetVal V).s is non empty;
(SetVal V).(r '&' s) = [:(SetVal V).r,(SetVal V).s:] by Def2;
hence (SetVal V).(r '&' s) is non empty by A3,A4;
(SetVal V).(r => s) = Funcs((SetVal V).r,(SetVal V).s) by Def2;
hence thesis by A4;
end;
A5: P[VERUM] by Def2;
for r holds P[r] from HILBERT2:sch 2(A5,A1,A2);
hence thesis;
end;
end;
theorem
SetVal(V,VERUM) = 1 by Def2;
theorem
SetVal(V,prop n) = V.n by Def2;
theorem
SetVal(V,p '&' q) = [:SetVal(V,p), SetVal(V,q):] by Def2;
theorem
SetVal(V,p => q) = Funcs(SetVal(V,p),SetVal(V,q)) by Def2;
registration
let V,p,q;
cluster SetVal(V,p => q) -> functional;
coherence
proof
let x be object;
assume x in SetVal(V,p => q);
then x in Funcs(SetVal(V,p),SetVal(V,q)) by Def2;
hence thesis;
end;
end;
registration
let V,p,q,r;
cluster -> Function-yielding for Element of SetVal(V,p => (q => r));
coherence
proof
let e be Element of SetVal(V,p => (q => r)),
x be object such that
x in dom e;
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 thesis;
end;
end;
registration
let V,p,q,r;
cluster Function-yielding for Function of SetVal(V,p => q),SetVal(V,p => r);
existence
proof
set e = the Function of SetVal(V,p => q),SetVal(V,p => r);
e is Function-yielding;
hence thesis;
end;
cluster Function-yielding for Element of SetVal(V,p => (q => r));
existence
proof
set e = the Element of SetVal(V,p => (q => r));
e is Function-yielding;
hence thesis;
end;
end;
begin :: permuting set valuations
definition
let V;
mode Permutation of V -> Function means
:Def4:
dom it = NAT & for n holds it .n is Permutation of V.n;
existence
proof
take id V;
thus dom id V = NAT by PARTFUN1:def 2;
let n;
(id V).n = id (V.n) by MSUALG_3:def 1;
hence thesis;
end;
end;
reserve P for Permutation of V;
definition
let V,P;
func Perm P -> ManySortedFunction of SetVal V, SetVal V means
:Def5:
it.VERUM = id 1 & (for n holds it.prop n = P.n) &
for p,q ex p9 being Permutation of SetVal(V,p),
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
proof
deffunc F(Element of NAT)=P.$1;
defpred I[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), q9 being Permutation of SetVal(V,$2) st p9 =
$3 & q9 = $4 & $5 = p9 => q9) & ($3 is not Permutation of SetVal(V,$1) or $4 is
not Permutation of SetVal(V,$2) implies $5 = {});
defpred C[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), q9 being Permutation of SetVal(V,$2) st p9 =
$3 & q9 = $4 & $5 = [:p9,q9:]) & ($3 is not Permutation of SetVal(V,$1) or $4
is not Permutation of SetVal(V,$2) implies $5 = {});
A1: for p,q for a,b being set ex c being set st C[p,q,a,b,c]
proof
let p,q;
let a,b be set;
per cases;
suppose that
A2: a is Permutation of SetVal(V,p) and
A3: b is Permutation of SetVal(V,q);
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:];
thus thesis;
end;
suppose
a is not Permutation of SetVal(V,p) or b is not Permutation of
SetVal(V,q);
hence thesis;
end;
end;
A4: for p,q for a,b being set ex d being set st I[p,q,a,b,d]
proof
let p,q;
let a,b be set;
per cases;
suppose that
A5: a is Permutation of SetVal(V,p) and
A6: b is Permutation of SetVal(V,q);
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;
thus thesis;
end;
suppose
a is not Permutation of SetVal(V,p) or b is not Permutation of
SetVal(V,q);
hence thesis;
end;
end;
A7: for p,q for a,b,c,d being set st I[p,q,a,b,c] & I[p,q,a,b,d] holds c = d;
A8: for p,q for a,b,c,d being set st C[p,q,a,b,c] & C[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 holds M.prop n = F(n) and
A11: for p,q holds C[p,q,M.p,M.q,M.(p '&' q)] & I[p,q,M.p,M.q,M.(p =>
q)] from HILBERT2:sch 3(A1,A4,A8,A7);
defpred P[Element of HP-WFF] means M.$1 is Permutation of (SetVal V).$1;
A12: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
let r,s such that
A13: M.r is Permutation of (SetVal V).r & M.s is Permutation of ( SetVal V).s;
A14: (SetVal V).(r '&' s) = [:SetVal(V,r),SetVal(V,s):] by Def2;
ex p9 being Permutation of SetVal(V,r), 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;
A15: (SetVal V).(r => s) = Funcs(SetVal(V,r),SetVal(V,s)) by Def2;
ex p9 being Permutation of SetVal(V,r), q9 being Permutation of
SetVal(V,s) st p9 = M.r & q9 = M.s & M.(r => s) = p9 => q9 by A11,A13;
hence thesis by A15;
end;
take M;
A16: for n holds P[prop n]
proof
let n;
M.prop n = P.n & (SetVal V).prop n = V.n by A10,Def2;
hence thesis by Def4;
end;
(SetVal V).VERUM = 1 by Def2;
then
A17: P[VERUM] by A9;
A18: for p holds P[p] from HILBERT2:sch 2(A17,A16,A12);
thus M is ManySortedFunction of SetVal V, SetVal V
proof
let p be object;
thus thesis by A18;
end;
thus M.VERUM = id 1 by A9;
thus for n holds M.prop n = P.n by A10;
let p,q;
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,q9;
thus p9 = M.p & q9 = M.q & M.(p '&' q) = [:p9,q9:] by A20,A21;
ex p9 being Permutation of SetVal(V,p), 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;
end;
uniqueness
proof
let M1,M2 be ManySortedFunction of SetVal V, SetVal V such that
A22: M1.VERUM = id 1 and
A23: for n holds M1.prop n = P.n and
A24: for p,q ex p9 being Permutation of SetVal(V,p), 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 holds M2.prop n = P.n and
A27: for p,q ex p9 being Permutation of SetVal(V,p), q9 being
Permutation of SetVal(V,q) st p9 = M2.p & q9 = M2.q & M2.(p '&' q) = [:p9,q9:]
& M2.(p => q) = p9 => q9;
defpred P[Element of HP-WFF] means M1.$1=M2.$1;
A28: for n holds P[prop n]
proof
let n;
thus M1.prop n = P.n by A23
.= M2.prop n by A26;
end;
A29: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
let r,s such that
A30: M1.r=M2.r & M1.s=M2.s;
A31: (ex p9 being Permutation of SetVal(V,r), 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), 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;
thus thesis by A30,A31;
end;
A32: P[VERUM] by A22,A25;
for r holds P[r] from HILBERT2:sch 2(A32,A28,A29);
hence M1 = M2;
end;
end;
definition
let V,P,p;
func Perm(P,p) -> Function of SetVal(V,p), SetVal(V,p) equals
(Perm P).p;
correctness;
end;
theorem Th32:
Perm(P,VERUM) = id SetVal(V,VERUM)
proof
thus Perm(P,VERUM) = id 1 by Def5
.= id SetVal(V,VERUM) by Def2;
end;
theorem
Perm(P,prop n) = P.n by Def5;
theorem Th34:
Perm(P,p '&' q) = [:Perm(P,p),Perm(P,q):]
proof
ex p9 being Permutation of SetVal(V,p), 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 thesis;
end;
theorem Th35:
for p9 being Permutation of SetVal(V,p), q9 being Permutation of
SetVal(V,q) st p9 = Perm(P,p) & q9 = Perm(P,q) holds Perm(P,p => q) = p9 => q9
proof
A1: ex p9 being Permutation of SetVal(V,p), 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), q9 be Permutation of SetVal(V,q);
assume p9 = Perm(P,p) & q9 = Perm(P,q);
hence thesis by A1;
end;
registration
let V,P,p;
cluster Perm(P,p) -> bijective;
coherence
proof
defpred P[Element of HP-WFF] means Perm(P,$1) is bijective;
A1: for n holds P[prop n]
proof
let n;
SetVal(V,prop n) = V.n & Perm(P,prop n) = P.n by Def2,Def5;
hence thesis by Def4;
end;
A2: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
let r,s;
assume Perm(P,r) is bijective;
then reconsider r9 = Perm(P,r) as Permutation of SetVal(V,r);
assume Perm(P,s) is bijective;
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,Th34;
hence Perm(P,r '&' s) is bijective;
SetVal(V,r => s) = Funcs(SetVal(V,r),SetVal(V,s)) & Perm(P,r => s) =
r9 => s9 by Def2,Th35;
hence thesis;
end;
Perm(P,VERUM) = id SetVal(V,VERUM) by Th32;
then
A3: P[VERUM];
for p holds P[p] from HILBERT2:sch 2(A3,A1,A2);
hence thesis;
end;
end;
theorem Th36:
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 g be Function of SetVal(V,p), SetVal(V,q);
thus Perm(P,p => q).g = (Perm(P,p) => Perm(P,q)).g by Th35
.= Perm(P,q)*g*Perm(P,p)" by Def1;
end;
theorem Th37:
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 g be Function of SetVal(V,p), SetVal(V,q);
thus Perm(P,p => q)".g = (Perm(P,p) => Perm(P,q))".g by Th35
.= Perm(P,q)"*g*Perm(P,p) by Th25;
end;
theorem Th38:
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 f,g be Function of SetVal(V,p), SetVal(V,q) such that
A1: f = Perm(P,p => q).g;
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,Th36;
end;
theorem Th39:
for V for P being Permutation of V for x being set st x
is_a_fixpoint_of Perm(P,p) 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 V;
let P be Permutation of V;
let x be set such that
A1: x is_a_fixpoint_of Perm(P,p);
let f be Function such that
A2: f is_a_fixpoint_of Perm(P,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 reconsider g = f as Function of SetVal(V,p), SetVal(V,q)
by A2,FUNCT_2:66;
set h = Perm(P,p => q).f;
h = Perm(P,q)*g*Perm(P,p)" by Th36;
then reconsider h as Function of SetVal(V,p), SetVal(V,q);
A3: h = f by A2;
A4: x in SetVal(V,p) by A1,FUNCT_2:52;
dom Perm(P,p => q) = SetVal(V,p => q) by FUNCT_2:52
.= Funcs(SetVal(V,p),SetVal(V,q)) by Def2;
then f.x in SetVal(V,q) by A4,Th4,A2;
hence f.x in dom Perm(P,q) by FUNCT_2:52;
thus Perm(P,q).(f.x) = (Perm(P,q)*g).x by A4,FUNCT_2:15
.= (f*Perm(P,p)).x by A3,Th38
.= f.(Perm(P,p).x) by A4,FUNCT_2:15
.= f.x by A1;
end;
begin :: canonical formulae
definition
let p;
attr p is canonical means
for V ex x being set st for P being Permutation of V holds
x is_a_fixpoint_of Perm(P,p);
end;
registration
cluster VERUM -> canonical;
coherence
proof
let V;
take 0;
let P be Permutation of V;
SetVal(V,VERUM) = 1 & 0 in 1 by Def2,CARD_1:49,TARSKI:def 1;
hence thesis by Th3,CARD_1:49;
end;
end;
registration
let p,q;
cluster p => (q => p) -> canonical;
coherence
proof
let V;
deffunc F(set)=SetVal(V,q) --> $1;
A1: for x being Element of SetVal(V,p) holds F(x) in SetVal(V,q => p)
proof
let x be Element of SetVal(V,p);
SetVal(V,q) --> x in Funcs(SetVal(V,q),SetVal(V,p)) by FUNCT_2:8;
hence thesis by Def2;
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 = F(x) from FUNCT_2:sch 8(A1);
take f;
let P be Permutation of V;
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;
now
let x be Element of SetVal(V,p);
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)
.= (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 Th36
.= (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;
end;
hence f = Perm(P,q => p)*f*Perm(P,p)"
.= Perm(P,p => (q => p)).f by Th36;
end;
cluster (p '&' q) => p -> canonical;
coherence
proof
let V;
take f = pr1(SetVal(V,p),SetVal(V,q));
let P be Permutation of V;
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;
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 Th36
.= Perm(P,p)*F*[:Perm(P,p),Perm(P,q):]" by Th34
.= 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 Th15
.= 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;
end;
cluster (p '&' q) => q -> canonical;
coherence
proof
let V;
take f = pr2(SetVal(V,p),SetVal(V,q));
let P be Permutation of V;
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;
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 Th36
.= Perm(P,q)*F*[:Perm(P,p),Perm(P,q):]" by Th34
.= 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 Th16
.= 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;
end;
cluster p => (q => (p '&' q)) -> canonical;
coherence
proof
let V;
take f = curry [:id SetVal(V,p),id SetVal(V,q):];
let P be Permutation of V;
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;
A7: now
let x be Element of SetVal(V,p);
set fx = f.x;
reconsider fx as Function of SetVal(V,q), SetVal(V,p '&' q) by Def2;
set Fx = F.(Perm(P,p)".x);
Fx in SetVal(V,q => (p '&' q));
then Fx in Funcs(SetVal(V,q),SetVal(V,p '&' q)) by Def2;
then reconsider Fx as Function of SetVal(V,q), SetVal(V,p '&' q) by
FUNCT_2:66;
now
let y be Element of SetVal(V,q);
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 Th34
.= Perm(P,p '&' q).[Perm(P,p)".x,(id SetVal(V,q)).(Perm(P,q)".y)]
.= Perm(P,p '&' q). [(id SetVal(V,p)).(Perm(P,p)".x),(id SetVal(V,q)
).(Perm(P,q)".y)]
.= 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;
end;
hence f.x = Perm(P,p '&' q)*Fx*Perm(P,q)"
.= Perm(P,q => (p '&' q)).(F.(Perm(P,p)".x)) by Th36
.= (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;
end;
thus Perm(P,p => (q => (p '&' q))).f = Perm(P,q => (p '&' q))*F*Perm(P,p)"
by Th36
.= f by A7;
end;
end;
registration
let p,q,r;
cluster (p => (q => r)) => ((p => q) => (p => r)) -> canonical;
coherence
proof
deffunc G(Function-yielding Function)=Frege $1;
let V;
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 G(x) in SetVal(V,(p
=> q) => (p => r))
proof
let x be Element of SetVal(V,p => (q => 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,Th23;
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;
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 = G(x) from
FUNCT_2:sch 8(A2);
take F;
let P be Permutation of V;
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;
now
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));
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;
Yf = Perm(P,q => r)"*ff*Perm(P,p) by Th37;
then reconsider
h = Frege Yf as Function-yielding Function of SetVal(V,p => q),
SetVal(V,p => r) by A1,A4,Th23;
set M = Perm(P,p => r)*h*Perm(P,p => q)";
A5: product doms ff = product(SetVal(V,p) --> SetVal(V,q)) by A4,Th5
.= 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 as ManySortedFunction of product doms f;
A7: for g be Function st g in product doms f holds M.g = f..g
proof
Yf in SetVal(V,p => (q => r));
then Yf in Funcs(SetVal(V,p),SetVal(V,q => r)) by Def2;
then Yf is Function of SetVal(V,p), Funcs(SetVal(V,q),SetVal(V,r)) by A4,
FUNCT_2:66;
then
A8: product doms Yf = product(SetVal(V,p) --> SetVal(V,q)) by Th5
.= 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 such that
A9: g in product doms f;
reconsider G = g as Function of SetVal(V,p),SetVal(V,q) by A5,A9,
FUNCT_2:66;
L: dom FF = SetVal(V,p) by FUNCT_2:def 1;
L2: dom G = SetVal(V,p) by FUNCT_2:def 1;
A10: dom(FF..G) = dom FF /\ dom G by PRALG_1:def 19
.= SetVal(V,p) by L2,L;
A11: rng(FF..G) c= SetVal(V,r) by Th20;
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 Yf by A8,Def2; then
A14: Perm(P,p => q)".G in SetVal(V,p => q) by A8,Th37;
B2: rng G c= SetVal(V,q) by RELAT_1:def 19;
dom (Perm(P,q)") = SetVal(V,q) by FUNCT_2:def 1; then
dom (Perm(P,q)"*g) = dom g by RELAT_1:27,B2
.= SetVal(V,p) by L2; then
BB: dom (X*FF) = dom (Perm(P,q)"*g) by FUNCT_2:def 1;
A15: X = (Perm(P,q) => Perm(P,r))" by Th35
.= Perm(P,q)" => (Perm(P,r)") by Th26;
A16: h.(Perm(P,p => q)".g) = h.(Perm(P,q)"*G*Perm(P,p)) by Th37
.= Yf..(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 Th37
.= (X*FF)..(Perm(P,q)"*g)*Perm(P,p) by Th18,BB
.= (Perm(P,r)"*(FF..G))*Perm(P,p) by A15,Th27
.= Perm(P,p => r)".GG by Th37;
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;
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 Th36
.= 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;
end;
hence F = Perm(P,(p => q) => (p => r))*F*Perm(P,p => (q => r))"
.= Perm(P,(p => (q => r)) => ((p => q) => (p => r))).F by Th36;
end;
end;
theorem Th40:
p is canonical & p => q is canonical implies q is canonical
proof
assume that
A1: p is canonical and
A2: p => q is canonical;
let V;
consider x being set such that
A3: for P being Permutation of V holds x is_a_fixpoint_of Perm(P,p) by A1;
set P = the Permutation of V;
A4: dom Perm(P,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;
f is_a_fixpoint_of Perm(P,p => q) by A5;
then reconsider f as Function of SetVal(V,p), SetVal(V,q) by FUNCT_2:66,A4;
take f.x;
let P be Permutation of V;
A6: f is_a_fixpoint_of Perm(P,p => q) by A5;
x is_a_fixpoint_of Perm(P,p) by A3;
hence thesis by A6,Th39;
end;
theorem
p in HP_TAUT implies p is canonical
proof
set X = {q: q is canonical};
X c= HP-WFF
proof
let x be object;
assume x in X;
then ex p st p = x & p is canonical;
hence thesis;
end;
then reconsider X as Subset of HP-WFF;
X is Hilbert_theory
proof
thus VERUM in X;
let p,q,r;
thus p => (q => p) in X;
thus (p => (q => r)) => ((p => q) => (p => r)) in X;
thus (p '&' q) => p in X;
thus (p '&' q) => q in X;
thus p => (q => (p '&' q)) in X;
assume p in X;
then
A1: ex s st s = p & s is canonical;
assume p => q in X;
then ex s st s = p => q & s is canonical;
then q is canonical by A1,Th40;
hence thesis;
end;
then
A2: HP_TAUT c= X by HILBERT1:13;
assume p in HP_TAUT;
then p in X by A2;
then ex q st p = q & q is canonical;
hence thesis;
end;
registration
cluster canonical for Element of HP-WFF;
existence
proof
take VERUM;
thus thesis;
end;
end;
begin :: pseudo-canonical formulae
definition
let p;
attr p is pseudo-canonical means
for V for P being Permutation of V
ex x being set st x is_a_fixpoint_of Perm(P,p);
end;
registration
cluster canonical -> pseudo-canonical for Element of HP-WFF;
coherence
proof
let p;
assume
A1: p is canonical;
let V;
consider x being set such that
A2: for P being Permutation of V holds x is_a_fixpoint_of Perm(P,p) by A1;
let P be Permutation of V;
take x;
thus thesis by A2;
end;
end;
theorem
p is pseudo-canonical & p => q is pseudo-canonical implies
q is pseudo-canonical
proof
assume that
A1: p is pseudo-canonical and
A2: p => q is pseudo-canonical;
let V;
let P be Permutation of V;
consider x being set such that
A3: x is_a_fixpoint_of Perm(P,p) by A1;
consider f being set such that
A4: f is_a_fixpoint_of Perm(P,p => q) by A2;
dom Perm(P,p => q) = SetVal(V,p => q) by FUNCT_2:52
.= Funcs(SetVal(V,p),SetVal(V,q)) by Def2;
then reconsider f as Function of SetVal(V,p), SetVal(V,q) by FUNCT_2:66,A4;
take f.x;
thus thesis by A3,A4,Th39;
end;
theorem Th43:
for p,q for V for P being Permutation of V st (ex f being set st
f is_a_fixpoint_of Perm(P,p)) & not (ex f being set st f is_a_fixpoint_of Perm(
P,q)) holds p => q is not pseudo-canonical
proof
let p,q;
let V;
let P be Permutation of V;
given x being set such that
A1: x is_a_fixpoint_of Perm(P,p);
assume
A2: for x being set holds not x is_a_fixpoint_of Perm(P,q);
assume p => q is pseudo-canonical;
then consider f being set such that
A3: f is_a_fixpoint_of Perm(P,p => q);
reconsider f as Function by A3;
f.x is_a_fixpoint_of Perm(P,q) by A1,A3,Th39;
hence contradiction by A2;
end;
theorem
for a, b being Element of NAT st a <> b holds
(prop a) => (prop b) => (prop a) => (prop a) is non pseudo-canonical
proof
let a, b be Element of NAT such that
A1: a <> b;
set A = { (0,1) -->(i,j) where i,j is Element of INT: i < j or i is even & i
= j}, X = product ((0,1) --> (INT,INT));
A c= X
proof
let x be object;
assume x in A;
then ex i,j being Element of INT st x = (0,1) -->(i,j) &( i < j or i is
even & i = j);
hence thesis by Th10;
end;
then reconsider A as Subset of X;
set p1 = (0,1) --> (1,0);
A2: not b in dom(a .--> 2) by A1,FUNCOP_1:75;
reconsider p1 as Permutation of 2 by Th14;
defpred P[set,set] means ex i being Integer st $1 = i & $2 = i+1;
set V = (NAT --> INT) +* (a .--> Segm 2);
reconsider V 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 holds ex u being Element of INT st P[e,u]
proof
let e be Element of INT;
reconsider e as Integer;
reconsider u = e+1 as Element of INT by INT_1:def 2;
take u;
thus thesis;
end;
consider p0 being Function of INT, INT such that
A6: for e being Element of INT holds P[e,p0.e] from FUNCT_2:sch 3(A5);
A7: dom p0 = INT by FUNCT_2:def 1;
for y being object holds y in INT iff
ex x being object st x in dom p0 & y = p0.x
proof
let y be object;
hereby
assume y in INT;
then reconsider i = y as Integer;
reconsider x = i-1 as object;
take x;
thus x in dom p0 by A7,INT_1:def 2;
then ex j being Integer st x = j & p0.x = j+1 by A6,A7;
hence y = p0.x by XCMPLX_1:27;
end;
given x being object such that
A8: x in dom p0 and
A9: y = p0.x;
ex i being Integer st x = i & p0.x = i + 1 by A6,A7,A8;
hence thesis by A9,INT_1:def 2;
end;
then
A10: rng p0 = INT by FUNCT_1:def 3;
A11: p0 is one-to-one
proof
let x1,x2 be object;
assume x1 in dom p0 & x2 in dom p0;
then reconsider I1 = x1, I2 = x2 as Element of INT by FUNCT_2:def 1;
assume
A12: p0.x1 = p0.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 thesis by A12,XCMPLX_1:2;
end;
A13: SetVal(V,prop b) = V.b by Def2
.= (NAT --> INT).b by A2,FUNCT_4:11
.= INT;
A14: X = 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,X) 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 as Permutation of INT by A11,A10,FUNCT_2:57;
set P = (NAT --> p0) +* (a .--> p1);
A16: dom P = dom(NAT --> p0) \/ dom(a .--> p1) by FUNCT_4:def 1
.= dom(NAT --> p0) \/ {a}
.= NAT \/ {a}
.= NAT by ZFMISC_1:40;
for n holds P.n is Permutation of V.n
proof
let n;
per cases;
suppose
A17: n = a;
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 P.n = (a .--> p1).a by A17,FUNCT_4:13
.= p1 by FUNCOP_1:72;
hence thesis by A18;
end;
suppose
A19: n <> a;
then not n in dom(a .--> 2) by FUNCOP_1:75;
then
A20: V.n = (NAT --> INT).n by FUNCT_4:11
.= INT;
not n in dom(a .--> p1) by A19,FUNCOP_1:75;
then P.n = (NAT --> p0).n by FUNCT_4:11
.= p0;
hence thesis by A20;
end;
end;
then reconsider P 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 Q by FUNCT_2:def 1;
rng(Perm(P,(prop a) => prop b)") = dom(Perm(P,(prop a) => prop b)"")
by FUNCT_1:32
.= X 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
.= X by A14,FUNCT_2:def 3
.= dom chi(A`,X) by FUNCT_3:def 3;
for x being object st x in dom chi(A`,X) holds (f*Perm(P,(prop a) =>
prop b)").x = chi(A`,X).x
proof
A24: dom(p0") = INT by A10,FUNCT_1:32;
let x be object;
A25: not b in dom(a .--> p1) by A1,FUNCOP_1:75;
assume
A26: x in dom chi(A`,X);
then x in X 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,Th11;
reconsider i0, 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;
then
A32: Perm(P,prop b)"*g = (0,1) --> (p0".i0,p0".j0) by A27,A24,Th13
.= (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 Th37
.= f.((0,1) --> (j0-1,i0-1)) by A21,A32,Th12;
per cases;
suppose
A34: x in A;
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,Th9;
A38: now
assume (0,1) --> (j0-1,i0-1) in A;
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,Th9;
per cases by A40;
suppose i < j;
hence contradiction by A36,A37,A41,XREAL_1:9;
end;
suppose i is even & i = j;
hence contradiction by A36,A37,A41,XCMPLX_1:19;
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 X by Th10;
then (0,1) --> (j0-1,i0-1) in X \ A by A38,XBOOLE_0:def 5;
hence (f*Perm(P,(prop a) => prop b)").x = 0 by A33,FUNCT_3:37
.= chi(A`,X).x by A42,FUNCT_3:37;
end;
suppose
A43: not x in A;
x in X by A27,Th10;
then
A44: x in X \ 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
per cases by A48,A46,XXREAL_0:1;
suppose i0 > j0;
then j0-1 < i0-1 by XREAL_1:9;
hence (0,1) --> (j0-1,i0-1) in A by A45,A47;
end;
suppose i0 = j0 & i0 is odd;
hence (0,1) --> (j0-1,i0-1) in A by A45;
end;
end;
hence (f*Perm(P,(prop a) => prop b)").x = 1 by A33,FUNCT_3:def 3
.= chi(A`,X).x by A44,FUNCT_3:def 3;
end;
end;
then f*Perm(P,(prop a) => prop b)" = chi(A`,X) by A23;
hence f = Perm(P,prop a)*(f*Perm(P,(prop a) => prop b)") by A21,Th8
.= Perm(P,prop a)*f*Perm(P,(prop a) => prop b)" by RELAT_1:36
.= Q.f by Th36;
end;
for x being set holds not x is_a_fixpoint_of Perm(P,prop a)
proof
let x be set;
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);
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 thesis by A21,FUNCT_4:63;
end;
hence thesis by A22,Th43;
end;