The abstract of the Mizar article:

On the Sets Inhabited by Numbers

by

Andrzej Trybulec

Received August 23, 2003

MML identifier: MEMBERED

[ Mizar article, MML identifier index ]

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;


begin

reserve x, X, F for set;

definition let X be set;
 attr X is complex-membered means
:: MEMBERED:def 1
 x in X implies x is complex;
 attr X is real-membered means
:: MEMBERED:def 2
 x in X implies x is real;
 attr X is rational-membered means
:: MEMBERED:def 3
 x in X implies x is rational;
 attr X is integer-membered means
:: MEMBERED:def 4
 x in X implies x is integer;
 attr X is natural-membered means
:: MEMBERED:def 5
 x in X implies x is natural;
end;

definition
 cluster natural-membered -> integer-membered set;
 cluster integer-membered -> rational-membered set;
 cluster rational-membered -> real-membered set;
 cluster real-membered -> complex-membered set;
end;

definition
 cluster non empty natural-membered set;
end;

definition
 cluster -> complex-membered Subset of COMPLEX;
 cluster -> real-membered Subset of REAL;
 cluster -> rational-membered Subset of RAT;
 cluster -> integer-membered Subset of INT;
 cluster -> natural-membered Subset of NAT;
end;

definition
 cluster COMPLEX -> complex-membered;
 cluster REAL -> real-membered;
 cluster RAT -> rational-membered;
 cluster INT -> integer-membered;
 cluster NAT -> natural-membered;
end;

theorem :: MEMBERED:1
 X is complex-membered implies X c= COMPLEX;

theorem :: MEMBERED:2
 X is real-membered implies X c= REAL;

theorem :: MEMBERED:3
 X is rational-membered implies X c= RAT;

theorem :: MEMBERED:4
 X is integer-membered implies X c= INT;

theorem :: MEMBERED:5
 X is natural-membered implies X c= NAT;

definition let X be complex-membered set;
 cluster -> complex Element of X;
end;

definition let X be real-membered set;
 cluster -> real Element of X;
end;

definition let X be rational-membered set;
 cluster -> rational Element of X;
end;

definition let X be integer-membered set;
 cluster -> integer Element of X;
end;

definition let X be natural-membered set;
 cluster -> natural Element of X;
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 :: MEMBERED:6
 for X being non empty complex-membered set
  ex c st c in X;

theorem :: MEMBERED:7
 for X being non empty real-membered set
  ex r st r in X;

theorem :: MEMBERED:8
 for X being non empty rational-membered set
  ex w st w in X;

theorem :: MEMBERED:9
 for X being non empty integer-membered set
  ex i st i in X;

theorem :: MEMBERED:10
 for X being non empty natural-membered set
  ex n st n in X;

theorem :: MEMBERED:11
 for X being complex-membered set
  st for c holds c in X
 holds X = COMPLEX;

theorem :: MEMBERED:12
 for X being real-membered set
  st for r holds r in X
 holds X = REAL;

theorem :: MEMBERED:13
 for X being rational-membered set
  st for w holds w in X
 holds X = RAT;

theorem :: MEMBERED:14
 for X being integer-membered set
  st for i holds i in X
 holds X = INT;

theorem :: MEMBERED:15
 for X being natural-membered set
  st for n holds n in X
 holds X = NAT;

theorem :: MEMBERED:16
 for Y being complex-membered set st X c= Y
  holds X is complex-membered;

theorem :: MEMBERED:17
 for Y being real-membered set st X c= Y
  holds X is real-membered;

theorem :: MEMBERED:18
 for Y being rational-membered set st X c= Y
  holds X is rational-membered;

theorem :: MEMBERED:19
 for Y being integer-membered set st X c= Y
  holds X is integer-membered;

theorem :: MEMBERED:20
 for Y being natural-membered set st X c= Y
  holds X is natural-membered;

definition
 cluster {} -> natural-membered;
