Copyright (c) 2003 Association of Mizar Users
environ
vocabulary MEMBERED, XCMPLX_0, ARYTM, INT_1, ORDINAL2, BOOLE, COMPLEX1, RAT_1,
ORDINAL1, TARSKI, SETFAM_1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, NUMBERS, XCMPLX_0,
XREAL_0, RAT_1, INT_1, ORDINAL1, ORDINAL2;
constructors XCMPLX_0, RAT_1, ENUMSET1, SETFAM_1;
clusters INT_1, NUMBERS, ARYTM_3, XREAL_0, RAT_1, XBOOLE_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions XCMPLX_0, XREAL_0, INT_1, TARSKI, RAT_1, XBOOLE_0;
theorems INT_1, ORDINAL2, XBOOLE_0, XREAL_0, XCMPLX_0, RAT_1, SUBSET_1,
ORDINAL1, TARSKI, ENUMSET1, XBOOLE_1, SETFAM_1, NUMBERS;
schemes XBOOLE_0;
begin
Lm1: 1 = succ 0 .= 0 \/ {0} by ORDINAL1:def 1 .= {0};
reserve x, X, F for set;
definition let X be set;
attr X is complex-membered means
:Def1: x in X implies x is complex;
attr X is real-membered means
:Def2: x in X implies x is real;
attr X is rational-membered means
:Def3: x in X implies x is rational;
attr X is integer-membered means
:Def4: x in X implies x is integer;
attr X is natural-membered means
:Def5: x in X implies x is natural;
end;
definition
cluster natural-membered -> integer-membered set;
coherence
proof let X;
assume
A1: X is natural-membered;
let x;
assume x in X;
then x is natural by A1,Def5;
then x in omega by ORDINAL2:def 21;
hence x is Element of INT by INT_1:14;
end;
cluster integer-membered -> rational-membered set;
coherence
proof let X;
assume
A2: X is integer-membered;
let x;
assume x in X;
then x is integer by A2,Def4;
then x is Element of INT by INT_1:def 2;
then x in INT;
hence x in RAT by RAT_1:11;
end;
cluster rational-membered -> real-membered set;
coherence
proof let X;
assume
A3: X is rational-membered;
let x;
assume x in X;
then x is rational by A3,Def3;
then x in RAT by RAT_1:def 2;
hence x in REAL by RAT_1:4;
end;
cluster real-membered -> complex-membered set;
coherence
proof let X;
assume
A4: X is real-membered;
let x;
assume x in X;
then x is real by A4,Def2;
then x in REAL by XREAL_0:def 1;
hence x in COMPLEX by NUMBERS:11;
end;
end;
definition
cluster non empty natural-membered set;
existence
proof take 1;
thus 1 is non empty;
let x;
assume x in 1;
hence thesis by Lm1,TARSKI:def 1;
end;
end;
definition
cluster -> complex-membered Subset of COMPLEX;
coherence
proof let S be Subset of COMPLEX;
let x;
assume x in S;
hence x is complex by XCMPLX_0:def 2;
end;
cluster -> real-membered Subset of REAL;
coherence
proof let S be Subset of REAL;
let x;
thus thesis by XREAL_0:def 1;
end;
cluster -> rational-membered Subset of RAT;
coherence
proof let S be Subset of RAT;
let x;
thus thesis by RAT_1:def 2;
end;
cluster -> integer-membered Subset of INT;
coherence
proof let S be Subset of INT;
let x;
thus thesis by INT_1:def 2;
end;
cluster -> natural-membered Subset of NAT;
coherence
proof let S be Subset of NAT;
let x;
thus thesis by ORDINAL2:def 21;
end;
end;
definition
cluster COMPLEX -> complex-membered;
coherence
proof let x;
thus thesis by XCMPLX_0:def 2;
end;
cluster REAL -> real-membered;
coherence
proof let x;
thus thesis by XREAL_0:def 1;
end;
cluster RAT -> rational-membered;
coherence
proof let x;
thus thesis by RAT_1:def 2;
end;
cluster INT -> integer-membered;
coherence
proof let x;
thus thesis by INT_1:def 2;
end;
cluster NAT -> natural-membered;
coherence
proof let x;
thus thesis by ORDINAL2:def 21;
end;
end;
theorem Th1:
X is complex-membered implies X c= COMPLEX
proof assume
A1: X is complex-membered;
let x;
assume x in X;
then x is complex by A1,Def1;
hence x in COMPLEX by XCMPLX_0:def 2;
end;
theorem Th2:
X is real-membered implies X c= REAL
proof assume
A1: X is real-membered;
let x;
assume x in X;
then x is real by A1,Def2;
hence x in REAL by XREAL_0:def 1;
end;
theorem Th3:
X is rational-membered implies X c= RAT
proof assume
A1: X is rational-membered;
let x;
assume x in X;
then x is rational by A1,Def3;
hence x in RAT by RAT_1:def 2;
end;
theorem Th4:
X is integer-membered implies X c= INT
proof assume
A1: X is integer-membered;
let x;
assume x in X;
then x is integer by A1,Def4;
then x is Element of INT by INT_1:def 2;
hence x in INT;
end;
theorem Th5:
X is natural-membered implies X c= NAT
proof assume
A1: X is natural-membered;
let x;
assume x in X;
then x is natural by A1,Def5;
hence x in NAT by ORDINAL2:def 21;
end;
definition let X be complex-membered set;
cluster -> complex Element of X;
coherence
proof let e be Element of X;
per cases;
suppose X is empty;
then e = 0 by SUBSET_1:def 2;
hence e is complex;
suppose X is non empty;
hence e is complex by Def1;
end;
end;
definition let X be real-membered set;
cluster -> real Element of X;
coherence
proof let e be Element of X;
per cases;
suppose X is empty;
then e = 0 by SUBSET_1:def 2;
hence e is real;
suppose X is non empty;
hence e is real by Def2;
end;
end;
definition let X be rational-membered set;
cluster -> rational Element of X;
coherence
proof let e be Element of X;
per cases;
suppose X is empty;
then e = 0 by SUBSET_1:def 2;
then e is Element of INT by INT_1:def 2;
then e in INT;
hence e is rational by RAT_1:11,def 2;
suppose X is non empty;
hence e is rational by Def3;
end;
end;
definition let X be integer-membered set;
cluster -> integer Element of X;
coherence
proof let e be Element of X;
per cases;
suppose X is empty;
then e = 0 by SUBSET_1:def 2;
hence e is integer;
suppose X is non empty;
hence e is integer by Def4;
end;
end;
definition let X be natural-membered set;
cluster -> natural Element of X;
coherence
proof let e be Element of X;
per cases;
suppose X is empty;
then e = 0 by SUBSET_1:def 2;
hence e is natural;
suppose X is non empty;
hence e is natural by Def5;
end;
end;
reserve c, c1, c2, c3 for complex number,
r, r1, r2, r3 for real number,
w, w1, w2, w3 for rational number,
i, i1, i2, i3 for integer number,
n, n1, n2, n3 for natural number;
theorem
for X being non empty complex-membered set
ex c st c in X
proof let X be non empty complex-membered set;
consider x being set such that
A1: x in X by XBOOLE_0:def 1;
x is complex number by A1,Def1;
hence thesis by A1;
end;
theorem
for X being non empty real-membered set
ex r st r in X
proof let X be non empty real-membered set;
consider x being set such that
A1: x in X by XBOOLE_0:def 1;
x is real number by A1,Def2;
hence thesis by A1;
end;
theorem
for X being non empty rational-membered set
ex w st w in X
proof let X be non empty rational-membered set;
consider x being set such that
A1: x in X by XBOOLE_0:def 1;
x is rational number by A1,Def3;
hence thesis by A1;
end;
theorem
for X being non empty integer-membered set
ex i st i in X
proof let X be non empty integer-membered set;
consider x being set such that
A1: x in X by XBOOLE_0:def 1;
x is integer number by A1,Def4;
hence thesis by A1;
end;
theorem
for X being non empty natural-membered set
ex n st n in X
proof let X be non empty natural-membered set;
consider x being set such that
A1: x in X by XBOOLE_0:def 1;
x is natural number by A1,Def5;
hence thesis by A1;
end;
theorem
for X being complex-membered set
st for c holds c in X
holds X = COMPLEX
proof let X be complex-membered set such that
A1: for c holds c in X;
thus X c= COMPLEX by Th1;
let e be set;
assume e in COMPLEX;
then e is complex by XCMPLX_0:def 2;
hence e in X by A1;
end;
theorem
for X being real-membered set
st for r holds r in X
holds X = REAL
proof let X be real-membered set such that
A1: for r holds r in X;
thus X c= REAL by Th2;
let e be set;
assume e in REAL;
then e is real by XREAL_0:def 1;
hence e in X by A1;
end;
theorem
for X being rational-membered set
st for w holds w in X
holds X = RAT
proof let X be rational-membered set such that
A1: for w holds w in X;
thus X c= RAT by Th3;
let e be set;
assume e in RAT;
then e is rational by RAT_1:def 2;
hence e in X by A1;
end;
theorem
for X being integer-membered set
st for i holds i in X
holds X = INT
proof let X be integer-membered set such that
A1: for i holds i in X;
thus X c= INT by Th4;
let e be set;
assume e in INT;
then e is integer by INT_1:def 2;
hence e in X by A1;
end;
theorem
for X being natural-membered set
st for n holds n in X
holds X = NAT
proof let X be natural-membered set such that
A1: for n holds n in X;
thus X c= NAT by Th5;
let e be set;
assume e in NAT;
then e is natural by ORDINAL2:def 21;
hence e in X by A1;
end;
theorem Th16:
for Y being complex-membered set st X c= Y
holds X is complex-membered
proof let Y be complex-membered set such that
A1: X c= Y;
let x;
thus thesis by A1,Def1;
end;
theorem Th17:
for Y being real-membered set st X c= Y
holds X is real-membered
proof let Y be real-membered set such that
A1: X c= Y;
let x;
thus thesis by A1,Def2;
end;
theorem Th18:
for Y being rational-membered set st X c= Y
holds X is rational-membered
proof let Y be rational-membered set such that
A1: X c= Y;
let x;
thus thesis by A1,Def3;
end;
theorem Th19:
for Y being integer-membered set st X c= Y
holds X is integer-membered
proof let Y be integer-membered set such that
A1: X c= Y;
let x;
thus thesis by A1,Def4;
end;
theorem Th20:
for Y being natural-membered set st X c= Y
holds X is natural-membered
proof let Y be natural-membered set such that
A1: X c= Y;
let x;
thus thesis by A1,Def5;
end;
definition
cluster {} -> natural-membered;
coherence proof let x; thus thesis; end;
end;
definition
cluster empty -> natural-membered set;
coherence;
end;
definition let c;
cluster {c} -> complex-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 1;
end;
end;
definition let r;
cluster {r} -> real-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 1;
end;
end;
definition let w;
cluster {w} -> rational-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 1;
end;
end;
definition let i;
cluster {i} -> integer-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 1;
end;
end;
definition let n;
cluster {n} -> natural-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 1;
end;
end;
definition let c1,c2;
cluster {c1,c2} -> complex-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 2;
end;
end;
definition let r1,r2;
cluster {r1,r2} -> real-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 2;
end;
end;
definition let w1,w2;
cluster {w1,w2} -> rational-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 2;
end;
end;
definition let i1,i2;
cluster {i1,i2} -> integer-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 2;
end;
end;
definition let n1,n2;
cluster {n1,n2} -> natural-membered;
coherence
proof let e be set;
thus thesis by TARSKI:def 2;
end;
end;
definition let c1,c2,c3;
cluster {c1,c2,c3} -> complex-membered;
coherence
proof let e be set;
thus thesis by ENUMSET1:def 1;
end;
end;
definition let r1,r2,r3;
cluster {r1,r2,r3} -> real-membered;
coherence
proof let e be set;
thus thesis by ENUMSET1:def 1;
end;
end;
definition let w1,w2,w3;
cluster {w1,w2,w3} -> rational-membered;
coherence
proof let e be set;
thus thesis by ENUMSET1:def 1;
end;
end;
definition let i1,i2,i3;
cluster {i1,i2,i3} -> integer-membered;
coherence
proof let e be set;
thus thesis by ENUMSET1:def 1;
end;
end;
definition let n1,n2,n3;
cluster {n1,n2,n3} -> natural-membered;
coherence
proof let e be set;
thus thesis by ENUMSET1:def 1;
end;
end;
definition let X be complex-membered set;
cluster -> complex-membered Subset of X;
coherence
proof let S be Subset of X, x;
thus thesis by Def1;
end;
end;
definition let X be real-membered set;
cluster -> real-membered Subset of X;
coherence
proof let S be Subset of X, x;
thus thesis by Def2;
end;
end;
definition let X be rational-membered set;
cluster -> rational-membered Subset of X;
coherence
proof let S be Subset of X, x;
thus thesis by Def3;
end;
end;
definition let X be integer-membered set;
cluster -> integer-membered Subset of X;
coherence
proof let S be Subset of X, x;
thus thesis by Def4;
end;
end;
definition let X be natural-membered set;
cluster -> natural-membered Subset of X;
coherence
proof let S be Subset of X, x;
thus thesis by Def5;
end;
end;
definition let X,Y be complex-membered set;
cluster X \/ Y -> complex-membered;
coherence
proof let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 2;
hence thesis by Def1;
end;
end;
definition let X,Y be real-membered set;
cluster X \/ Y -> real-membered;
coherence
proof let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 2;
hence thesis by Def2;
end;
end;
definition let X,Y be rational-membered set;
cluster X \/ Y -> rational-membered;
coherence
proof let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 2;
hence thesis by Def3;
end;
end;
definition let X,Y be integer-membered set;
cluster X \/ Y -> integer-membered;
coherence
proof let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 2;
hence thesis by Def4;
end;
end;
definition let X,Y be natural-membered set;
cluster X \/ Y -> natural-membered;
coherence
proof let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 2;
hence thesis by Def5;
end;
end;
definition let X be complex-membered set, Y be set;
cluster X /\ Y -> complex-membered;
coherence
proof X /\ Y c= X by XBOOLE_1:17;
hence thesis by Th16;
end;
cluster Y /\ X -> complex-membered;
coherence
proof Y /\ X c= X by XBOOLE_1:17;
hence thesis by Th16;
end;
end;
definition let X be real-membered set, Y be set;
cluster X /\ Y -> real-membered;
coherence
proof X /\ Y c= X by XBOOLE_1:17;
hence thesis by Th17;
end;
cluster Y /\ X -> real-membered;
coherence
proof Y /\ X c= X by XBOOLE_1:17;
hence thesis by Th17;
end;
end;
definition let X be rational-membered set, Y be set;
cluster X /\ Y -> rational-membered;
coherence
proof X /\ Y c= X by XBOOLE_1:17;
hence thesis by Th18;
end;
cluster Y /\ X -> rational-membered;
coherence
proof Y /\ X c= X by XBOOLE_1:17;
hence thesis by Th18;
end;
end;
definition let X be integer-membered set, Y be set;
cluster X /\ Y -> integer-membered;
coherence
proof X /\ Y c= X by XBOOLE_1:17;
hence thesis by Th19;
end;
cluster Y /\ X -> integer-membered;
coherence
proof Y /\ X c= X by XBOOLE_1:17;
hence thesis by Th19;
end;
end;
definition let X be natural-membered set, Y be set;
cluster X /\ Y -> natural-membered;
coherence
proof X /\ Y c= X by XBOOLE_1:17;
hence thesis by Th20;
end;
cluster Y /\ X -> natural-membered;
coherence
proof Y /\ X c= X by XBOOLE_1:17;
hence thesis by Th20;
end;
end;
definition let X be complex-membered set, Y be set;
cluster X \ Y -> complex-membered;
coherence
proof X \ Y c= X by XBOOLE_1:36;
hence thesis by Th16;
end;
end;
definition let X be real-membered set, Y be set;
cluster X \ Y -> real-membered;
coherence
proof X \ Y c= X by XBOOLE_1:36;
hence thesis by Th17;
end;
end;
definition let X be rational-membered set, Y be set;
cluster X \ Y -> rational-membered;
coherence
proof X \ Y c= X by XBOOLE_1:36;
hence thesis by Th18;
end;
end;
definition let X be integer-membered set, Y be set;
cluster X \ Y -> integer-membered;
coherence
proof X \ Y c= X by XBOOLE_1:36;
hence thesis by Th19;
end;
end;
definition let X be natural-membered set, Y be set;
cluster X \ Y -> natural-membered;
coherence
proof X \ Y c= X by XBOOLE_1:36;
hence thesis by Th20;
end;
end;
definition let X,Y be complex-membered set;
cluster X \+\ Y -> complex-membered;
coherence
proof X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
hence thesis;
end;
end;
definition let X,Y be real-membered set;
cluster X \+\ Y -> real-membered;
coherence
proof X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
hence thesis;
end;
end;
definition let X,Y be rational-membered set;
cluster X \+\ Y -> rational-membered;
coherence
proof X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
hence thesis;
end;
end;
definition let X,Y be integer-membered set;
cluster X \+\ Y -> integer-membered;
coherence
proof X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
hence thesis;
end;
end;
definition let X,Y be natural-membered set;
cluster X \+\ Y -> natural-membered;
coherence
proof X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
hence thesis;
end;
end;
definition let X,Y be complex-membered set;
redefine pred X c= Y means
:Def6: c in X implies c in Y;
compatibility
proof
thus X c= Y implies for c st c in X holds c in Y;
assume
A1: c in X implies c in Y;
let x;
assume
A2: x in X;
then x is complex by Def1;
hence thesis by A1,A2;
end;
end;
definition let X,Y be real-membered set;
redefine pred X c= Y means
:Def7: r in X implies r in Y;
compatibility
proof
thus X c= Y implies for r st r in X holds r in Y;
assume
A1: r in X implies r in Y;
let c;
assume
A2: c in X;
then c is real by Def2;
hence thesis by A1,A2;
end;
end;
definition let X,Y be rational-membered set;
redefine pred X c= Y means
:Def8: w in X implies w in Y;
compatibility
proof
thus X c= Y implies for w st w in X holds w in Y;
assume
A1: w in X implies w in Y;
let r;
assume
A2: r in X;
then r is rational by Def3;
hence thesis by A1,A2;
end;
end;
definition let X,Y be integer-membered set;
redefine pred X c= Y means
:Def9: i in X implies i in Y;
compatibility
proof
thus X c= Y implies for i st i in X holds i in Y;
assume
A1: i in X implies i in Y;
let w;
assume
A2: w in X;
then w is integer by Def4;
hence thesis by A1,A2;
end;
end;
definition let X,Y be natural-membered set;
redefine pred X c= Y means
:Def10: n in X implies n in Y;
compatibility
proof
thus X c= Y implies for n st n in X holds n in Y;
assume
A1: n in X implies n in Y;
let i;
assume
A2: i in X;
then i is natural by Def5;
hence thesis by A1,A2;
end;
end;
definition let X,Y be complex-membered set;
redefine pred X = Y means
c in X iff c in Y;
compatibility
proof
thus X = Y implies for c holds c in X iff c in Y;
assume c in X iff c in Y;
hence X c= Y & Y c= X by Def6;
end;
end;
definition let X,Y be real-membered set;
redefine pred X = Y means
r in X iff r in Y;
compatibility
proof
thus X = Y implies for r holds r in X iff r in Y;
assume r in X iff r in Y;
then X c= Y & Y c= X by Def7;
hence thesis by XBOOLE_0:def 10;
end;
end;
definition let X,Y be rational-membered set;
redefine pred X = Y means
w in X iff w in Y;
compatibility
proof
thus X = Y implies for w holds w in X iff w in Y;
assume w in X iff w in Y;
then X c= Y & Y c= X by Def8;
hence thesis by XBOOLE_0:def 10;
end;
end;
definition let X,Y be integer-membered set;
redefine pred X = Y means
i in X iff i in Y;
compatibility
proof
thus X = Y implies for i holds i in X iff i in Y;
assume i in X iff i in Y;
then X c= Y & Y c= X by Def9;
hence thesis by XBOOLE_0:def 10;
end;
end;
definition let X,Y be natural-membered set;
redefine pred X = Y means
n in X iff n in Y;
compatibility
proof
thus X = Y implies for n holds n in X iff n in Y;
assume n in X iff n in Y;
then X c= Y & Y c= X by Def10;
hence thesis by XBOOLE_0:def 10;
end;
end;
definition let X,Y be complex-membered set;
redefine pred X meets Y means
ex c st c in X & c in Y;
compatibility
proof
thus X misses Y implies not ex c st c in X & c in Y by XBOOLE_0:3;
assume
A1: not ex c st c in X & c in Y;
assume X meets Y;
then consider x such that
A2: x in X & x in Y by XBOOLE_0:3;
x is complex by A2,Def1;
hence thesis by A1,A2;
end;
end;
definition let X,Y be real-membered set;
redefine pred X meets Y means
ex r st r in X & r in Y;
compatibility
proof
thus X misses Y implies not ex r st r in X & r in Y by XBOOLE_0:3;
assume
A1: not ex r st r in X & r in Y;
assume X meets Y;
then consider x such that
A2: x in X & x in Y by XBOOLE_0:3;
x is real by A2,Def2;
hence thesis by A1,A2;
end;
end;
definition let X,Y be rational-membered set;
redefine pred X meets Y means
ex w st w in X & w in Y;
compatibility
proof
thus X misses Y implies not ex w st w in X & w in Y by XBOOLE_0:3;
assume
A1: not ex w st w in X & w in Y;
assume X meets Y;
then consider x such that
A2: x in X & x in Y by XBOOLE_0:3;
x is rational by A2,Def3;
hence thesis by A1,A2;
end;
end;
definition let X,Y be integer-membered set;
redefine pred X meets Y means
ex i st i in X & i in Y;
compatibility
proof
thus X misses Y implies not ex i st i in X & i in Y by XBOOLE_0:3;
assume
A1: not ex i st i in X & i in Y;
assume X meets Y;
then consider x such that
A2: x in X & x in Y by XBOOLE_0:3;
x is integer by A2,Def4;
hence thesis by A1,A2;
end;
end;
definition let X,Y be natural-membered set;
redefine pred X meets Y means
ex n st n in X & n in Y;
compatibility
proof
thus X misses Y implies not ex n st n in X & n in Y by XBOOLE_0:3;
assume
A1: not ex n st n in X & n in Y;
assume X meets Y;
then consider x such that
A2: x in X & x in Y by XBOOLE_0:3;
x is natural by A2,Def5;
hence thesis by A1,A2;
end;
end;
theorem
(for X st X in F holds X is complex-membered)
implies union F is complex-membered
proof assume
A1: for X st X in F holds X is complex-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is complex-membered by A1,A3;
hence x is complex by A2,Def1;
end;
theorem
(for X st X in F holds X is real-membered)
implies union F is real-membered
proof assume
A1: for X st X in F holds X is real-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is real-membered by A1,A3;
hence x is real by A2,Def2;
end;
theorem
(for X st X in F holds X is rational-membered)
implies union F is rational-membered
proof assume
A1: for X st X in F holds X is rational-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is rational-membered by A1,A3;
hence x is rational by A2,Def3;
end;
theorem
(for X st X in F holds X is integer-membered)
implies union F is integer-membered
proof assume
A1: for X st X in F holds X is integer-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is integer-membered by A1,A3;
hence x is integer by A2,Def4;
end;
theorem
(for X st X in F holds X is natural-membered)
implies union F is natural-membered
proof assume
A1: for X st X in F holds X is natural-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is natural-membered by A1,A3;
hence x is natural by A2,Def5;
end;
theorem
for X st X in F & X is complex-membered
holds meet F is complex-membered
proof let X;
assume X in F;
then meet F c= X by SETFAM_1:4;
hence thesis by Th16;
end;
theorem
for X st X in F & X is real-membered
holds meet F is real-membered
proof let X;
assume X in F;
then meet F c= X by SETFAM_1:4;
hence thesis by Th17;
end;
theorem
for X st X in F & X is rational-membered
holds meet F is rational-membered
proof let X;
assume X in F;
then meet F c= X by SETFAM_1:4;
hence thesis by Th18;
end;
theorem
for X st X in F & X is integer-membered
holds meet F is integer-membered
proof let X;
assume X in F;
then meet F c= X by SETFAM_1:4;
hence thesis by Th19;
end;
theorem
for X st X in F & X is natural-membered
holds meet F is natural-membered
proof let X;
assume X in F;
then meet F c= X by SETFAM_1:4;
hence thesis by Th20;
end;
scheme CM_Separation {P[set]}:
ex X being complex-membered set st
for c holds c in X iff P[c]
proof
defpred _P[set] means P[$1];
consider X being set such that
A1: x in X iff x in COMPLEX & _P[x] from Separation;
X is complex-membered
proof let x;
assume x in X;
then x in COMPLEX by A1;
hence thesis by XCMPLX_0:def 2;
end;
then reconsider X as complex-membered set;
take X; let c;
c in COMPLEX by XCMPLX_0:def 2;
hence thesis by A1;
end;
scheme RM_Separation {P[set]}:
ex X being real-membered set st
for r holds r in X iff P[r]
proof
defpred _P[set] means P[$1];
consider X being set such that
A1: x in X iff x in REAL & _P[x] from Separation;
X is real-membered
proof let x;
assume x in X;
then x in REAL by A1;
hence thesis by XREAL_0:def 1;
end;
then reconsider X as real-membered set;
take X; let r;
r in REAL by XREAL_0:def 1;
hence thesis by A1;
end;
scheme WM_Separation {P[set]}:
ex X being rational-membered set st
for w holds w in X iff P[w]
proof
defpred _P[set] means P[$1];
consider X being set such that
A1: x in X iff x in RAT & _P[x] from Separation;
X is rational-membered
proof let x;
assume x in X;
then x in RAT by A1;
hence thesis by RAT_1:def 2;
end;
then reconsider X as rational-membered set;
take X; let w;
w in RAT by RAT_1:def 2;
hence thesis by A1;
end;
scheme IM_Separation {P[set]}:
ex X being integer-membered set st
for i holds i in X iff P[i]
proof
defpred _P[set] means P[$1];
consider X being set such that
A1: x in X iff x in INT & _P[x] from Separation;
X is integer-membered
proof let x;
assume x in X;
then x in INT by A1;
hence thesis by INT_1:def 2;
end;
then reconsider X as integer-membered set;
take X; let i;
i in INT by INT_1:12;
hence thesis by A1;
end;
scheme NM_Separation {P[set]}:
ex X being natural-membered set st
for n holds n in X iff P[n]
proof
defpred _P[set] means P[$1];
consider X being set such that
A1: x in X iff x in NAT & _P[x] from Separation;
X is natural-membered
proof let x;
assume x in X;
then x in NAT by A1;
hence thesis by ORDINAL2:def 21;
end;
then reconsider X as natural-membered set;
take X; let n;
n in NAT by ORDINAL2:def 21;
hence thesis by A1;
end;