:: Mostowski's Fundamental Operations - Part I
:: by Andrzej Kondracki
::
:: Received December 17, 1990
:: Copyright (c) 1990-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 CLASSES2, SUBSET_1, ZF_REFLE, ORDINAL1, FINSET_1, FUNCT_1,
XBOOLE_0, ZF_LANG, NUMBERS, VALUED_1, RELAT_1, TARSKI, ZFMISC_1, MCART_1,
CARD_1, XXREAL_0, NAT_1, ARYTM_3, ZF_MODEL, FUNCT_2, ORDINAL4, FUNCOP_1,
XBOOLEAN, BVFUNC_2, ZF_FUND1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, DOMAIN_1, ORDINAL1,
NUMBERS, XCMPLX_0, NAT_1, ORDINAL4, CARD_1, FINSET_1, RELAT_1, CLASSES2,
ZF_REFLE, ZF_LANG, ZF_MODEL, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
MCART_1, FUNCOP_1, XXREAL_0;
constructors PARTFUN1, WELLORD2, DOMAIN_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1,
CLASSES1, ORDINAL4, ZF_MODEL, RELSET_1, NUMBERS;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0, CARD_1,
CLASSES2, ZF_LANG, ZF_LANG1, RELAT_1, XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, RELAT_1;
equalities TARSKI, XBOOLE_0, ORDINAL1, ORDINAL4;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, ORDINAL1, ORDINAL3, CARD_1, CLASSES2, ZFMISC_1, ZF_LANG,
ZF_LANG1, ZF_MODEL, ENUMSET1, FUNCT_1, FUNCT_2, FUNCT_5, RELAT_1,
FINSET_1, GRFUNC_1, NAT_1, FUNCOP_1, WELLORD2, CLASSES1, RELSET_1,
XBOOLE_0, XBOOLE_1, XCMPLX_1, XTUPLE_0;
schemes FUNCT_1, FUNCT_2, ORDINAL1, FINSET_1, ZF_LANG1, BINOP_2, XBOOLE_0;
begin
reserve V for Universe,
a,b,x,y,z,x9,y9 for Element of V,
X for Subclass of V,
o,p,q,r,s,t,u,a1,a2,a3,A,B,C,D for set,
K,L,M for Ordinal,
n for Element of omega,
fs for finite Subset of omega,
e,g,h for Function,
E for non empty set,
f for Function of VAR,E,
k,k1 for Element of NAT,
v1,v2,v3 for Element of VAR,
H,H9 for ZF-formula;
registration let V;
cluster Relation-like for Element of V;
existence
proof set u = the Element of V;
take [:u,u:];
thus thesis;
end;
end;
definition
::$CD
let V,x,y;
redefine func x(#)y -> Relation-like Element of V; :: redefines (#) (RELAT_1, definition)
coherence
proof
set Z=x(#)y;
defpred PAIR[object] means ex p,r being object st $1=[p,r];
A1: now
consider B such that
A2: for o being object holds o in B iff o in y & PAIR[o]
from XBOOLE_0:sch 1;
for o being object holds o in B implies o in y by A2;
then B c= y;
then
A3: B in V by CLASSES1:def 1;
consider A such that
A4: for o being object holds o in A iff o in x & PAIR[o]
from XBOOLE_0:sch 1;
ex g st dom g = [:A,B:] & Z c= rng g
proof
deffunc G(object) = [$1`1`1,$1`2`2];
consider g such that
A5: dom g=[:A,B:] & for o being object st o in [:A,B:] holds g.o=G(o) from
FUNCT_1:sch 3;
take g;
thus dom g=[:A,B:] by A5;
thus Z c= rng g
proof
let p,r be object;
assume [p,r] in Z;
then consider q being object such that
A6: [p,q] in x & [q,r] in y by RELAT_1:def 8;
set s=[[p,q],[q,r]];
[p,q] in A & [q,r] in B by A4,A2,A6;
then
A7: s in [:A,B:] by ZFMISC_1:def 2;
then g.s=[s`1`1,s`2`2] by A5
.=[[p,q]`1,s`2`2]
.=[[p,q]`1,[q,r]`2]
.=[p,[q,r]`2]
.=[p,r];
hence thesis by A5,A7,FUNCT_1:def 3;
end;
end;
then
A8: card Z c= card [:A,B:] by CARD_1:12;
for o being object holds o in A implies o in x by A4;
then A c= x;
then A in V by CLASSES1:def 1;
then [:A,B:] in V by A3,CLASSES2:61;
then card [:A,B:] in card V by CLASSES2:1;
hence card Z in card V by A8,ORDINAL1:12;
end;
Z c= V
proof
let q,s be object;
assume [q,s] in Z;
then consider r being object such that
A9: [q,r] in x and
A10: [r,s] in y by RELAT_1:def 8;
y c= V by ORDINAL1:def 2;
then {{r,s},{r}} c= V by A10,ORDINAL1:def 2;
then {r,s} in V by ZFMISC_1:32;
then {r,s} c= V by ORDINAL1:def 2;
then
A11: s in V by ZFMISC_1:32;
x c= V by ORDINAL1:def 2;
then {{q,r},{q}} c= V by A9,ORDINAL1:def 2;
then {q} in V by ZFMISC_1:32;
then {q} c= V by ORDINAL1:def 2;
then q in V by ZFMISC_1:31;
hence thesis by A11,CLASSES2:58;
end;
hence thesis by A1,CLASSES1:1;
end;
end;
definition
func decode -> Function of omega,VAR means
:Def1:
for p being Element of omega holds it.p = x.card p;
existence
proof
deffunc F(Element of omega) = x.card $1;
thus ex f being Function of omega, VAR st for x being Element of omega
holds f.x = F(x) from FUNCT_2:sch 4;
end;
uniqueness
proof
deffunc F(Element of omega) = x.card $1;
thus for f1,f2 being Function of omega,VAR st (for x being Element of
omega holds f1.x = F(x)) & (for x being Element of omega holds f2.x = F(x))
holds f1 = f2 from BINOP_2:sch 1;
end;
end;
definition
let v1;
func x".v1 -> Element of NAT means
:Def2:
x.it=v1;
existence
proof
v1 in VAR;
then consider k such that
A1: v1=k and
A2: k>=5 by ZF_LANG:def 1;
consider m being Nat such that
A3: k=5+m by A2,NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
take m;
thus thesis by A1,A3,ZF_LANG:def 2;
end;
uniqueness
proof
let k,k9 be Element of NAT;
assume x.k=v1 & x.k9=v1;
then 5+k=v1 & 5+k9=v1 by ZF_LANG:def 2;
hence thesis by XCMPLX_1:2;
end;
end;
Lm1: dom decode = omega & rng decode = VAR & decode is one-to-one & decode" is
one-to-one & dom(decode") = VAR & rng(decode") = omega
proof
thus
A1: dom decode = omega by FUNCT_2:def 1;
now
let p be object;
now
assume p in VAR;
then reconsider p9=p as Element of VAR;
reconsider q= x".p9 as object;
take q;
thus q in dom decode by A1;
thus decode.q=x.card (x".p9) by Def1
.=x.(x".p9)
.=p by Def2;
end;
hence p in VAR iff
ex q being object st q in dom decode & p=decode.q by FUNCT_2:5;
end;
hence
A2: rng decode = VAR by FUNCT_1:def 3;
now
let p,q be object;
assume that
A3: p in dom decode & q in dom decode and
A4: decode.p=decode.q;
reconsider p9=p, q9=q as Element of omega by A3;
x.card p9 = decode.q by A4,Def1
.= x.card q9 by Def1;
then
A5: 5+card p9 = x.card q9 by ZF_LANG:def 2
.= 5+card q9 by ZF_LANG:def 2;
consider k such that
A6: p9= k;
consider k1 such that
A7: q9= k1;
k=card p9 by A6
.=card k1 by A5,A7,XCMPLX_1:2
.=k1;
hence p=q by A6,A7;
end;
hence
A8: decode is one-to-one by FUNCT_1:def 4;
hence decode" is one-to-one;
thus thesis by A1,A2,A8,FUNCT_1:33;
end;
definition
let A be Subset of VAR;
func code A -> Subset of omega equals
(decode").:A;
coherence by Lm1,RELAT_1:111;
end;
registration
let A be finite Subset of VAR;
cluster code A -> finite;
coherence;
end;
definition
let H,E;
func Diagram(H,E) -> set means
:Def4:
p in it iff ex f st p=(f*decode)|code Free(H) & f in St(H,E);
existence
proof
defpred P[object] means ex f st $1=(f*decode)|code Free(H) & f in St(H,E);
consider B such that
A1: for p being object holds p in B iff p in Funcs(code Free(H),E) & P[p]
from XBOOLE_0:sch 1;
take B;
p in B iff ex f st p=(f*decode)|code Free(H) & f in St(H,E)
proof
now
given f such that
A2: p=(f*decode)|code Free(H) and
A3: f in St(H,E);
dom (f*decode)=omega by FUNCT_2:def 1;
then dom((f*decode)|code Free(H))=omega /\ code Free(H) by RELAT_1:61;
then
A4: dom((f*decode)|code Free(H))=code Free(H) by XBOOLE_1:28;
rng((f*decode)|code Free(H)) c= E;
then p in Funcs(code Free(H),E) by A2,A4,FUNCT_2:def 2;
hence p in B by A1,A2,A3;
end;
hence thesis by A1;
end;
hence thesis;
end;
uniqueness
proof
let B,C such that
A5: p in B iff ex f st p=(f*decode)|code Free(H) & f in St(H,E) and
A6: p in C iff ex f st p=(f*decode)|code Free(H) & f in St(H,E);
thus B c= C
proof
let p be object;
assume p in B;
then ex f st p=(f*decode)|code Free(H) & f in St(H,E) by A5;
hence thesis by A6;
end;
let p be object;
assume p in C;
then ex f st p=(f*decode)|code Free(H) & f in St(H,E) by A6;
hence thesis by A5;
end;
end;
definition
let V,X;
attr X is closed_wrt_A1 means
for a st a in X holds {{[0-element_of(V
),x],[1-element_of(V),y]}: x in y & x in a & y in a} in X;
attr X is closed_wrt_A2 means
for a,b st a in X & b in X holds {a,b} in X;
attr X is closed_wrt_A3 means
for a st a in X holds union a in X;
attr X is closed_wrt_A4 means
for a,b st a in X & b in X holds {{[x,y ]}: x in a & y in b} in X;
attr X is closed_wrt_A5 means
for a,b st a in X & b in X holds {x \/ y: x in a & y in b} in X;
attr X is closed_wrt_A6 means
for a,b st a in X & b in X holds {x\y: x in a & y in b} in X;
attr X is closed_wrt_A7 means
for a,b st a in X & b in X holds {x(#) y: x in a & y in b} in X;
end;
definition
let V,X;
attr X is closed_wrt_A1-A7 means
X is closed_wrt_A1 closed_wrt_A2
closed_wrt_A3 closed_wrt_A4 closed_wrt_A5 closed_wrt_A6 closed_wrt_A7;
end;
Lm2: for A being Element of omega holds A = x".x.card A
by Def2;
Lm3: dom((f*decode)|fs)=fs & rng((f*decode)|fs) c= E & (f*decode)|fs in Funcs(
fs,E) & dom(f*decode)=omega
proof
dom(f*decode)=omega by FUNCT_2:def 1;
hence
A1: dom((f*decode)|fs)=fs by RELAT_1:62;
thus rng((f*decode)|fs) c= E;
hence (f*decode)|fs in Funcs(fs,E) by A1,FUNCT_2:def 2;
thus thesis by FUNCT_2:def 1;
end;
Lm4: decode.(x".v1)=v1 & (decode").v1= x".v1 & (f*decode).( x".v1)=f.v1
proof
thus
A1: decode.( x".v1)=x.card ( x".v1) by Def1
.=x.x".v1
.=v1 by Def2;
hence decode".v1= x".v1 by Lm1,FUNCT_1:34;
x".v1 in omega;
then x".v1 in dom(f*decode) by Lm3;
hence thesis by A1,FUNCT_1:12;
end;
Lm5: for A being finite Subset of VAR holds p in code A iff ex v1 st v1 in A &
p= x".v1
proof
let A be finite Subset of VAR;
A1: p in code A iff
ex q being object st q in dom(decode") & q in A & p=(decode").q by
FUNCT_1:def 6;
thus p in code A implies ex v1 st v1 in A & p= x".v1
proof
assume
A2: p in code A;
then reconsider p9 = p as Element of omega;
consider q such that
A3: q in A and
q in dom(decode") and
A4: p=(decode").q by A1,A2;
reconsider q as Element of VAR by A3;
take q;
q=decode.p by A4,Lm1,FUNCT_1:35
.=x.card p9 by Def1;
hence thesis by A3,Lm2;
end;
given v1 such that
A5: v1 in A and
A6: p= x".v1;
p=decode".v1 by A6,Lm4;
hence thesis by A5,Lm1,FUNCT_1:def 6;
end;
Lm6: code {v1} = {x".v1}
proof
thus code {v1} c= { x".v1}
proof
let p be object;
assume p in code {v1};
then consider v2 such that
A1: v2 in {v1} and
A2: p= x".v2 by Lm5;
v2=v1 by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
let p be object;
assume p in { x".v1};
then
A3: p= x".v1 by TARSKI:def 1;
v1 in {v1} by TARSKI:def 1;
hence thesis by A3,Lm5;
end;
Lm7: code {v1,v2} = {x".v1, x".v2}
proof
thus code {v1,v2} c= { x".v1, x".v2}
proof
let p be object;
assume p in code {v1,v2};
then ex v3 st v3 in {v1,v2} & p= x".v3 by Lm5;
then p= x".v1 or p= x".v2 by TARSKI:def 2;
hence thesis by TARSKI:def 2;
end;
let p be object such that
A1: p in { x".v1, x".v2};
now
per cases by A1,TARSKI:def 2;
suppose
A2: p= x".v1;
v1 in {v1,v2} by TARSKI:def 2;
hence thesis by A2,Lm5;
end;
suppose
A3: p= x".v2;
v2 in {v1,v2} by TARSKI:def 2;
hence thesis by A3,Lm5;
end;
end;
hence thesis;
end;
Lm8: for A being finite Subset of VAR holds A,code A are_equipotent
proof
let A be finite Subset of VAR;
A1: (decode")|A is one-to-one & rng((decode")|A)=code A by Lm1,FUNCT_1:52
,RELAT_1:115;
dom((decode")|A)=dom(decode") /\ A by RELAT_1:61
.=A by Lm1,XBOOLE_1:28;
hence thesis by A1,WELLORD2:def 4;
end;
Lm9: v1 in Free H implies ((f*decode)|code Free H).( x".v1)=f.v1
proof
assume v1 in Free H;
then
A1: x".v1 in code Free H by Lm5;
dom((f*decode)|code Free H)=code Free H by Lm3;
hence ((f*decode)|code Free H).( x".v1)=(f*decode).( x".v1) by A1,FUNCT_1:47
.=f.v1 by Lm4;
end;
Lm10: for f,g being Function of VAR,E st (f*decode)|code Free H=(g*decode)|
code Free H & f in St(H,E) holds g in St(H,E)
proof
let f,g be Function of VAR,E such that
A1: (f*decode)|code Free H=(g*decode)|code Free H and
A2: f in St(H,E);
A3: for v1 st v1 in Free H holds f.v1=g.v1
proof
let v1;
assume
A4: v1 in Free H;
hence f.v1=((g*decode)|code Free H).( x".v1) by A1,Lm9
.=g.v1 by A4,Lm9;
end;
E,f |= H by A2,ZF_MODEL:def 4;
then E,g |= H by A3,ZF_LANG1:75;
hence thesis by ZF_MODEL:def 4;
end;
Lm11: p in Funcs(fs,E) implies ex f st p=(f*decode)|fs
proof
set ElofE = the Element of E;
deffunc G(object) = ElofE;
assume p in Funcs(fs,E);
then
A1: ex e st e=p & dom e=fs & rng e c= E by FUNCT_2:def 2;
then reconsider g=p as Function of fs,E by FUNCT_2:def 1,RELSET_1:4;
deffunc F(object) = g.$1;
defpred C[object] means $1 in dom g;
A2: now
let q be object such that
q in omega;
now
assume q in dom g;
then g.q in rng g by FUNCT_1:def 3;
hence g.q in E;
end;
hence (C[q] implies F(q) in E) & (not C[q] implies G(q) in E);
end;
consider h being Function of omega,E such that
A3: for q being object st q in omega
holds (C[q] implies h.q=F(q)) & (not C[q]
implies h.q=G(q)) from FUNCT_2:sch 5(A2);
decode" is Function of VAR,omega by Lm1,FUNCT_2:def 1,RELSET_1:4;
then reconsider f=h*(decode") as Function of VAR,E by FUNCT_2:13;
take f;
A4: dom h = omega by FUNCT_2:def 1;
then
A5: dom g = dom h /\ fs by A1,XBOOLE_1:28;
A6: for p being object st p in dom g holds h.p=g.p by A1,A3;
h=h*(id dom decode) by A4,Lm1,RELAT_1:51
.=h*(decode"*decode) by Lm1,FUNCT_1:39
.=f*decode by RELAT_1:36;
hence thesis by A5,A6,FUNCT_1:46;
end;
theorem Th1:
X c= V & (o in X implies o is Element of V) & (o in A & A in X
implies o is Element of V)
proof
thus X c= V & (o in X implies o is Element of V);
assume that
A1: o in A and
A2: A in X;
A c= V by A2,ORDINAL1:def 2;
hence thesis by A1;
end;
theorem Th2:
X is closed_wrt_A1-A7 implies (o in X iff {o} in X) & (A in X
implies union A in X)
proof
assume
A1: X is closed_wrt_A1-A7;
then
A2: X is closed_wrt_A2;
A3: now
assume o in X;
then {o,o} in X by A2;
hence {o} in X by ENUMSET1:29;
end;
A4: X is closed_wrt_A3 by A1;
now
assume {o} in X;
then union {o} in X by A4;
hence o in X by ZFMISC_1:25;
end;
hence o in X iff {o} in X by A3;
assume A in X;
hence thesis by A4;
end;
theorem Th3:
X is closed_wrt_A1-A7 implies {} in X
proof
set o = the Element of X;
reconsider p=o as Element of V;
set D={{[0-element_of(V),x],[1-element_of(V),y]}: x in y & x in {p} & y in {
p}};
A1: now
set q = the Element of D;
assume D <> {};
then q in D;
then consider x,y such that
q={[0-element_of(V),x],[1-element_of(V),y]} and
A2: x in y and
A3: x in {p} & y in {p};
x=p & y=p by A3,TARSKI:def 1;
hence contradiction by A2;
end;
assume X is closed_wrt_A1-A7;
then {p} in X & X is closed_wrt_A1 by Th2;
hence thesis by A1;
end;
theorem Th4:
X is closed_wrt_A1-A7 & A in X & B in X implies A \/ B in X & A\B
in X & A(#)B in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: A in X and
A3: B in X;
reconsider b=B as Element of V by A3;
reconsider a=A as Element of V by A2;
A4: {a} in X & {b} in X by A1,A2,A3,Th2;
set D={x \/ y: x in {a} & y in {b}};
A5: now
let o be object;
A6: now
assume o in D;
then consider x,y such that
A7: o=x \/ y and
A8: x in {a} and
A9: y in {b};
x=a by A8,TARSKI:def 1;
hence o=a \/ b by A7,A9,TARSKI:def 1;
end;
now
A10: a in {a} & b in {b} by TARSKI:def 1;
assume o=a \/ b;
hence o in D by A10;
end;
hence o in D iff o=a \/ b by A6;
end;
X is closed_wrt_A5 by A1;
then D in X by A4;
then {a \/ b} in X by A5,TARSKI:def 1;
hence A \/ B in X by A1,Th2;
set D={x\y: x in {a} & y in {b}};
A11: now
let o be object;
A12: now
assume o in D;
then consider x,y such that
A13: o=x\y and
A14: x in {a} and
A15: y in {b};
x=a by A14,TARSKI:def 1;
hence o=a\b by A13,A15,TARSKI:def 1;
end;
now
A16: a in {a} & b in {b} by TARSKI:def 1;
assume o=a\b;
hence o in D by A16;
end;
hence o in D iff o=a\b by A12;
end;
X is closed_wrt_A6 by A1;
then D in X by A4;
then {a\b} in X by A11,TARSKI:def 1;
hence A\B in X by A1,Th2;
set D={x(#)y: x in {a} & y in {b}};
A17: now
let o be object;
A18: now
assume o in D;
then consider x,y such that
A19: o=x(#)y and
A20: x in {a} and
A21: y in {b};
x=a by A20,TARSKI:def 1;
hence o=a(#)b by A19,A21,TARSKI:def 1;
end;
now
A22: a in {a} & b in {b} by TARSKI:def 1;
assume o=a(#)b;
hence o in D by A22;
end;
hence o in D iff o=a(#)b by A18;
end;
X is closed_wrt_A7 by A1;
then D in X by A4;
then {a(#)b} in X by A17,TARSKI:def 1;
hence thesis by A1,Th2;
end;
theorem Th5:
X is closed_wrt_A1-A7 & A in X & B in X implies A/\B in X
proof
assume that
A1: X is closed_wrt_A1-A7 & A in X and
A2: B in X;
A\B in X by A1,A2,Th4;
then A\(A\B) in X by A1,Th4;
hence thesis by XBOOLE_1:48;
end;
theorem Th6:
X is closed_wrt_A1-A7 & o in X & p in X implies {o,p} in X & [o,p ] in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: o in X and
A3: p in X;
reconsider a=o,b=p as Element of V by A2,A3;
A4: {o} in X by A1,A2,Th2;
A5: X is closed_wrt_A2 by A1;
hence {o,p} in X by A2,A3;
{a,b} in X by A2,A3,A5;
hence thesis by A5,A4;
end;
theorem Th7:
X is closed_wrt_A1-A7 implies omega c= X
proof
assume
A1: X is closed_wrt_A1-A7;
assume not thesis;
then consider o being object such that
A2: o in omega and
A3: not o in X;
defpred P[Ordinal] means $1 in omega & not $1 in X;
A4: ex K st P[K] by A2,A3;
consider L such that
A5: P[L] & for M st P[M] holds L c= M from ORDINAL1:sch 1(A4);
L<>{} by A1,A5,Th3;
then
A6: {} in L by ORDINAL3:8;
not omega c= L by A5;
then not L is limit_ordinal by A6,ORDINAL1:def 11;
then consider M such that
A7: succ M = L by ORDINAL1:29;
A8: M in L by A7,ORDINAL1:6;
A9: L c= omega by A5;
A10: now
assume not M in X;
then
A11: L c= M by A5,A9,A8;
M c= L by A8,ORDINAL1:def 2;
then M=L by A11;
hence contradiction by A7,ORDINAL1:9;
end;
then {M} in X by A1,Th2;
then M \/ {M} in X by A1,A10,Th4;
hence contradiction by A5,A7;
end;
theorem Th8:
X is closed_wrt_A1-A7 implies Funcs(fs,omega) c= X
proof
defpred P[set] means Funcs($1,omega) c= X;
assume
A1: X is closed_wrt_A1-A7;
then Funcs({},omega)={{}} & {} in X by Th3,FUNCT_5:57;
then
A2: P[{}] by ZFMISC_1:31;
A3: omega c= X by A1,Th7;
A4: for o,B being set st o in fs & B c= fs & P[B] holds P[B \/ {o}]
proof
let o,B be set;
assume that
A5: o in fs and
B c= fs and
A6: Funcs(B,omega) c= X;
now
let p be object;
assume p in Funcs(B \/ {o},omega);
then consider g such that
A7: p=g and
A8: dom g = B \/ {o} and
A9: rng g c= omega by FUNCT_2:def 2;
set A=g|B;
rng A c= rng g by RELAT_1:70;
then
A10: rng A c= omega by A9;
set C=g|{o};
A11: dom C=(B \/ {o}) /\ {o} by A8,RELAT_1:61
.={o} by XBOOLE_1:21;
then
A12: C={[o,C.o]} by GRFUNC_1:7;
o in dom C by A11,TARSKI:def 1;
then
A13: C.o in rng C by FUNCT_1:def 3;
rng C c= rng g by RELAT_1:70;
then rng C c= omega by A9;
then
A14: C.o in omega by A13;
o in omega by A5;
then [o,C.o] in X by A1,A3,A14,Th6;
then
A15: C in X by A1,A12,Th2;
dom A=(B \/ {o}) /\ B by A8,RELAT_1:61
.=B by XBOOLE_1:21;
then
A16: A in Funcs(B,omega) by A10,FUNCT_2:def 2;
g = (g|(B \/ {o})) by A8
.= A \/ C by RELAT_1:78;
hence p in X by A1,A6,A7,A16,A15,Th4;
end;
hence thesis by TARSKI:def 3;
end;
A17: fs is finite;
thus P[fs] from FINSET_1:sch 2(A17,A2,A4);
end;
theorem Th9:
X is closed_wrt_A1-A7 & a in X implies Funcs(fs,a) in X
proof
defpred P[set] means Funcs($1,a) in X;
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in X;
A3: X is closed_wrt_A4 by A1;
A4: X is closed_wrt_A5 by A1;
A5: for o,B being set st o in fs & B c= fs & P[B] holds P[B \/ {o}]
proof
let o,B be set such that
A6: o in fs and
B c= fs and
A7: Funcs(B,a) in X;
per cases;
suppose
B meets {o};
hence thesis by A7,ZFMISC_1:40,50;
end;
suppose
A8: B misses {o};
set r = {o};
set A={{[x,y]}: x in r & y in a};
A9: omega c= X & o in omega by A1,A6,Th7;
then o in X;
then reconsider p=o as Element of V;
A10: Funcs({o},a)=A
proof
thus Funcs({o},a) c= A
proof
let q be object;
assume q in Funcs({o},a);
then consider g such that
A11: q=g and
A12: dom g={o} and
A13: rng g c= a by FUNCT_2:def 2;
o in dom g by A12,TARSKI:def 1;
then
A14: g.o in rng g by FUNCT_1:def 3;
then reconsider s=g.o as Element of V by A2,A13,Th1;
o in r & g={[p,s]} by A12,GRFUNC_1:7,TARSKI:def 1;
hence thesis by A11,A13,A14;
end;
let q be object;
assume q in A;
then consider x,y such that
A15: q={[x,y]} and
A16: x in r and
A17: y in a;
reconsider g=q as Function by A15;
rng g={y} by A15,RELAT_1:9;
then
A18: rng g c= a by A17,ZFMISC_1:31;
x=o by A16,TARSKI:def 1;
then dom g={o} by A15,RELAT_1:9;
hence thesis by A18,FUNCT_2:def 2;
end;
reconsider x=Funcs(B,a) as Element of V by A7;
{o} in X by A1,A9,Th2;
then
A19: Funcs({o},a) in X by A2,A3,A10;
then reconsider y=Funcs({o},a) as Element of V;
set Z={x9 \/ y9: x9 in x & y9 in y};
Funcs(B \/ {o},a)=Z
proof
thus Funcs(B \/ {o},a) c= Z
proof
let q be object;
assume q in Funcs(B \/ {o},a);
then consider g such that
A20: q=g and
A21: dom g=B \/ {o} and
A22: rng g c= a by FUNCT_2:def 2;
set A=g|B;
rng A c= rng g by RELAT_1:70;
then
A23: rng A c= a by A22;
set C=g|{o};
rng C c= rng g by RELAT_1:70;
then
A24: rng C c= a by A22;
dom C=(B \/ {o}) /\ {o} by A21,RELAT_1:61
.={o} by XBOOLE_1:21;
then
A25: C in y by A24,FUNCT_2:def 2;
then reconsider y9=C as Element of V by A19,Th1;
dom A=(B \/ {o}) /\ B by A21,RELAT_1:61
.=B by XBOOLE_1:21;
then
A26: A in x by A23,FUNCT_2:def 2;
then reconsider x9=A as Element of V by A7,Th1;
g=(g|(B \/ {o})) by A21
.=A \/ C by RELAT_1:78;
then q=x9 \/ y9 by A20;
hence thesis by A26,A25;
end;
let q be object;
assume q in Z;
then consider x9,y9 such that
A27: q=x9 \/ y9 and
A28: x9 in x and
A29: y9 in y;
consider e such that
A30: x9=e and
A31: dom e=B and
A32: rng e c= a by A28,FUNCT_2:def 2;
consider g such that
A33: y9=g and
A34: dom g={o} and
A35: rng g c= a by A29,FUNCT_2:def 2;
reconsider h=e \/ g as Function by A8,A31,A34,GRFUNC_1:13;
rng h=rng e \/ rng g by RELAT_1:12;
then
A36: rng h c= a \/ a by A32,A35,XBOOLE_1:13;
dom h=B \/ {o} by A31,A34,XTUPLE_0:23;
hence thesis by A27,A30,A33,A36,FUNCT_2:def 2;
end;
hence thesis by A4,A7,A19;
end;
end;
Funcs({},a)={{}} & {} in X by A1,Th3,FUNCT_5:57;
then
A37: P[{}] by A1,Th2;
A38: fs is finite;
thus P[fs] from FINSET_1:sch 2(A38,A37,A5);
end;
theorem Th10:
X is closed_wrt_A1-A7 & a in Funcs(fs,omega) & b in X implies
{a(#)x: x in b} in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in Funcs(fs,omega) and
A3: b in X;
Funcs(fs,omega) c= X by A1,Th8;
then
A4: {a} in X by A1,A2,Th2;
set A={a(#)x: x in b};
set s={a};
set B={y(#)x where y,x is Element of V: y in s & x in b};
A5: B c= A
proof
let q be object;
assume q in B;
then consider y,x such that
A6: q=y(#)x & y in s and
A7: x in b;
q=a(#)x by A6,TARSKI:def 1;
hence thesis by A7;
end;
A c= B
proof
let q be object;
assume q in A;
then
A8: ex x st q=a(#)x & x in b;
a in s by TARSKI:def 1;
hence thesis by A8;
end;
then
A9: A=B by A5;
X is closed_wrt_A7 by A1;
hence thesis by A3,A4,A9;
end;
Lm12: X is closed_wrt_A1-A7 implies n in X
by Th7,TARSKI:def 3;
Lm13: X is closed_wrt_A1-A7 implies 0-element_of(V) in X & 1-element_of(V) in X
proof
assume
A1: X is closed_wrt_A1-A7;
hence 0-element_of(V) in X by Th3;
{} in X by A1,Th3;
then 1 = succ 0 & {} \/ {{}} in X by A1,Th2;
hence thesis;
end;
theorem Th11:
X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs(
fs,a) implies {x: x in Funcs(fs\{n},a) & ex u st {[n,u]} \/ x in b} in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: n in fs and
A3: a in X and
A4: b in X and
A5: b c= Funcs(fs,a);
A6: Funcs({n},a) in X by A1,A3,Th9;
then reconsider F=Funcs({n},a) as Element of V;
set T={[n,x]: x in a};
A7: T=union F
proof
thus T c= union F
proof
let q be object;
assume q in T;
then consider x such that
A8: q=[n,x] and
A9: x in a;
reconsider g={[n,x]} as Function;
rng g={x} by RELAT_1:9;
then dom g={n} & rng g c= a by A9,RELAT_1:9,ZFMISC_1:31;
then
A10: g in F by FUNCT_2:def 2;
q in g by A8,TARSKI:def 1;
hence thesis by A10,TARSKI:def 4;
end;
let q be object;
assume q in union F;
then consider A such that
A11: q in A and
A12: A in F by TARSKI:def 4;
consider g such that
A13: A=g and
A14: dom g={n} and
A15: rng g c= a by A12,FUNCT_2:def 2;
n in dom g by A14,TARSKI:def 1;
then
A16: g.n in rng g by FUNCT_1:def 3;
then reconsider o=g.n as Element of V by A3,A15,Th1;
q in {[n,g.n]} by A11,A13,A14,GRFUNC_1:7;
then q=[n,o] by TARSKI:def 1;
hence thesis by A15,A16;
end;
then T in X by A1,A6,Th2;
then
A17: {T} in X by A1,Th2;
then reconsider t={T} as Element of V;
set Y={x: x in Funcs(fs\{n},a) & ex u st {[n,u]} \/ x in b};
set Z={y\z: y in b & z in t};
A18: Z=Y
proof
thus Z c= Y
proof
let q be object;
assume q in Z;
then consider y,z such that
A19: q=y\z and
A20: y in b and
A21: z in t;
A22: q=y\T by A19,A21,TARSKI:def 1;
consider g such that
A23: y=g and
A24: dom g=fs and
A25: rng g c= a by A5,A20,FUNCT_2:def 2;
set h=g|(fs\{n});
A26: dom h=fs /\ (fs\{n}) by A24,RELAT_1:61
.=fs /\ fs \ fs /\ {n} by XBOOLE_1:50
.=fs\{n} by XBOOLE_1:47;
A27: h=g\T
proof
let r,s be object;
thus [r,s] in h implies [r,s] in g\T
proof
assume
A28: [r,s] in h;
r in fs\{n} by A26,A28,FUNCT_1:1;
then not r in {n} by XBOOLE_0:def 5;
then
A29: r<>n by TARSKI:def 1;
A30: not [r,s] in T
proof
assume [r,s] in T;
then ex x st [r,s]=[n,x] & x in a;
hence contradiction by A29,XTUPLE_0:1;
end;
[r,s] in g by A28,RELAT_1:def 11;
hence thesis by A30,XBOOLE_0:def 5;
end;
assume
A31: [r,s] in g\T;
A32: s=g.r by A31,FUNCT_1:1;
A33: r in dom g by A31,FUNCT_1:1;
then
A34: s in rng g by A32,FUNCT_1:def 3;
n<>r
proof
reconsider a1=s as Element of V by A3,A25,A34,Th1;
assume n=r;
then [r,a1] in T by A25,A34;
hence contradiction by A31,XBOOLE_0:def 5;
end;
then not r in {n} by TARSKI:def 1;
then
A35: r in fs\{n} by A24,A33,XBOOLE_0:def 5;
then s=h.r by A32,FUNCT_1:49;
hence thesis by A26,A35,FUNCT_1:1;
end;
rng h c= rng g by RELAT_1:70;
then rng h c= a by A25;
then
A36: q in Funcs(fs\{n},a) by A22,A23,A26,A27,FUNCT_2:def 2;
Funcs(fs\{n},a) in X by A1,A3,Th9;
then reconsider a2=q as Element of V by A36,Th1;
{[n,g.n]}=y/\T
proof
thus {[n,g.n]} c= y/\T
proof
let r,s be object;
A37: g.n in rng g by A2,A24,FUNCT_1:def 3;
then reconsider a1=g.n as Element of V by A3,A25,Th1;
A38: [n,a1] in T by A25,A37;
set p = [r,s];
assume p in {[n,g.n]};
then
A39: p=[n,g.n] by TARSKI:def 1;
then p in y by A2,A23,A24,FUNCT_1:1;
hence thesis by A39,A38,XBOOLE_0:def 4;
end;
let p be object;
assume
A40: p in y/\T;
then p in T by XBOOLE_0:def 4;
then
A41: ex x st p=[n,x] & x in a;
p in y by A40,XBOOLE_0:def 4;
then p=[n,g.n] by A23,A41,FUNCT_1:1;
hence thesis by TARSKI:def 1;
end;
then {[n,g.n]} \/ (y\T) in b by A20,XBOOLE_1:51;
then a2 in Y by A22,A36;
hence thesis;
end;
reconsider z=T as Element of V by A7;
let q be object;
assume q in Y;
then consider x such that
A42: q=x and
A43: x in Funcs(fs\{n},a) and
A44: ex u st {[n,u]} \/ x in b;
consider u such that
A45: {[n,u]} \/ x in b by A44;
reconsider y={[n,u]} \/ x as Element of V by A4,A45,Th1;
A46: x=y\z
proof
consider g such that
A47: x=g and
A48: dom g=fs\{n} and
rng g c= a by A43,FUNCT_2:def 2;
thus x c= y\z
proof
let p be object;
assume
A49: p in x;
then consider a1,a2 being object such that
A50: p=[a1,a2] by A47,RELAT_1:def 1;
a1 in dom g by A47,A49,A50,FUNCT_1:1;
then
A51: not a1 in {n} by A48,XBOOLE_0:def 5;
A52: not p in z
proof
assume p in z;
then ex x9 st p=[n,x9] & x9 in a;
then a1=n by A50,XTUPLE_0:1;
hence contradiction by A51,TARSKI:def 1;
end;
p in y by A49,XBOOLE_0:def 3;
hence thesis by A52,XBOOLE_0:def 5;
end;
thus y\z c= x
proof
A53: x misses z
proof
assume not thesis;
then consider r being object such that
A54: r in g and
A55: r in z by A47,XBOOLE_0:3;
consider a1,a2 being object such that
A56: r=[a1,a2] by A54,RELAT_1:def 1;
a1 in dom g by A54,A56,FUNCT_1:1;
then
A57: not a1 in {n} by A48,XBOOLE_0:def 5;
not r in z
proof
assume r in z;
then ex x9 st r=[n,x9] & x9 in a;
then a1=n by A56,XTUPLE_0:1;
hence contradiction by A57,TARSKI:def 1;
end;
hence contradiction by A55;
end;
{[n,u]} c= z
proof
consider g such that
A58: {[n,u]} \/ x = g and
dom g=fs and
A59: rng g c= a by A5,A45,FUNCT_2:def 2;
{[n,u]} c= g by A58,XBOOLE_1:7;
then [n,u] in g by ZFMISC_1:31;
then n in dom g & u=g.n by FUNCT_1:1;
then
A60: u in rng g by FUNCT_1:def 3;
then reconsider a1=u as Element of V by A3,A59,Th1;
assume not thesis;
then
A61: ex r being object st r in {[n,u]} & not r in z;
[n,a1] in z by A59,A60;
hence contradiction by A61,TARSKI:def 1;
end;
then {[n,u]}\z={} by XBOOLE_1:37;
then
A62: (x\z)\/({[n,u]}\z)=x by A53,XBOOLE_1:83;
let p be object;
assume p in y\z;
hence thesis by A62,XBOOLE_1:42;
end;
end;
z in t by TARSKI:def 1;
hence thesis by A42,A45,A46;
end;
X is closed_wrt_A6 by A1;
hence thesis by A4,A17,A18;
end;
theorem Th12:
for n st X is closed_wrt_A1-A7 & a in X & b in X holds {{[n,x]}
\/ y: x in a & y in b} in X
proof
let n;
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in X and
A3: b in X;
A4: Funcs({n},a) in X by A1,A2,Th9;
then reconsider F=Funcs({n},a) as Element of V;
set Z={{[n,x]} \/ y: x in a & y in b};
set Y={x \/ y: x in F & y in b};
A5: Y=Z
proof
thus Y c= Z
proof
let p be object;
assume p in Y;
then consider x,y such that
A6: p=x \/ y and
A7: x in F and
A8: y in b;
consider g such that
A9: x=g and
A10: dom g={n} and
A11: rng g c= a by A7,FUNCT_2:def 2;
n in dom g by A10,TARSKI:def 1;
then
A12: g.n in rng g by FUNCT_1:def 3;
then reconsider z=g.n as Element of V by A2,A11,Th1;
p={[n,z]} \/ y by A6,A9,A10,GRFUNC_1:7;
hence thesis by A8,A11,A12;
end;
let p be object;
assume p in Z;
then consider x,y such that
A13: p={[n,x]} \/ y and
A14: x in a and
A15: y in b;
reconsider g={[n,x]} as Function;
rng g={x} by RELAT_1:9;
then dom g={n} & rng g c= a by A14,RELAT_1:9,ZFMISC_1:31;
then
A16: {[n,x]} in F by FUNCT_2:def 2;
then reconsider z={[n,x]} as Element of V by A4,Th1;
p=z \/ y by A13;
hence thesis by A15,A16;
end;
X is closed_wrt_A5 by A1;
hence thesis by A3,A4,A5;
end;
theorem Th13:
(X is closed_wrt_A1-A7 & B is finite & for o st o in B holds o
in X) implies B in X
proof
defpred P[set] means $1 in X;
assume that
A1: X is closed_wrt_A1-A7 and
A2: B is finite and
A3: for o st o in B holds o in X;
A4: B is finite by A2;
A5: for o,C being set st o in B & C c= B & P[C] holds P[C \/ {o}]
proof
let o,C be set;
assume that
A6: o in B and
C c= B and
A7: C in X;
o in X by A3,A6;
then {o} in X by A1,Th2;
hence thesis by A1,A7,Th4;
end;
A8: P[{}] by A1,Th3;
thus P[B] from FINSET_1:sch 2(A4,A8,A5);
end;
theorem Th14:
X is closed_wrt_A1-A7 & A c= X & y in Funcs(fs,A) implies y in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: A c= X and
A3: y in Funcs(fs,A);
consider g such that
A4: y=g and
A5: dom g=fs and
A6: rng g c= A by A3,FUNCT_2:def 2;
A7: now
let o;
assume
A8: o in y;
then consider p,q being object such that
A9: o=[p,q] by A4,RELAT_1:def 1;
A10: p in dom g by A4,A8,A9,FUNCT_1:1;
q=g.p by A4,A8,A9,FUNCT_1:1;
then q in rng g by A10,FUNCT_1:def 3;
then
A11: q in A by A6;
A12: omega c= X by A1,Th7;
p in omega by A5,A10;
hence o in X by A1,A2,A9,A12,A11,Th6;
end;
rng g is finite by A5,FINSET_1:8;
then [:dom g,rng g:] is finite by A5;
then y is finite by A4,FINSET_1:1,RELAT_1:7;
hence thesis by A1,A7,Th13;
end;
theorem Th15:
for n st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs(fs
,a) holds {{[n,x]} \/ y: x in a} in X
proof
let n;
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in X and
A3: a c= X & y in Funcs(fs,a);
set Z={{[n,x]} \/ y: x in a};
set s={y};
set Y={{[n,x]} \/ z: x in a & z in s};
A4: Y=Z
proof
thus Y c= Z
proof
let p be object;
assume p in Y;
then consider x,z such that
A5: p={[n,x]} \/ z & x in a and
A6: z in s;
z=y by A6,TARSKI:def 1;
hence thesis by A5;
end;
let p be object;
assume p in Z;
then
A7: ex x st p={[n,x]} \/ y & x in a;
y in s by TARSKI:def 1;
hence thesis by A7;
end;
y in X by A1,A3,Th14;
then {y} in X by A1,Th2;
hence thesis by A1,A2,A4,Th12;
end;
theorem
X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs(fs,
a) & b c= Funcs(fs \/ {n},a) & b in X implies {x: x in a & {[n,x]} \/ y in b}
in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: not n in fs and
A3: a in X and
A4: a c= X and
A5: y in Funcs(fs,a) and
A6: b c= Funcs(fs \/ {n},a) and
A7: b in X;
y in X by A1,A4,A5,Th14;
then
A8: {y} in X by A1,Th2;
set T={{[n,x]} \/ y: x in a};
set T9= T /\ b;
T in X by A1,A3,A4,A5,Th15;
then
A9: T9 in X by A1,A7,Th5;
then reconsider t9=T9 as Element of V;
set S={{[n,x]}: {[n,x]} \/ y in b};
set s={y};
set R={x\z: x in t9 & z in s};
A10: {[n,x]} \/ y in b implies x in a
proof
A11: [n,x] in {[n,x]} by TARSKI:def 1;
assume {[n,x]} \/ y in b;
then consider g such that
A12: {[n,x]} \/ y = g and
dom g=fs \/ {n} and
A13: rng g c= a by A6,FUNCT_2:def 2;
{[n,x]} c= g by A12,XBOOLE_1:7;
then n in dom g & x=g.n by A11,FUNCT_1:1;
then x in rng g by FUNCT_1:def 3;
hence thesis by A13;
end;
A14: R = S
proof
thus R c= S
proof
let p be object;
assume p in R;
then consider x,z such that
A15: p=x\z and
A16: x in t9 and
A17: z in s;
A18: x in b by A16,XBOOLE_0:def 4;
x in T by A16,XBOOLE_0:def 4;
then consider x9 such that
A19: x={[n,x9]} \/ y and
x9 in a;
A20: {[n,x9]} misses y
proof
assume not thesis;
then consider r being object such that
A21: r in {[n,x9]} and
A22: r in y by XBOOLE_0:3;
A23: ex g st y=g & dom g=fs & rng g c= a by A5,FUNCT_2:def 2;
r=[n,x9] by A21,TARSKI:def 1;
hence contradiction by A2,A22,A23,FUNCT_1:1;
end;
z=y by A17,TARSKI:def 1;
then x\z=({[n,x9]}\y) \/ (y\y) by A19,XBOOLE_1:42
.={[n,x9]} \/ (y\y) by A20,XBOOLE_1:83
.={[n,x9]} \/ {} by XBOOLE_1:37
.={[n,x9]};
hence thesis by A15,A18,A19;
end;
let p be object;
assume p in S;
then consider x such that
A24: p={[n,x]} and
A25: {[n,x]} \/ y in b;
reconsider x9={[n,x]} \/ y as Element of V by A7,A25,Th1;
x in a by A10,A25;
then x9 in T;
then
A26: y in s & x9 in t9 by A25,TARSKI:def 1,XBOOLE_0:def 4;
A27: {[n,x]} misses y
proof
assume not thesis;
then consider r being object such that
A28: r in {[n,x]} and
A29: r in y by XBOOLE_0:3;
A30: ex g st y=g & dom g=fs & rng g c= a by A5,FUNCT_2:def 2;
r=[n,x] by A28,TARSKI:def 1;
hence contradiction by A2,A29,A30,FUNCT_1:1;
end;
x9\y=({[n,x]}\y) \/ (y\y) by XBOOLE_1:42
.={[n,x]} \/ (y\y) by A27,XBOOLE_1:83
.={[n,x]} \/ {} by XBOOLE_1:37
.={[n,x]};
hence thesis by A24,A26;
end;
X is closed_wrt_A6 by A1;
then R in X by A9,A8;
then union S in X by A1,A14,Th2;
then union union S in X by A1,Th2;
then
A31: union union union S in X by A1,Th2;
set Z={x: x in a & {[n,x]} \/ y in b};
A32: Z c= union union union S
proof
let p be object;
assume p in Z;
then consider x such that
A33: p=x and
x in a and
A34: {[n,x]} \/ y in b;
A35: [n,x] in {[n,x]} by TARSKI:def 1;
A36: {n,x} in {{n,x},{n}} by TARSKI:def 2;
{[n,x]} in S by A34;
then {{n,x},{n}} in union S by A35,TARSKI:def 4;
then
A37: {n,x} in union union S by A36,TARSKI:def 4;
x in {n,x} by TARSKI:def 2;
hence thesis by A33,A37,TARSKI:def 4;
end;
A38: union union union S c= Z \/ {n}
proof
let p be object;
assume p in union union union S;
then consider C such that
A39: p in C and
A40: C in union union S by TARSKI:def 4;
consider D such that
A41: C in D and
A42: D in union S by A40,TARSKI:def 4;
consider E being set such that
A43: D in E and
A44: E in S by A42,TARSKI:def 4;
consider x such that
A45: E={[n,x]} and
A46: {[n,x]} \/ y in b by A44;
D=[n,x] by A43,A45,TARSKI:def 1;
then p in {n,x} or p in {n} by A39,A41,TARSKI:def 2;
then
A47: p=n or p=x or p in {n} by TARSKI:def 2;
x in a by A10,A46;
then p in Z or p in {n} by A46,A47,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
per cases;
suppose
n in Z;
then {n} c= Z by ZFMISC_1:31;
then Z \/ {n} = Z by XBOOLE_1:12;
hence thesis by A31,A32,A38,XBOOLE_0:def 10;
end;
suppose
not n in Z;
then
A48: Z misses {n} by ZFMISC_1:50;
(union union union S) \ {n} c= (Z \/ {n}) \ {n} by A38,XBOOLE_1:33;
then (union union union S) \ {n} c= (Z\{n}) \/ ({n}\{n}) by XBOOLE_1:42;
then (union union union S) \ {n} c= Z \/ ({n}\{n}) by A48,XBOOLE_1:83;
then
A49: (union union union S) \ {n} c= Z \/ {} by XBOOLE_1:37;
Z \ {n} c= (union union union S) \ {n} by A32,XBOOLE_1:33;
then Z c= (union union union S) \ {n} by A48,XBOOLE_1:83;
then
A50: (union union union S) \ {n} = Z by A49;
n in X by A1,Lm12;
then {n} in X by A1,Th2;
hence thesis by A1,A31,A50,Th4;
end;
end;
Lm14: {[o,p],[p,p]}(#){[p,q]}={[o,q],[p,q]}
proof
let s,u be object;
thus [s,u] in {[o,p],[p,p]}(#){[p,q]} implies [s,u] in {[o,q],[p,q]}
proof
assume [s,u] in {[o,p],[p,p]}(#){[p,q]};
then consider t being object such that
A1: [s,t] in {[o,p],[p,p]} and
A2: [t,u] in {[p,q]} by RELAT_1:def 8;
[t,u]=[p,q] by A2,TARSKI:def 1;
then
A3: u=q by XTUPLE_0:1;
[s,t]=[o,p] or [s,t]=[p,p] by A1,TARSKI:def 2;
then [s,u]=[o,q] or [s,u]=[p,q] by A3,XTUPLE_0:1;
hence thesis by TARSKI:def 2;
end;
assume
A4: [s,u] in {[o,q],[p,q]};
per cases by A4,TARSKI:def 2;
suppose
A5: [s,u]=[o,q];
[o,p] in {[o,p],[p,p]} & [p,q] in {[p,q]} by TARSKI:def 1,def 2;
hence thesis by A5,RELAT_1:def 8;
end;
suppose
A6: [s,u]=[p,q];
[p,p] in {[o,p],[p,p]} & [p,q] in {[p,q]} by TARSKI:def 1,def 2;
hence thesis by A6,RELAT_1:def 8;
end;
end;
theorem Th17:
X is closed_wrt_A1-A7 & a in X implies {{[0-element_of(V),x], [
1-element_of(V),x]} : x in a} in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in X;
set f={[0-element_of(V),1-element_of(V)],[1-element_of(V),1-element_of(V)]};
A3: 1-element_of(V) in X by A1,Lm13;
then
A4: [1-element_of(V),1-element_of(V)] in X by A1,Th6;
set F={{[1-element_of(V),x]}:x in a};
A5: X is closed_wrt_A4 by A1;
A6: F in X
proof
reconsider s={1-element_of(V)} as Element of V;
A7: F={{[y,x]} where y,x: y in s & x in a}
proof
thus F c= {{[y,x]} where y,x: y in s & x in a}
proof
reconsider y=1-element_of(V) as Element of V;
let p be object;
assume p in F;
then
A8: ex x st p={[1-element_of(V),x]} & x in a;
y in s by TARSKI:def 1;
hence thesis by A8;
end;
let p be object;
assume p in {{[y,x]} where y,x: y in s & x in a};
then consider y,x such that
A9: p={[y,x]} & y in s and
A10: x in a;
p={[1-element_of(V),x]} by A9,TARSKI:def 1;
hence thesis by A10;
end;
1-element_of(V) in X by A1,Lm13;
then {1-element_of(V)} in X by A1,Th2;
hence thesis by A2,A5,A7;
end;
then reconsider F9=F as Element of V;
set f9={f};
set Z={{[0-element_of(V),x],[1-element_of(V),x]}: x in a};
A11: Z={x(#)y: x in f9 & y in F9}
proof
thus Z c= {x(#)y: x in f9 & y in F9}
proof
reconsider x9=f as Element of V;
let p be object;
A12: x9 in f9 by TARSKI:def 1;
assume p in Z;
then consider x such that
A13: p={[0-element_of(V),x],[1-element_of(V),x]} & x in a;
reconsider y={[1-element_of(V),x]} as Element of V;
y in F9 & p=x9(#)y by A13,Lm14;
hence thesis by A12;
end;
let p be object;
assume p in {x(#)y: x in f9 & y in F9};
then consider x,y such that
A14: p=x(#)y and
A15: x in f9 and
A16: y in F9;
consider x9 such that
A17: y={[1-element_of(V),x9]} and
A18: x9 in a by A16;
x={[0-element_of(V),1-element_of(V)],[1-element_of(V), 1-element_of(V
)]} by A15,TARSKI:def 1;
then p={[0-element_of(V),x9],[1-element_of(V),x9]} by A14,A17,Lm14;
hence thesis by A18;
end;
0-element_of(V) in X by A1,Lm13;
then [0-element_of(V),1-element_of(V)] in X by A1,A3,Th6;
then f in X by A1,A4,Th6;
then
A19: {f} in X by A1,Th2;
X is closed_wrt_A7 by A1;
hence thesis by A19,A6,A11;
end;
Lm15: p<>r implies {[o,p],[q,r]}(#){[p,s],[r,t]}={[o,s],[q,t]}
proof
assume
A1: p<>r;
let a1,a3 be object;
thus [a1,a3] in {[o,p],[q,r]}(#){[p,s],[r,t]}
implies [a1,a3] in {[o,s],[q,t]}
proof
assume [a1,a3] in {[o,p],[q,r]}(#){[p,s],[r,t]};
then consider a2 being object such that
A2: [a1,a2] in {[o,p],[q,r]} and
A3: [a2,a3] in {[p,s],[r,t]} by RELAT_1:def 8;
[a1,a2]=[o,p] or [a1,a2]=[q,r] by A2,TARSKI:def 2;
then
A4: a1=o & a2=p or a1=q & a2=r by XTUPLE_0:1;
[a2,a3]=[p,s] or [a2,a3]=[r,t] by A3,TARSKI:def 2;
then a1=o & a2=p & a3=s or a1=q & a2=r & a3=t by A1,A4,XTUPLE_0:1;
hence thesis by TARSKI:def 2;
end;
assume
A5: [a1,a3] in {[o,s],[q,t]};
per cases by A5,TARSKI:def 2;
suppose
A6: [a1,a3]=[o,s];
[o,p] in {[o,p],[q,r]} & [p,s] in {[p,s],[r,t]} by TARSKI:def 2;
hence thesis by A6,RELAT_1:def 8;
end;
suppose
A7: [a1,a3]=[q,t];
[q,r] in {[o,p],[q,r]} & [r,t] in {[p,s],[r,t]} by TARSKI:def 2;
hence thesis by A7,RELAT_1:def 8;
end;
end;
Lm16: for g be Function holds dom g={o,q} iff g={[o,g.o],[q,g.q]}
proof
let g be Function;
hereby
assume
A1: dom g={o,q};
now
let p be object;
A2: now
assume
A3: p=[o,g.o] or p=[q,g.q];
now
per cases by A3;
suppose
A4: p=[o,g.o];
o in dom g by A1,TARSKI:def 2;
hence p in g by A4,FUNCT_1:1;
end;
suppose
A5: p=[q,g.q];
q in dom g by A1,TARSKI:def 2;
hence p in g by A5,FUNCT_1:1;
end;
end;
hence p in g;
end;
now
assume
A6: p in g;
then consider r,s being object such that
A7: p=[r,s] by RELAT_1:def 1;
r in dom g by A6,A7,FUNCT_1:1;
then r=o or r=q by A1,TARSKI:def 2;
hence p=[o,g.o] or p=[q,g.q] by A6,A7,FUNCT_1:1;
end;
hence p in g iff p=[o,g.o] or p=[q,g.q] by A2;
end;
hence g={[o,g.o],[q,g.q]} by TARSKI:def 2;
end;
assume
A8: g={[o,g.o],[q,g.q]};
now
let p be object;
A9: now
assume
A10: p=o or p=q;
now
per cases by A10;
suppose
p=o;
then [p,g.p] in g by A8,TARSKI:def 2;
hence p in dom g by FUNCT_1:1;
end;
suppose
p=q;
then [p,g.p] in g by A8,TARSKI:def 2;
hence p in dom g by FUNCT_1:1;
end;
end;
hence p in dom g;
end;
now
assume p in dom g;
then [p,g.p] in g by FUNCT_1:1;
then [p,g.p]=[o,g.o] or [p,g.p]=[q,g.q] by A8,TARSKI:def 2;
hence p=o or p=q by XTUPLE_0:1;
end;
hence p in dom g iff p=o or p=q by A9;
end;
hence thesis by TARSKI:def 2;
end;
theorem Th18:
X is closed_wrt_A1-A7 & E in X implies for v1,v2 holds Diagram(
v1 '=' v2,E) in X & Diagram(v1 'in' v2,E) in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: E in X;
A3: X is closed_wrt_A4 by A1;
A4: X is closed_wrt_A1 by A1;
A5: omega c= X by A1,Th7;
reconsider m=E as Element of V by A2;
let v1,v2;
set H=v1 '=' v2;
set H9=v1 'in' v2;
A6: Free(H)={v1,v2} by ZF_LANG1:58;
then
A7: v1 in Free H by TARSKI:def 2;
A8: v2 in Free H by A6,TARSKI:def 2;
A9: Free(H9)={v1,v2} by ZF_LANG1:59;
then
A10: v1 in Free H9 by TARSKI:def 2;
A11: v2 in Free H9 by A9,TARSKI:def 2;
per cases;
suppose
A12: v1=v2;
set a=code Free(H);
set Z={{[z,y]} where z,y: z in a & y in m};
A13: Free(H)={v1} by A6,A12,ENUMSET1:29;
A14: x".v1 in X by A5;
A15: Z=Diagram(H,E)
proof
thus Z c= Diagram(H,E)
proof
let p be object;
A16: H is being_equality by ZF_LANG:5;
assume p in Z;
then consider z,y such that
A17: p={[z,y]} and
A18: z in a and
A19: y in m;
reconsider f =VAR --> y as Function of VAR,E by A19,FUNCOP_1:45;
z in { x".v1} by A13,A18,Lm6;
then
A20: z= x".v1 by TARSKI:def 1;
dom((f*decode)|code Free(H))=code Free H by Lm3
.={z} by A13,A20,Lm6;
then
((f*decode)|code Free H)={[z,((f*decode)|code Free(H)).z]} by GRFUNC_1:7;
then (f*decode)|code Free H={[z,f.v1]} by A7,A20,Lm9;
then
A21: (f*decode)|code Free H=p by A17,FUNCOP_1:7;
f.(Var1 H)=f.v2 by A12,ZF_LANG1:1
.=f.(Var2 H) by ZF_LANG1:1;
then f in St(H,E) by A16,ZF_MODEL:7;
hence thesis by A21,Def4;
end;
reconsider z= x".v1 as Element of V by A14;
let p be object;
assume p in Diagram(H,E);
then consider f such that
A22: p=(f*decode)|code Free(H) and
f in St(H,E) by Def4;
reconsider y=f.v1 as Element of V by A2,Th1;
dom((f*decode)|code Free H)=code Free H by Lm3
.={z} by A13,Lm6;
then ((f*decode)|code Free H)={[z,((f*decode)|code Free(H)).z]} by
GRFUNC_1:7;
then
A23: p={[z,y]} by A7,A22,Lm9;
z in {z} by TARSKI:def 1;
then z in a by A13,Lm6;
hence thesis by A23;
end;
{x".v1} in X by A1,A14,Th2;
then code Free(H) in X by A13,Lm6;
hence Diagram(H,E) in X by A2,A3,A15;
Diagram(H9,E)={}
proof
set p = the Element of Diagram(H9,E);
assume not thesis;
then consider f being Function of VAR,E such that
p=(f*decode)|code Free(H9) and
A24: f in St(H9,E) by Def4;
H9 is being_membership by ZF_LANG:5;
then f.(Var1 H9) in f.(Var2 H9) by A24,ZF_MODEL:8;
then f.v1 in f.(Var2 H9) by ZF_LANG1:2;
then f.v1 in f.v2 by ZF_LANG1:2;
hence contradiction by A12;
end;
hence thesis by A1,Th3;
end;
suppose
A25: v1<>v2;
x".v2 in X & 1-element_of(V) in X by A5;
then
A26: [ x".v2,1-element_of(V)] in X by A1,Th6;
x".v1 in X & 0-element_of(V) in X by A1,A5,Lm13;
then [ x".v1,0-element_of(V)] in X by A1,Th6;
then ({[ x".v1,0-element_of(V)],[ x".v2,1-element_of(V)]}) in X by A1,A26
,Th6;
then reconsider d={[ x".v1,0-element_of(V)],[ x".v2,1-element_of(V)]} as
Element of V;
set fs=code Free H;
A27: fs={ x".v1, x".v2} by A6,Lm7;
A28: now
assume x".v1= x".v2;
then v1=x.(x".v2) by Def2
.=v2 by Def2;
hence contradiction by A25;
end;
A29: d in Funcs(fs,omega)
proof
reconsider g={[x".v1,0-element_of(V)]}, h={[x".v2,1-element_of(V)]} as
Function;
reconsider e=d as Function by A28,GRFUNC_1:8;
A30: 0-element_of(V) in omega by ORDINAL1:def 11;
A31: e=g \/ h by ENUMSET1:1;
then rng e=rng g \/ rng h by RELAT_1:12
.={0-element_of(V)} \/ rng h by RELAT_1:9
.={0-element_of(V)} \/ {1-element_of(V)} by RELAT_1:9
.={0-element_of(V),1-element_of(V)} by ENUMSET1:1;
then
A32: rng e c= omega by A30,ZFMISC_1:32;
dom e=dom g \/ dom h by A31,XTUPLE_0:23
.={ x".v1} \/ dom h by RELAT_1:9
.={ x".v1} \/ { x".v2} by RELAT_1:9
.=fs by A27,ENUMSET1:1;
hence thesis by A32,FUNCT_2:def 2;
end;
set a={{[0-element_of(V),x],[1-element_of(V),x]}: x in m};
a in X by A1,A2,Th17;
then reconsider a as Element of V;
set b={{[0-element_of(V),x],[1-element_of(V),y]}: x in y & x in m & y in m
};
set Y={d(#)x: x in a};
A33: b in X by A2,A4;
then reconsider b as Element of V;
set Z={d(#)x: x in b};
Y=Diagram(H,E)
proof
thus Y c= Diagram(H,E)
proof
let p be object;
assume p in Y;
then consider x such that
A34: p=d(#)x and
A35: x in a;
consider y such that
A36: x={[0-element_of(V),y],[1-element_of(V),y]} and
A37: y in m by A35;
reconsider f=VAR --> y as Function of VAR,E by A37,FUNCOP_1:45;
A38: f.(Var1 H)=y by FUNCOP_1:7
.=f.(Var2 H) by FUNCOP_1:7;
H is being_equality by ZF_LANG:5;
then
A39: f in St(H,E) by A38,ZF_MODEL:7;
A40: ((f*decode)|code Free H).( x".v2)=f.v2 by A8,Lm9
.=y by FUNCOP_1:7;
A41: ((f*decode)|code Free H).( x".v1)=f.v1 by A7,Lm9
.=y by FUNCOP_1:7;
A42: dom((f*decode)|code Free(H))={ x".v1, x".v2} by A27,Lm3;
p={[ x".v1,y],[ x".v2,y]} by A34,A36,Lm15;
then (f*decode)|code Free(H)=p by A42,A41,A40,Lm16;
hence thesis by A39,Def4;
end;
let p be object;
assume p in Diagram(H,E);
then consider f such that
A43: p=(f*decode)|code Free(H) and
A44: f in St(H,E) by Def4;
reconsider y=f.v1 as Element of V by A2,Th1;
H is being_equality by ZF_LANG:5;
then f.(Var1 H)=f.(Var2 H) by A44,ZF_MODEL:7;
then f.v1=f.(Var2 H) by ZF_LANG1:1
.=f.v2 by ZF_LANG1:1;
then
A45: ((f*decode)|code Free H).( x".v2)=y by A8,Lm9;
reconsider x={[0-element_of(V),y],[1-element_of(V),y]} as Element of V;
dom((f*decode)|code Free(H))={ x".v1, x".v2} & ((f*decode)|code
Free H).( x".v1)=y by A7,A27,Lm3,Lm9;
then p={[ x".v1,y],[ x".v2,y]} by A43,A45,Lm16;
then ({[0-element_of(V),y],[1-element_of(V),y]}) in a & p=d(#)x by Lm15;
hence thesis;
end;
hence Diagram(H,E) in X by A1,A2,A29,Th10,Th17;
Z=Diagram(H9,E)
proof
thus Z c= Diagram(H9,E)
proof
reconsider a1=v1 as Element of VAR;
let p be object;
assume p in Z;
then consider x such that
A46: p=d(#)x and
A47: x in b;
consider y,z such that
A48: x={[0-element_of(V),y],[1-element_of(V),z]} and
A49: y in z and
A50: y in m & z in m by A47;
A51: p={[ x".v1,y],[ x".v2,z]} by A46,A48,Lm15;
reconsider y9=y, z9=z as Element of E by A50;
deffunc F(set) = z9;
consider f being Function of VAR,E such that
A52: f.a1=y9 & for v3 being Element of VAR st v3<>a1 holds f.v3=F
(v3) from FUNCT_2:sch 6;
A53: ((f*decode)|code Free H9).( x".v2)=f.v2 by A11,Lm9
.=z by A25,A52;
A54: ((f*decode)|code Free H9).( x".v1)=y by A10,A52,Lm9;
f.v1 in f.v2 by A25,A49,A52;
then f.(Var1 H9) in f.v2 by ZF_LANG1:2;
then H9 is being_membership & f.(Var1 H9) in f.(Var2 H9) by ZF_LANG:5
,ZF_LANG1:2;
then
A55: f in St(H9,E) by ZF_MODEL:8;
dom((f*decode)|code Free H9)={ x".v1, x".v2} by A6,A9,A27,Lm3;
then p=(f*decode)|code Free(H9) by A51,A54,A53,Lm16;
hence thesis by A55,Def4;
end;
let p be object;
assume p in Diagram(H9,E);
then consider f being Function of VAR,E such that
A56: p=(f*decode)|code Free(H9) and
A57: f in St(H9,E) by Def4;
reconsider z=f.v2 as Element of V by A2,Th1;
reconsider y=f.v1 as Element of V by A2,Th1;
H9 is being_membership by ZF_LANG:5;
then f.(Var1 H9) in f.(Var2 H9) by A57,ZF_MODEL:8;
then f.v1 in f.(Var2 H9) by ZF_LANG1:2;
then y in z by ZF_LANG1:2;
then
A58: ({[0-element_of(V),y],[1-element_of(V),z]}) in b;
reconsider x={[0-element_of(V),y],[1-element_of(V),z]} as Element of V;
A59: ((f*decode)|code Free H9).( x".v2)=f.v2 by A11,Lm9;
dom((f*decode)|code Free(H9))={ x".v1, x".v2} & ((f*decode)|code
Free H9).( x".v1)=f.v1 by A6,A9,A10,A27,Lm3,Lm9;
then p={[ x".v1,y],[ x".v2,z]} by A56,A59,Lm16;
then p=d(#)x by Lm15;
hence thesis by A58;
end;
hence thesis by A1,A33,A29,Th10;
end;
end;
theorem Th19:
X is closed_wrt_A1-A7 & E in X implies for H st Diagram(H,E) in
X holds Diagram('not' H,E) in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: E in X;
reconsider m=E as Element of V by A2;
let H such that
A3: Diagram(H,E) in X;
set fs=code Free(H);
A4: fs=code Free('not' H) by ZF_LANG1:60;
now
let p be object;
A5: now
assume p in Diagram('not' H,E);
then consider f such that
A6: p=(f*decode)|fs and
A7: f in St('not' H,E) by A4,Def4;
thus p in Funcs(fs,E) by A6,Lm3;
thus not p in Diagram(H,E)
proof
assume not thesis;
then
ex g being Function of VAR,E st p=(g*decode)|fs & g in St(H,E) by Def4;
then f in St(H,E) by A6,Lm10;
hence contradiction by A7,ZF_MODEL:4;
end;
end;
now
assume that
A8: p in Funcs(fs,E) and
A9: not p in Diagram(H,E);
consider e such that
A10: p=e and
dom e = fs and
rng e c= E by A8,FUNCT_2:def 2;
consider f such that
A11: e=(f*decode)|fs by A8,A10,Lm11;
not f in St(H,E) by A9,A10,A11,Def4;
then Free('not' H)=Free(H) & f in St('not' H,E) by ZF_LANG1:60,ZF_MODEL:4
;
hence p in Diagram('not' H,E) by A10,A11,Def4;
end;
hence p in Diagram('not' H,E) iff p in Funcs(fs,E) & not p in Diagram(H,E)
by A5;
end;
then
A12: Diagram('not' H,E)=Funcs(fs,E)\Diagram(H,E) by XBOOLE_0:def 5;
Funcs(fs,m) in X by A1,A2,Th9;
hence thesis by A1,A3,A12,Th4;
end;
theorem Th20:
X is closed_wrt_A1-A7 & E in X implies for H,H9 st Diagram(H,E)
in X & Diagram(H9,E) in X holds Diagram(H '&' H9,E) in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: E in X;
reconsider E9=E as Element of V by A2;
let H,H9 such that
A3: Diagram(H,E) in X and
A4: Diagram(H9,E) in X;
set fs=code Free(H), fs9=code Free(H9);
reconsider D1=Diagram(H,E),D2=Diagram(H9,E) as Element of V by A3,A4;
A5: (Funcs(fs9\fs,E9)) in X by A1,A2,Th9;
then reconsider F1=Funcs(fs9\fs,E9) as Element of V;
A6: (Funcs(fs\fs9,E9)) in X by A1,A2,Th9;
then reconsider F2=Funcs(fs\fs9,E9) as Element of V;
set A={x \/ y : x in D1 & y in F1}, B={x \/ y : x in D2 & y in F2};
A7: X is closed_wrt_A5 by A1;
then
A8: B in X by A4,A6;
now
let p be object;
assume
A9: p in A /\ B;
then p in A by XBOOLE_0:def 4;
then consider x,y such that
A10: p=x \/ y and
A11: x in D1 and
A12: y in F1;
p in B by A9,XBOOLE_0:def 4;
then consider x9,y9 such that
A13: p=x9 \/ y9 and
A14: x9 in D2 and
A15: y9 in F2;
consider g being Function of VAR,E such that
A16: x9=(g*decode)|fs9 and
A17: g in St(H9,E) by A14,Def4;
consider e such that
A18: y=e and
A19: dom e=fs9\fs and
A20: rng e c= E by A12,FUNCT_2:def 2;
consider f being Function of VAR,E such that
A21: x=(f*decode)|fs and
A22: f in St(H,E) by A11,Def4;
A23: dom((f*decode)|fs)=fs by Lm3;
then reconsider gg=((f*decode)|fs) \/ e as Function by A19,GRFUNC_1:13
,XBOOLE_1:79;
rng gg=rng((f*decode)|fs) \/ rng e by RELAT_1:12;
then
A24: rng gg c= E by A20,XBOOLE_1:8;
dom gg=fs \/ (fs9\fs) by A19,A23,XTUPLE_0:23;
then dom gg=fs \/ fs9 by XBOOLE_1:39;
then gg in Funcs(fs \/ fs9,E) by A24,FUNCT_2:def 2;
then consider ff being Function of VAR,E such that
A25: gg=(ff*decode)|(fs \/ fs9) by Lm11;
now
thus
A26: fs=dom((ff*decode)|fs) & dom((f*decode)|fs)=fs by Lm3;
let q being object such that
A27: q in fs;
((ff*decode)|(fs \/ fs9))= ((ff*decode)|fs) \/ ((ff*decode)|fs9) by
RELAT_1:78;
hence ((ff*decode)|fs).q=((ff*decode)|(fs \/ fs9)).q by A26,A27,
GRFUNC_1:15
.=((f*decode)|fs).q by A25,A26,A27,GRFUNC_1:15;
end;
then
A28: ff in St(H,E) by A22,Lm10,FUNCT_1:2;
now
thus
A29: fs9=dom((ff*decode)|fs9) & dom((g*decode)|fs9)=fs9 by Lm3;
let q being object such that
A30: q in fs9;
((ff*decode)|(fs \/ fs9)) =((ff*decode)|fs) \/ ((ff*decode)|fs9) by
RELAT_1:78;
hence ((ff*decode)|fs9).q=((ff*decode)|(fs \/ fs9)).q by A29,A30,
GRFUNC_1:15
.=((g*decode)|fs9).q by A10,A13,A15,A21,A16,A18,A25,A29,A30,GRFUNC_1:15
;
end;
then ff in St(H9,E) by A17,Lm10,FUNCT_1:2;
then
A31: ff in St(H '&' H9,E) by A28,ZF_MODEL:5;
p=(ff*decode)|code (Free H \/ Free H9) by A10,A21,A18,A25,RELAT_1:120
.=(ff*decode)|code Free(H '&' H9) by ZF_LANG1:61;
hence p in Diagram(H '&' H9,E) by A31,Def4;
end;
then
A32: A /\ B c= Diagram(H '&' H9,E);
Diagram(H '&' H9,E) c= A /\ B
proof
let p be object;
assume p in Diagram(H '&' H9,E);
then consider f being Function of VAR,E such that
A33: p=(f*decode)|code Free(H '&' H9) and
A34: f in St(H '&' H9,E) by Def4;
f in St(H9,E) by A34,ZF_MODEL:5;
then
A35: ((f*decode)|fs9) in D2 by Def4;
then reconsider z=((f*decode)|fs9) as Element of V by A4,Th1;
(f*decode)|(fs\fs9) is Function of fs\fs9,E by FUNCT_2:32;
then
A36: ((f*decode)|(fs\fs9)) in F2 by FUNCT_2:8;
then reconsider t=((f*decode)|(fs\fs9)) as Element of V by A6,Th1;
A37: Free(H '&' H9)=Free(H) \/ Free(H9) by ZF_LANG1:61;
then p=(f*decode)|(fs9 \/ fs) by A33,RELAT_1:120
.=((f*decode)|(fs9 \/ (fs\fs9))) by XBOOLE_1:39
.=((f*decode)|fs9) \/ ((f*decode)|(fs\fs9)) by RELAT_1:78;
then p=z \/ t;
then
A38: p in B by A35,A36;
f in St(H,E) by A34,ZF_MODEL:5;
then
A39: ((f*decode)|fs) in D1 by Def4;
then reconsider x=((f*decode)|fs) as Element of V by A3,Th1;
(f*decode)|(fs9\fs) is Function of fs9\fs,E by FUNCT_2:32;
then
A40: ((f*decode)|(fs9\fs)) in F1 by FUNCT_2:8;
then reconsider y=((f*decode)|(fs9\fs)) as Element of V by A5,Th1;
p=(f*decode)|(fs \/ fs9) by A33,A37,RELAT_1:120
.=((f*decode)|(fs \/ (fs9\fs))) by XBOOLE_1:39
.=((f*decode)|fs) \/ ((f*decode)|(fs9\fs)) by RELAT_1:78;
then p=x \/ y;
then p in A by A39,A40;
hence thesis by A38,XBOOLE_0:def 4;
end;
then
A41: A /\ B = Diagram(H '&' H9,E) by A32;
A in X by A3,A5,A7;
hence thesis by A1,A8,A41,Th5;
end;
theorem Th21:
X is closed_wrt_A1-A7 & E in X implies for H,v1 st Diagram(H,E)
in X holds Diagram(All(v1,H),E) in X
proof
assume that
A1: X is closed_wrt_A1-A7 and
A2: E in X;
let H,v1 such that
A3: Diagram(H,E) in X;
per cases;
suppose
A4: not v1 in Free(H);
then Free(H)=Free(H)\{v1} by ZFMISC_1:57;
then
A5: Free(All(v1,H))=Free(H) by ZF_LANG1:62;
Diagram(All(v1,H),E)=Diagram(H,E)
proof
thus Diagram(All(v1,H),E)c=Diagram(H,E)
proof
let p be object;
assume p in Diagram(All(v1,H),E);
then consider f such that
A6: p=(f*decode)|code Free(All(v1,H)) and
A7: f in St(All(v1,H),E) by Def4;
f in St(H,E) by A7,ZF_MODEL:6;
hence thesis by A5,A6,Def4;
end;
let p be object;
assume p in Diagram(H,E);
then consider f such that
A8: p=(f*decode)|code Free(H) and
A9: f in St(H,E) by Def4;
for g being Function of VAR,E st for v2 st g.v2<>f.v2 holds v1=v2
holds g in St(H,E)
proof
let g be Function of VAR,E;
assume for v2 st g.v2<>f.v2 holds v1=v2;
then
A10: for v2 st v2 in Free(H) holds f.v2=g.v2 by A4;
E,f |= H by A9,ZF_MODEL:def 4;
then E,g |= H by A10,ZF_LANG1:75;
hence thesis by ZF_MODEL:def 4;
end;
then f in St(All(v1,H),E) by A9,ZF_MODEL:6;
hence thesis by A5,A8,Def4;
end;
hence thesis by A3;
end;
suppose
A11: v1 in Free(H);
reconsider m=E as Element of V by A2;
set n= x".v1;
set fs=code Free(H);
A12: Diagram('not' H,E) c= Funcs(fs,E)
proof
let p be object;
assume p in Diagram('not' H,E);
then
A13: ex f being Function of VAR,E st p=(f*decode)|code Free('not' H) & f
in St('not' H,E) by Def4;
Free('not' H)=Free H by ZF_LANG1:60;
hence thesis by A13,Lm3;
end;
A14: fs\{n}=(code Free H)\(code {v1}) by Lm6
.=code((Free H)\{v1}) by Lm1,FUNCT_1:64;
then
A15: fs\{n}=code Free(All(v1,H)) by ZF_LANG1:62;
A16: Diagram('not' H,E) in X by A1,A2,A3,Th19;
then reconsider Dn=Diagram('not' H,E) as Element of V;
set C={x: x in Funcs(fs\{n},m) & ex u st {[n,u]} \/ x in Dn};
A17: Funcs(fs\{n},m) in X by A1,A2,Th9;
{v1}c=Free(H) by A11,ZFMISC_1:31;
then Free(H)=(Free(H)\{v1}) \/ {v1} by XBOOLE_1:45;
then
A18: fs=code(Free(H)\{v1}) \/ code {v1} by RELAT_1:120
.=code(Free(H)\{v1}) \/ {n} by Lm6;
A19: Funcs(fs\{n},m)\C=Diagram(All(v1,H),E)
proof
thus Funcs(fs\{n},m)\C c= Diagram(All(v1,H),E)
proof
let p be object;
assume
A20: p in Funcs(fs\{n},m)\C;
then consider h such that
A21: p=h and
dom h = fs\{n} and
rng h c= E by FUNCT_2:def 2;
consider f such that
A22: h=(f*decode)|(fs\{n}) by A20,A21,Lm11;
A23: not p in C by A20,XBOOLE_0:def 5;
f in St(All(v1,H),E)
proof
assume
A24: not f in St(All(v1,H),E);
A25: for ff being Function of VAR,E st p=(ff*decode)|code Free(All(
v1,H)) holds ff in St(H,E)
proof
let ff be Function of VAR,E;
assume
A26: p=(ff*decode)|code Free(All(v1,H));
(ff*decode)|(fs\{n}) in Funcs(fs\{n},m) by Lm3;
then reconsider x=((ff*decode)|(fs\{n})) as Element of V by A17,Th1
;
assume not ff in St(H,E);
then ff in St('not' H,E) by ZF_MODEL:4;
then (ff*decode)|code Free('not' H) in Dn by Def4;
then ((ff*decode)|((fs\{n}) \/ {n})) in Dn by A18,A14,ZF_LANG1:60;
then
A27: ((ff*decode)|(fs\{n})) \/ ((ff*decode)|{n}) in Dn by RELAT_1:78;
dom((ff*decode)|{n})={n} by Lm3;
then {[n,((ff*decode)|{n}).n]} \/ x in Dn by A27,GRFUNC_1:7;
hence contradiction by A15,A20,A23,A26;
end;
then f in St(H,E) by A15,A21,A22;
then consider e being Function of VAR,E such that
A28: for v2 st e.v2<>f.v2 holds v2=v1 and
A29: not e in St(H,E) by A24,ZF_MODEL:6;
now
thus
A30: fs\{n}=dom((e*decode)|(fs\{n})) & fs\{n}=dom((f*decode)|
(fs\{n})) by Lm3;
let q be object;
assume
A31: q in fs\{n};
then reconsider p99 = q as Element of omega;
A32: q= x".x.card p99 by Lm2;
not q in {n} by A31,XBOOLE_0:def 5;
then
A33: x.card p99 <> v1 by A32,TARSKI:def 1;
thus ((e*decode)|(fs\{n})).q=(e*decode).q by A30,A31,FUNCT_1:47
.=e.(x.card p99) by A32,Lm4
.=f.(x.card p99) by A28,A33
.=(f*decode).q by A32,Lm4
.=((f*decode)|(fs\{n})).q by A30,A31,FUNCT_1:47;
end;
hence contradiction by A15,A21,A22,A25,A29,FUNCT_1:2;
end;
hence thesis by A15,A21,A22,Def4;
end;
let p be object;
assume p in Diagram(All(v1,H),E);
then consider f such that
A34: p=(f*decode)|code Free(All(v1,H)) and
A35: f in St(All(v1,H),E) by Def4;
A36: p in Funcs(fs\{n},m) by A15,A34,Lm3;
then reconsider x=p as Element of V by A17,Th1;
A37: now
A38: fs=code Free('not' H) by ZF_LANG1:60;
given u such that
A39: {[n,u]} \/ x in Dn;
consider h being Function of VAR,E such that
A40: {[n,u]} \/ x=(h*decode)|fs by A12,A39,Lm11;
now
reconsider g={[n,u]} as Function;
thus
A41: dom((h*decode)|(fs\{n}))=(fs\{n}) & dom((f*decode)|(fs\{n}
))=(fs\{n}) by Lm3;
let q be object such that
A42: q in (fs\{n});
((h*decode)|(fs\{n})) c= ((h*decode)|fs) by RELAT_1:75,XBOOLE_1:36;
hence ((h*decode)|(fs\{n})).q=((h*decode)|fs).q by A41,A42,GRFUNC_1:2
.=((f*decode)|(fs\{n})).q by A15,A34,A40,A41,A42,GRFUNC_1:15;
end;
then
A43: h in St(All(v1,H),E) by A15,A35,Lm10,FUNCT_1:2;
ex hh being Function of VAR,E st {[n,u]} \/ x=(hh*decode)|code
Free('not' H) & hh in St('not' H,E) by A39,Def4;
then h in St('not' H,E) by A40,A38,Lm10;
then not h in St(H,E) by ZF_MODEL:4;
hence contradiction by A43,ZF_MODEL:6;
end;
now
assume x in C;
then ex y st y=x & y in Funcs(fs\{n},m) & ex u st {[n,u]} \/ y in Dn;
hence contradiction by A37;
end;
hence thesis by A36,XBOOLE_0:def 5;
end;
n in fs by A11,Lm5;
then C in X by A1,A2,A16,A12,Th11;
hence thesis by A1,A17,A19,Th4;
end;
end;
theorem
X is closed_wrt_A1-A7 & E in X implies Diagram(H,E) in X
proof
defpred P[ZF-formula] means Diagram($1,E) in X;
assume
A1: X is closed_wrt_A1-A7 & E in X;
then
A2: for H st P[H] holds P['not' H] by Th19;
A3: for H,v1 st P[H] holds P[All(v1,H)] by A1,Th21;
A4: for H,H9 st P[H] & P[H9] holds P[H '&' H9] by A1,Th20;
A5: for v1,v2 holds P[v1 '=' v2] & P[v1 'in' v2] by A1,Th18;
for H holds P[H] from ZF_LANG1:sch 1(A5,A2,A4,A3);
hence thesis;
end;
:: Auxiliary theorems
theorem
X is closed_wrt_A1-A7 implies n in X & 0-element_of(V) in X &
1-element_of(V) in X by Lm12,Lm13;
theorem
{[o,p],[p,p]}(#){[p,q]}={[o,q],[p,q]} by Lm14;
theorem
p<>r implies {[o,p],[q,r]}(#){[p,s],[r,t]}={[o,s],[q,t]} by Lm15;
theorem
code {v1} = { x".v1} & code {v1,v2} = { x".v1, x".v2} by Lm6,Lm7;
theorem
for f being Function holds dom f={o,q} iff f={[o,f.o],[q,f.q]} by Lm16;
theorem
dom decode = omega & rng decode = VAR & decode is one-to-one & decode"
is one-to-one & dom(decode") = VAR & rng(decode") = omega by Lm1;
theorem
for A being finite Subset of VAR holds A,code A are_equipotent by Lm8;
theorem
for A being Element of omega holds A = x".x.card A by Lm2;
theorem
dom((f*decode)|fs)=fs & rng((f*decode)|fs) c= E & (f*decode)|fs in
Funcs(fs,E) & dom(f*decode)=omega by Lm3;
theorem
decode.(x".v1)=v1 & (decode").v1= x".v1 & (f*decode).(x".v1)=f.v1 by Lm4;
theorem
for A being finite Subset of VAR holds p in code A iff ex v1 st v1 in
A & p= x".v1 by Lm5;
theorem
for A,B being finite Subset of VAR holds code(A \/ B)=code A \/ code B
& code(A\B)=(code A)\(code B) by Lm1,FUNCT_1:64,RELAT_1:120;
theorem
v1 in Free H implies ((f*decode)|code Free H).( x".v1)=f.v1 by Lm9;
theorem
for f,g being Function of VAR,E st (f*decode)|code Free H=(g*decode)|
code Free H & f in St(H,E) holds g in St(H,E) by Lm10;
theorem
p in Funcs(fs,E) implies ex f st p=(f*decode)|fs by Lm11;