end;

definition
 cluster empty -> natural-membered set;
end;

definition let c;
 cluster {c} -> complex-membered;
end;

definition let r;
 cluster {r} -> real-membered;
end;

definition let w;
 cluster {w} -> rational-membered;
end;

definition let i;
 cluster {i} -> integer-membered;
end;

definition let n;
 cluster {n} -> natural-membered;
end;

definition let c1,c2;
 cluster {c1,c2} -> complex-membered;
end;

definition let r1,r2;
 cluster {r1,r2} -> real-membered;
end;

definition let w1,w2;
 cluster {w1,w2} -> rational-membered;
end;

definition let i1,i2;
 cluster {i1,i2} -> integer-membered;
end;

definition let n1,n2;
 cluster {n1,n2} -> natural-membered;
end;

definition let c1,c2,c3;
 cluster {c1,c2,c3} -> complex-membered;
end;

definition let r1,r2,r3;
 cluster {r1,r2,r3} -> real-membered;
end;

definition let w1,w2,w3;
 cluster {w1,w2,w3} -> rational-membered;
end;

definition let i1,i2,i3;
 cluster {i1,i2,i3} -> integer-membered;
end;

definition let n1,n2,n3;
 cluster {n1,n2,n3} -> natural-membered;
end;

definition let X be complex-membered set;
 cluster -> complex-membered Subset of X;
end;

definition let X be real-membered set;
 cluster -> real-membered Subset of X;
end;

definition let X be rational-membered set;
 cluster -> rational-membered Subset of X;
end;

definition let X be integer-membered set;
 cluster -> integer-membered Subset of X;
end;

definition let X be natural-membered set;
 cluster -> natural-membered Subset of X;
end;

definition let X,Y be complex-membered set;
 cluster X \/ Y -> complex-membered;
end;

definition let X,Y be real-membered set;
 cluster X \/ Y -> real-membered;
end;

definition let X,Y be rational-membered set;
 cluster X \/ Y -> rational-membered;
end;

definition let X,Y be integer-membered set;
 cluster X \/ Y -> integer-membered;
end;

definition let X,Y be natural-membered set;
 cluster X \/ Y -> natural-membered;
end;

definition let X be complex-membered set, Y be set;
 cluster X /\ Y -> complex-membered;
 cluster Y /\ X -> complex-membered;
end;

definition let X be real-membered set, Y be set;
 cluster X /\ Y -> real-membered;
 cluster Y /\ X -> real-membered;
end;

definition let X be rational-membered set, Y be set;
 cluster X /\ Y -> rational-membered;
 cluster Y /\ X -> rational-membered;
end;

definition let X be integer-membered set, Y be set;
 cluster X /\ Y -> integer-membered;
 cluster Y /\ X -> integer-membered;
end;

definition let X be natural-membered set, Y be set;
 cluster X /\ Y -> natural-membered;
 cluster Y /\ X -> natural-membered;
end;

definition let X be complex-membered set, Y be set;
 cluster X \ Y -> complex-membered;
end;

definition let X be real-membered set, Y be set;
 cluster X \ Y -> real-membered;
end;

definition let X be rational-membered set, Y be set;
 cluster X \ Y -> rational-membered;
end;

definition let X be integer-membered set, Y be set;
 cluster X \ Y -> integer-membered;
end;

definition let X be natural-membered set, Y be set;
 cluster X \ Y -> natural-membered;
end;

definition let X,Y be complex-membered set;
 cluster X \+\ Y -> complex-membered;
end;

definition let X,Y be real-membered set;
 cluster X \+\ Y -> real-membered;
end;

definition let X,Y be rational-membered set;
 cluster X \+\ Y -> rational-membered;
end;

definition let X,Y be integer-membered set;
 cluster X \+\ Y -> integer-membered;
end;

definition let X,Y be natural-membered set;
 cluster X \+\ Y -> natural-membered;
end;

definition let X,Y be complex-membered set;
 redefine pred X c= Y means
:: MEMBERED:def 6
 c in X implies c in Y;
end;

definition let X,Y be real-membered set;
 redefine pred X c= Y means
:: MEMBERED:def 7
 r in X implies r in Y;
end;

definition let X,Y be rational-membered set;
 redefine pred X c= Y means
:: MEMBERED:def 8
 w in X implies w in Y;
end;

definition let X,Y be integer-membered set;
 redefine pred X c= Y means
:: MEMBERED:def 9
 i in X implies i in Y;
end;

definition let X,Y be natural-membered set;
 redefine pred X c= Y means
:: MEMBERED:def 10
 n in X implies n in Y;
end;

definition let X,Y be complex-membered set;
 redefine pred X = Y means
:: MEMBERED:def 11
   c in X iff c in Y;
end;

definition let X,Y be real-membered set;
 redefine pred X = Y means
:: MEMBERED:def 12
   r in X iff r in Y;
end;

definition let X,Y be rational-membered set;
 redefine pred X = Y means
:: MEMBERED:def 13
   w in X iff w in Y;
end;

definition let X,Y be integer-membered set;
 redefine pred X = Y means
:: MEMBERED:def 14
   i in X iff i in Y;
end;

definition let X,Y be natural-membered set;
 redefine pred X = Y means
:: MEMBERED:def 15
   n in X iff n in Y;
end;

definition let X,Y be complex-membered set;
 redefine pred X meets Y means
:: MEMBERED:def 16
   ex c st c in X & c in Y;
end;

definition let X,Y be real-membered set;
 redefine pred X meets Y means
:: MEMBERED:def 17
   ex r st r in X & r in Y;
end;

definition let X,Y be rational-membered set;
 redefine pred X meets Y means
:: MEMBERED:def 18
   ex w st w in X & w in Y;
end;

definition let X,Y be integer-membered set;
 redefine pred X meets Y means
:: MEMBERED:def 19
   ex i st i in X & i in Y;
end;

definition let X,Y be natural-membered set;
 redefine pred X meets Y means
:: MEMBERED:def 20
   ex n st n in X & n in Y;
end;

theorem :: MEMBERED:21
 (for X st X in F holds X is complex-membered)
   implies union F is complex-membered;

theorem :: MEMBERED:22
 (for X st X in F holds X is real-membered)
   implies union F is real-membered;

theorem :: MEMBERED:23
 (for X st X in F holds X is rational-membered)
   implies union F is rational-membered;

theorem :: MEMBERED:24
 (for X st X in F holds X is integer-membered)
   implies union F is integer-membered;

theorem :: MEMBERED:25
 (for X st X in F holds X is natural-membered)
   implies union F is natural-membered;

theorem :: MEMBERED:26
 for X st X in F & X is complex-membered
  holds meet F is complex-membered;

theorem :: MEMBERED:27
 for X st X in F & X is real-membered
  holds meet F is real-membered;

theorem :: MEMBERED:28
 for X st X in F & X is rational-membered
  holds meet F is rational-membered;

theorem :: MEMBERED:29
 for X st X in F & X is integer-membered
  holds meet F is integer-membered;

theorem :: MEMBERED:30
 for X st X in F & X is natural-membered
  holds meet F is natural-membered;

scheme CM_Separation {P[set]}:
 ex X being complex-membered set st
  for c holds c in X iff P[c];

scheme RM_Separation {P[set]}:
 ex X being real-membered set st
  for r holds r in X iff P[r];

scheme WM_Separation {P[set]}:
 ex X being rational-membered set st
  for w holds w in X iff P[w];

scheme IM_Separation {P[set]}:
 ex X being integer-membered set st
  for i holds i in X iff P[i];

scheme NM_Separation {P[set]}:
 ex X being natural-membered set st
  for n holds n in X iff P[n];