domain_1.miz
begin
reserve a,b,c,d for
set,
D,X1,X2,X3,X4 for non
empty
set,
x1,y1,z1 for
Element of X1,
x2 for
Element of X2,
x3 for
Element of X3,
x4 for
Element of X4,
A1,B1 for
Subset of X1;
theorem ::
DOMAIN_1:1
a
in
[:X1, X2:] implies ex x1, x2 st a
=
[x1, x2]
proof
assume a
in
[:X1, X2:];
then
consider x1,x2 be
object such that
A1: x1
in X1 and
A2: x2
in X2 and
A3: a
=
[x1, x2] by
ZFMISC_1:def 2;
reconsider x2 as
Element of X2 by
A2;
reconsider x1 as
Element of X1 by
A1;
take x1, x2;
thus thesis by
A3;
end;
theorem ::
DOMAIN_1:2
for x,y be
Element of
[:X1, X2:] st (x
`1 )
= (y
`1 ) & (x
`2 )
= (y
`2 ) holds x
= y
proof
let x,y be
Element of
[:X1, X2:];
[(x
`1 ), (x
`2 )]
= x;
hence thesis by
MCART_1: 21;
end;
definition
let X1, X2, x1, x2;
:: original:
[
redefine
func
[x1,x2] ->
Element of
[:X1, X2:] ;
coherence by
ZFMISC_1: 87;
end
definition
let X1, X2;
let x be
Element of
[:X1, X2:];
:: original:
`1
redefine
func x
`1 ->
Element of X1 ;
coherence by
MCART_1: 10;
:: original:
`2
redefine
func x
`2 ->
Element of X2 ;
coherence by
MCART_1: 10;
end
theorem ::
DOMAIN_1:3
Th3: a
in
[:X1, X2, X3:] iff ex x1, x2, x3 st a
=
[x1, x2, x3]
proof
thus a
in
[:X1, X2, X3:] implies ex x1, x2, x3 st a
=
[x1, x2, x3]
proof
assume a
in
[:X1, X2, X3:];
then a
in
[:
[:X1, X2:], X3:] by
ZFMISC_1:def 3;
then
consider x12,x3 be
object such that
A1: x12
in
[:X1, X2:] and
A2: x3
in X3 and
A3: a
=
[x12, x3] by
ZFMISC_1:def 2;
reconsider x3 as
Element of X3 by
A2;
consider x1,x2 be
object such that
A4: x1
in X1 and
A5: x2
in X2 and
A6: x12
=
[x1, x2] by
A1,
ZFMISC_1:def 2;
reconsider x2 as
Element of X2 by
A5;
reconsider x1 as
Element of X1 by
A4;
a
=
[x1, x2, x3] by
A3,
A6;
hence thesis;
end;
given x1, x2, x3 such that
A7: a
=
[x1, x2, x3];
a
=
[
[x1, x2], x3] by
A7;
then a
in
[:
[:X1, X2:], X3:];
hence thesis by
ZFMISC_1:def 3;
end;
theorem ::
DOMAIN_1:4
Th4: (for a holds a
in D iff ex x1, x2, x3 st a
=
[x1, x2, x3]) implies D
=
[:X1, X2, X3:]
proof
assume
A1: for a holds a
in D iff ex x1, x2, x3 st a
=
[x1, x2, x3];
now
let a be
object;
thus a
in D implies a
in
[:
[:X1, X2:], X3:]
proof
assume a
in D;
then
consider x1, x2, x3 such that
A2: a
=
[x1, x2, x3] by
A1;
a
=
[
[x1, x2], x3] by
A2;
hence thesis;
end;
assume a
in
[:
[:X1, X2:], X3:];
then
consider x12,x3 be
object such that
A3: x12
in
[:X1, X2:] and
A4: x3
in X3 and
A5: a
=
[x12, x3] by
ZFMISC_1:def 2;
reconsider x3 as
Element of X3 by
A4;
consider x1,x2 be
object such that
A6: x1
in X1 and
A7: x2
in X2 and
A8: x12
=
[x1, x2] by
A3,
ZFMISC_1:def 2;
reconsider x2 as
Element of X2 by
A7;
reconsider x1 as
Element of X1 by
A6;
a
=
[x1, x2, x3] by
A5,
A8;
hence a
in D by
A1;
end;
then D
=
[:
[:X1, X2:], X3:] by
TARSKI: 2;
hence thesis by
ZFMISC_1:def 3;
end;
theorem ::
DOMAIN_1:5
D
=
[:X1, X2, X3:] iff for a holds a
in D iff ex x1, x2, x3 st a
=
[x1, x2, x3] by
Th3,
Th4;
reserve x,y for
Element of
[:X1, X2, X3:];
definition
let X1, X2, X3, x1, x2, x3;
:: original:
[
redefine
func
[x1,x2,x3] ->
Element of
[:X1, X2, X3:] ;
coherence by
MCART_1: 69;
end
theorem ::
DOMAIN_1:6
a
= (x
`1_3 ) iff for x1, x2, x3 st x
=
[x1, x2, x3] holds a
= x1 by
MCART_1: 65;
theorem ::
DOMAIN_1:7
b
= (x
`2_3 ) iff for x1, x2, x3 st x
=
[x1, x2, x3] holds b
= x2 by
MCART_1: 66;
theorem ::
DOMAIN_1:8
c
= (x
`3_3 ) iff for x1, x2, x3 st x
=
[x1, x2, x3] holds c
= x3 by
MCART_1: 67;
AA: for X1,X2,X3 be non
empty
set holds for x be
Element of
[:X1, X2, X3:] holds x
=
[(x
`1_3 ), (x
`2_3 ), (x
`3_3 )];
theorem ::
DOMAIN_1:9
(x
`1_3 )
= (y
`1_3 ) & (x
`2_3 )
= (y
`2_3 ) & (x
`3_3 )
= (y
`3_3 ) implies x
= y
proof
[(x
`1_3 ), (x
`2_3 ), (x
`3_3 )]
= x;
hence thesis by
AA;
end;
theorem ::
DOMAIN_1:10
Th10: a
in
[:X1, X2, X3, X4:] iff ex x1, x2, x3, x4 st a
=
[x1, x2, x3, x4]
proof
thus a
in
[:X1, X2, X3, X4:] implies ex x1, x2, x3, x4 st a
=
[x1, x2, x3, x4]
proof
assume a
in
[:X1, X2, X3, X4:];
then a
in
[:
[:X1, X2, X3:], X4:] by
ZFMISC_1:def 4;
then
consider x123,x4 be
object such that
A1: x123
in
[:X1, X2, X3:] and
A2: x4
in X4 and
A3: a
=
[x123, x4] by
ZFMISC_1:def 2;
reconsider x4 as
Element of X4 by
A2;
consider x1 be
Element of X1, x2 be
Element of X2, x3 be
Element of X3 such that
A4: x123
=
[x1, x2, x3] by
A1,
Th3;
a
=
[x1, x2, x3, x4] by
A3,
A4;
hence thesis;
end;
given x1, x2, x3, x4 such that
A5: a
=
[x1, x2, x3, x4];
a
=
[
[x1, x2, x3], x4] by
A5;
then a
in
[:
[:X1, X2, X3:], X4:];
hence thesis by
ZFMISC_1:def 4;
end;
theorem ::
DOMAIN_1:11
Th11: (for a holds a
in D iff ex x1, x2, x3, x4 st a
=
[x1, x2, x3, x4]) implies D
=
[:X1, X2, X3, X4:]
proof
assume
A1: for a holds a
in D iff ex x1, x2, x3, x4 st a
=
[x1, x2, x3, x4];
now
let a be
object;
thus a
in D implies a
in
[:
[:X1, X2, X3:], X4:]
proof
assume a
in D;
then
consider x1, x2, x3, x4 such that
A2: a
=
[x1, x2, x3, x4] by
A1;
a
=
[
[x1, x2, x3], x4] by
A2;
hence thesis;
end;
assume a
in
[:
[:X1, X2, X3:], X4:];
then
consider x123,x4 be
object such that
A3: x123
in
[:X1, X2, X3:] and
A4: x4
in X4 and
A5: a
=
[x123, x4] by
ZFMISC_1:def 2;
reconsider x4 as
Element of X4 by
A4;
consider x1, x2, x3 such that
A6: x123
=
[x1, x2, x3] by
A3,
Th3;
a
=
[x1, x2, x3, x4] by
A5,
A6;
hence a
in D by
A1;
end;
then D
=
[:
[:X1, X2, X3:], X4:] by
TARSKI: 2;
hence thesis by
ZFMISC_1:def 4;
end;
theorem ::
DOMAIN_1:12
D
=
[:X1, X2, X3, X4:] iff for a holds a
in D iff ex x1, x2, x3, x4 st a
=
[x1, x2, x3, x4] by
Th10,
Th11;
reserve x for
Element of
[:X1, X2, X3, X4:];
definition
let X1, X2, X3, X4, x1, x2, x3, x4;
:: original:
[
redefine
func
[x1,x2,x3,x4] ->
Element of
[:X1, X2, X3, X4:] ;
coherence by
MCART_1: 80;
end
theorem ::
DOMAIN_1:13
a
= (x
`1_4 ) iff for x1, x2, x3, x4 st x
=
[x1, x2, x3, x4] holds a
= x1 by
MCART_1: 75;
theorem ::
DOMAIN_1:14
b
= (x
`2_4 ) iff for x1, x2, x3, x4 st x
=
[x1, x2, x3, x4] holds b
= x2 by
MCART_1: 76;
theorem ::
DOMAIN_1:15
c
= (x
`3_4 ) iff for x1, x2, x3, x4 st x
=
[x1, x2, x3, x4] holds c
= x3 by
MCART_1: 77;
theorem ::
DOMAIN_1:16
d
= (x
`4_4 ) iff for x1, x2, x3, x4 st x
=
[x1, x2, x3, x4] holds d
= x4 by
MCART_1: 78;
AB: for X1,X2,X3,X4 be non
empty
set holds for x be
Element of
[:X1, X2, X3, X4:] holds x
=
[(x
`1_4 ), (x
`2_4 ), (x
`3_4 ), (x
`4_4 )];
theorem ::
DOMAIN_1:17
for x,y be
Element of
[:X1, X2, X3, X4:] st (x
`1_4 )
= (y
`1_4 ) & (x
`2_4 )
= (y
`2_4 ) & (x
`3_4 )
= (y
`3_4 ) & (x
`4_4 )
= (y
`4_4 ) holds x
= y
proof
let x,y be
Element of
[:X1, X2, X3, X4:];
[(x
`1_4 ), (x
`2_4 ), (x
`3_4 ), (x
`4_4 )]
= x;
hence thesis by
AB;
end;
reserve A2 for
Subset of X2,
A3 for
Subset of X3,
A4 for
Subset of X4;
scheme ::
DOMAIN_1:sch1
Fraenkel1 { P[
object] } :
for X1 holds { x1 : P[x1] } is
Subset of X1;
let X1;
{ x1 : P[x1] }
c= X1
proof
let a be
object;
assume a
in { x1 : P[x1] };
then ex x1 st a
= x1 & P[x1];
hence thesis;
end;
hence thesis;
end;
scheme ::
DOMAIN_1:sch2
Fraenkel2 { P[
object,
object] } :
for X1, X2 holds {
[x1, x2] : P[x1, x2] } is
Subset of
[:X1, X2:];
let X1, X2;
{
[x1, x2] : P[x1, x2] }
c=
[:X1, X2:]
proof
let a be
object;
assume a
in {
[x1, x2] : P[x1, x2] };
then ex x1, x2 st a
=
[x1, x2] & P[x1, x2];
hence thesis;
end;
hence thesis;
end;
scheme ::
DOMAIN_1:sch3
Fraenkel3 { P[
object,
object,
object] } :
for X1, X2, X3 holds {
[x1, x2, x3] : P[x1, x2, x3] } is
Subset of
[:X1, X2, X3:];
let X1, X2, X3;
{
[x1, x2, x3] : P[x1, x2, x3] }
c=
[:X1, X2, X3:]
proof
let a be
object;
assume a
in {
[x1, x2, x3] : P[x1, x2, x3] };
then ex x1, x2, x3 st a
=
[x1, x2, x3] & P[x1, x2, x3];
hence thesis;
end;
hence thesis;
end;
scheme ::
DOMAIN_1:sch4
Fraenkel4 { P[
object,
object,
object,
object] } :
for X1, X2, X3, X4 holds {
[x1, x2, x3, x4] : P[x1, x2, x3, x4] } is
Subset of
[:X1, X2, X3, X4:];
let X1, X2, X3, X4;
{
[x1, x2, x3, x4] : P[x1, x2, x3, x4] }
c=
[:X1, X2, X3, X4:]
proof
let a be
object;
assume a
in {
[x1, x2, x3, x4] : P[x1, x2, x3, x4] };
then ex x1, x2, x3, x4 st a
=
[x1, x2, x3, x4] & P[x1, x2, x3, x4];
hence thesis;
end;
hence thesis;
end;
scheme ::
DOMAIN_1:sch5
Fraenkel5 { P,Q[
object] } :
for X1 st for x1 holds P[x1] implies Q[x1] holds { y1 : P[y1] }
c= { z1 : Q[z1] };
let X1 such that
A1: P[x1] implies Q[x1];
let a be
object;
assume a
in { x1 : P[x1] };
then
consider x1 such that
A2: a
= x1 and
A3: P[x1];
Q[x1] by
A1,
A3;
hence thesis by
A2;
end;
scheme ::
DOMAIN_1:sch6
Fraenkel6 { P,Q[
object] } :
for X1 st for x1 holds P[x1] iff Q[x1] holds { y1 : P[y1] }
= { z1 : Q[z1] };
let X1;
assume
A1: P[x1] iff Q[x1];
for X1 st for x1 holds P[x1] implies Q[x1] holds { y1 : P[y1] }
c= { z1 : Q[z1] } from
Fraenkel5;
hence { y1 : P[y1] }
c= { z1 : Q[z1] } by
A1;
for X1 st for x1 holds Q[x1] implies P[x1] holds { y1 : Q[y1] }
c= { z1 : P[z1] } from
Fraenkel5;
hence thesis by
A1;
end;
scheme ::
DOMAIN_1:sch7
SubsetD { D() -> non
empty
set , P[
object] } :
{ d where d be
Element of D() : P[d] } is
Subset of D();
for D be non
empty
set holds { d where d be
Element of D : P[d] } is
Subset of D from
Fraenkel1;
hence thesis;
end;
theorem ::
DOMAIN_1:18
X1
= the set of all x1
proof
defpred
P[
set] means not contradiction;
A1: y1
in the set of all x1;
{ x1 :
P[x1] } is
Subset of X1 from
SubsetD;
hence thesis by
A1,
SUBSET_1: 28;
end;
theorem ::
DOMAIN_1:19
[:X1, X2:]
= the set of all
[x1, x2]
proof
defpred
P[
set,
set] means not contradiction;
A1: for x be
Element of
[:X1, X2:] holds x
in the set of all
[x1, x2]
proof
let x be
Element of
[:X1, X2:];
x
=
[(x
`1 ), (x
`2 )];
hence thesis;
end;
for X1, X2 holds {
[x1, x2] :
P[x1, x2] } is
Subset of
[:X1, X2:] from
Fraenkel2;
then the set of all
[x1, x2] is
Subset of
[:X1, X2:];
hence thesis by
A1,
SUBSET_1: 28;
end;
theorem ::
DOMAIN_1:20
[:X1, X2, X3:]
= the set of all
[x1, x2, x3]
proof
defpred
P[
set,
set,
set] means not contradiction;
A1: for x be
Element of
[:X1, X2, X3:] holds x
in the set of all
[x1, x2, x3]
proof
let x be
Element of
[:X1, X2, X3:];
x
=
[(x
`1_3 ), (x
`2_3 ), (x
`3_3 )];
hence thesis;
end;
for X1, X2, X3 holds {
[x1, x2, x3] :
P[x1, x2, x3] } is
Subset of
[:X1, X2, X3:] from
Fraenkel3;
then the set of all
[x1, x2, x3] is
Subset of
[:X1, X2, X3:];
hence thesis by
A1,
SUBSET_1: 28;
end;
theorem ::
DOMAIN_1:21
[:X1, X2, X3, X4:]
= the set of all
[x1, x2, x3, x4]
proof
defpred
P[
set,
set,
set,
set] means not contradiction;
A1: for x be
Element of
[:X1, X2, X3, X4:] holds x
in the set of all
[x1, x2, x3, x4]
proof
let x be
Element of
[:X1, X2, X3, X4:];
x
=
[(x
`1_4 ), (x
`2_4 ), (x
`3_4 ), (x
`4_4 )];
hence thesis;
end;
for X1, X2, X3, X4 holds {
[x1, x2, x3, x4] :
P[x1, x2, x3, x4] } is
Subset of
[:X1, X2, X3, X4:] from
Fraenkel4;
then the set of all
[x1, x2, x3, x4] is
Subset of
[:X1, X2, X3, X4:];
hence thesis by
A1,
SUBSET_1: 28;
end;
theorem ::
DOMAIN_1:22
A1
= { x1 : x1
in A1 }
proof
thus A1
c= { x1 : x1
in A1 };
let a be
object;
assume a
in { x1 : x1
in A1 };
then ex x1 st a
= x1 & x1
in A1;
hence thesis;
end;
theorem ::
DOMAIN_1:23
[:A1, A2:]
= {
[x1, x2] : x1
in A1 & x2
in A2 }
proof
thus
[:A1, A2:]
c= {
[x1, x2] : x1
in A1 & x2
in A2 }
proof
let a be
object;
assume
A1: a
in
[:A1, A2:];
then
reconsider x = a as
Element of
[:X1, X2:];
A2: x
=
[(x
`1 ), (x
`2 )];
(x
`1 )
in A1 & (x
`2 )
in A2 by
A1,
MCART_1: 10;
hence thesis by
A2;
end;
let a be
object;
assume a
in {
[x1, x2] : x1
in A1 & x2
in A2 };
then ex x1, x2 st a
=
[x1, x2] & x1
in A1 & x2
in A2;
hence thesis by
ZFMISC_1: 87;
end;
theorem ::
DOMAIN_1:24
[:A1, A2, A3:]
= {
[x1, x2, x3] : x1
in A1 & x2
in A2 & x3
in A3 }
proof
thus
[:A1, A2, A3:]
c= {
[x1, x2, x3] : x1
in A1 & x2
in A2 & x3
in A3 }
proof
let a be
object;
assume
A1: a
in
[:A1, A2, A3:];
reconsider A1 as non
empty
Subset of X1 by
A1,
MCART_1: 31;
reconsider A2 as non
empty
Subset of X2 by
A1,
MCART_1: 31;
reconsider A3 as non
empty
Subset of X3 by
A1,
MCART_1: 31;
A2: a
in
[:A1, A2, A3:] by
A1;
reconsider x = a as
Element of
[:X1, X2, X3:] by
A2;
A3: x
=
[(x
`1_3 ), (x
`2_3 ), (x
`3_3 )];
A4: (x
`3_3 )
in A3 by
A2,
MCART_1: 72;
(x
`1_3 )
in A1 & (x
`2_3 )
in A2 by
A2,
MCART_1: 72;
hence thesis by
A4,
A3;
end;
let a be
object;
assume a
in {
[x1, x2, x3] : x1
in A1 & x2
in A2 & x3
in A3 };
then ex x1, x2, x3 st a
=
[x1, x2, x3] & x1
in A1 & x2
in A2 & x3
in A3;
hence thesis by
MCART_1: 69;
end;
theorem ::
DOMAIN_1:25
[:A1, A2, A3, A4:]
= {
[x1, x2, x3, x4] : x1
in A1 & x2
in A2 & x3
in A3 & x4
in A4 }
proof
thus
[:A1, A2, A3, A4:]
c= {
[x1, x2, x3, x4] : x1
in A1 & x2
in A2 & x3
in A3 & x4
in A4 }
proof
let a be
object;
assume
A1: a
in
[:A1, A2, A3, A4:];
reconsider A1 as non
empty
Subset of X1 by
A1,
MCART_1: 51;
reconsider A2 as non
empty
Subset of X2 by
A1,
MCART_1: 51;
reconsider A3 as non
empty
Subset of X3 by
A1,
MCART_1: 51;
reconsider A4 as non
empty
Subset of X4 by
A1,
MCART_1: 51;
A2: a
in
[:A1, A2, A3, A4:] by
A1;
then
reconsider x = a as
Element of
[:X1, X2, X3, X4:];
A3: (x
`3_4 )
in A3 & (x
`4_4 )
in A4 by
A2,
MCART_1: 83;
A4: x
=
[(x
`1_4 ), (x
`2_4 ), (x
`3_4 ), (x
`4_4 )];
(x
`1_4 )
in A1 & (x
`2_4 )
in A2 by
A2,
MCART_1: 83;
hence thesis by
A4,
A3;
end;
let a be
object;
assume a
in {
[x1, x2, x3, x4] : x1
in A1 & x2
in A2 & x3
in A3 & x4
in A4 };
then ex x1, x2, x3, x4 st a
=
[x1, x2, x3, x4] & x1
in A1 & x2
in A2 & x3
in A3 & x4
in A4;
hence thesis by
MCART_1: 80;
end;
theorem ::
DOMAIN_1:26
(
{} X1)
= { x1 : contradiction }
proof
thus (
{} X1)
c= { x1 : contradiction };
let a be
object;
assume a
in { x1 : contradiction };
then ex x1 st a
= x1 & contradiction;
hence thesis;
end;
theorem ::
DOMAIN_1:27
(A1
` )
= { x1 : not x1
in A1 }
proof
thus (A1
` )
c= { x1 : not x1
in A1 }
proof
let a be
object;
assume
A1: a
in (A1
` );
then not a
in A1 by
XBOOLE_0:def 5;
hence thesis by
A1;
end;
let a be
object;
assume a
in { x1 : not x1
in A1 };
then ex x1 st a
= x1 & not x1
in A1;
hence thesis by
SUBSET_1: 29;
end;
theorem ::
DOMAIN_1:28
(A1
/\ B1)
= { x1 : x1
in A1 & x1
in B1 }
proof
thus (A1
/\ B1)
c= { x1 : x1
in A1 & x1
in B1 }
proof
let a be
object;
assume
A1: a
in (A1
/\ B1);
then
reconsider x = a as
Element of X1;
x
in A1 & x
in B1 by
A1,
XBOOLE_0:def 4;
hence thesis;
end;
let a be
object;
assume a
in { x1 : x1
in A1 & x1
in B1 };
then ex x1 st a
= x1 & x1
in A1 & x1
in B1;
hence thesis by
XBOOLE_0:def 4;
end;
theorem ::
DOMAIN_1:29
(A1
\/ B1)
= { x1 : x1
in A1 or x1
in B1 }
proof
thus (A1
\/ B1)
c= { x1 : x1
in A1 or x1
in B1 }
proof
let a be
object;
assume
A1: a
in (A1
\/ B1);
then
reconsider x = a as
Element of X1;
x
in A1 or x
in B1 by
A1,
XBOOLE_0:def 3;
hence thesis;
end;
let a be
object;
assume a
in { x1 : x1
in A1 or x1
in B1 };
then ex x1 st a
= x1 & (x1
in A1 or x1
in B1);
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
DOMAIN_1:30
(A1
\ B1)
= { x1 : x1
in A1 & not x1
in B1 }
proof
thus (A1
\ B1)
c= { x1 : x1
in A1 & not x1
in B1 }
proof
let a be
object;
assume
A1: a
in (A1
\ B1);
then
reconsider x = a as
Element of X1;
x
in A1 & not x
in B1 by
A1,
XBOOLE_0:def 5;
hence thesis;
end;
let a be
object;
assume a
in { x1 : x1
in A1 & not x1
in B1 };
then ex x1 st a
= x1 & x1
in A1 & not x1
in B1;
hence thesis by
XBOOLE_0:def 5;
end;
theorem ::
DOMAIN_1:31
Th31: (A1
\+\ B1)
= { x1 : x1
in A1 & not x1
in B1 or not x1
in A1 & x1
in B1 }
proof
thus (A1
\+\ B1)
c= { x1 : x1
in A1 & not x1
in B1 or not x1
in A1 & x1
in B1 }
proof
let a be
object;
assume
A1: a
in (A1
\+\ B1);
then
reconsider x = a as
Element of X1;
x
in A1 & not x
in B1 or not x
in A1 & x
in B1 by
A1,
XBOOLE_0: 1;
hence thesis;
end;
let a be
object;
assume a
in { x1 : x1
in A1 & not x1
in B1 or not x1
in A1 & x1
in B1 };
then ex x1 st a
= x1 & (x1
in A1 & not x1
in B1 or not x1
in A1 & x1
in B1);
hence thesis by
XBOOLE_0: 1;
end;
theorem ::
DOMAIN_1:32
Th32: (A1
\+\ B1)
= { x1 : not x1
in A1 iff x1
in B1 }
proof
A1: for x1 holds (x1
in A1 & not x1
in B1 or not x1
in A1 & x1
in B1) iff ( not x1
in A1 iff x1
in B1);
defpred
Q[
set] means not $1
in A1 iff $1
in B1;
defpred
P[
set] means $1
in A1 & not $1
in B1 or not $1
in A1 & $1
in B1;
A2: (A1
\+\ B1)
= { x1 : x1
in A1 & not x1
in B1 or not x1
in A1 & x1
in B1 } by
Th31;
for X1 st for x1 holds
P[x1] iff
Q[x1] holds { y1 :
P[y1] }
= { z1 :
Q[z1] } from
Fraenkel6;
hence thesis by
A1,
A2;
end;
theorem ::
DOMAIN_1:33
(A1
\+\ B1)
= { x1 : x1
in A1 iff not x1
in B1 }
proof
A1: for x1 holds ( not x1
in A1 iff x1
in B1) iff (x1
in A1 iff not x1
in B1);
defpred
Q[
set] means $1
in A1 iff not $1
in B1;
defpred
P[
set] means not $1
in A1 iff $1
in B1;
A2: (A1
\+\ B1)
= { x1 : not x1
in A1 iff x1
in B1 } by
Th32;
for X1 st for x1 holds
P[x1] iff
Q[x1] holds { y1 :
P[y1] }
= { z1 :
Q[z1] } from
Fraenkel6;
hence thesis by
A1,
A2;
end;
theorem ::
DOMAIN_1:34
(A1
\+\ B1)
= { x1 : not (x1
in A1 iff x1
in B1) }
proof
A1: for x1 holds ( not x1
in A1 iff x1
in B1) iff not (x1
in A1 iff x1
in B1);
defpred
Q[
set] means not ($1
in A1 iff $1
in B1);
defpred
P[
set] means not $1
in A1 iff $1
in B1;
A2: (A1
\+\ B1)
= { x1 : not x1
in A1 iff x1
in B1 } by
Th32;
for X1 st for x1 holds
P[x1] iff
Q[x1] holds { y1 :
P[y1] }
= { z1 :
Q[z1] } from
Fraenkel6;
hence thesis by
A1,
A2;
end;
definition
let D be non
empty
set;
let x1 be
Element of D;
:: original:
{
redefine
func
{x1} ->
Subset of D ;
coherence by
SUBSET_1: 33;
let x2 be
Element of D;
:: original:
{
redefine
func
{x1,x2} ->
Subset of D ;
coherence by
SUBSET_1: 34;
let x3 be
Element of D;
:: original:
{
redefine
func
{x1,x2,x3} ->
Subset of D ;
coherence by
SUBSET_1: 35;
let x4 be
Element of D;
:: original:
{
redefine
func
{x1,x2,x3,x4} ->
Subset of D ;
coherence by
SUBSET_1: 36;
let x5 be
Element of D;
:: original:
{
redefine
func
{x1,x2,x3,x4,x5} ->
Subset of D ;
coherence by
SUBSET_1: 37;
let x6 be
Element of D;
:: original:
{
redefine
func
{x1,x2,x3,x4,x5,x6} ->
Subset of D ;
coherence by
SUBSET_1: 38;
let x7 be
Element of D;
:: original:
{
redefine
func
{x1,x2,x3,x4,x5,x6,x7} ->
Subset of D ;
coherence by
SUBSET_1: 39;
let x8 be
Element of D;
:: original:
{
redefine
func
{x1,x2,x3,x4,x5,x6,x7,x8} ->
Subset of D ;
coherence by
SUBSET_1: 40;
let x9 be
Element of D;
:: original:
{
redefine
func
{x1,x2,x3,x4,x5,x6,x7,x8,x9} ->
Subset of D ;
coherence by
SUBSET_1: 52;
let x10 be
Element of D;
:: original:
{
redefine
func
{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} ->
Subset of D ;
coherence by
SUBSET_1: 53;
end
begin
scheme ::
DOMAIN_1:sch8
SubsetFD { A,D() -> non
empty
set , F(
object) ->
Element of D() , P[
object] } :
{ F(x) where x be
Element of A() : P[x] } is
Subset of D();
set X = { F(x) where x be
Element of A() : P[x] };
X
c= D()
proof
let y be
object;
assume y
in X;
then ex z be
Element of A() st y
= F(z) & P[z];
hence thesis;
end;
hence thesis;
end;
scheme ::
DOMAIN_1:sch9
SubsetFD2 { A,B,D() -> non
empty
set , F(
object,
object) ->
Element of D() , P[
object,
object] } :
{ F(x,y) where x be
Element of A(), y be
Element of B() : P[x, y] } is
Subset of D();
set X = { F(x,y) where x be
Element of A(), y be
Element of B() : P[x, y] };
X
c= D()
proof
let w be
object;
assume w
in X;
then ex x be
Element of A(), y be
Element of B() st w
= F(x,y) & P[x, y];
hence thesis;
end;
hence thesis;
end;
definition
let D1,D2,D3 be non
empty
set, x be
Element of
[:
[:D1, D2:], D3:];
:: original:
`11
redefine
func x
`11 ->
Element of D1 ;
coherence
proof
(x
`11 )
= ((x
`1 )
`1 ) by
MCART_1:def 14;
hence thesis;
end;
:: original:
`12
redefine
func x
`12 ->
Element of D2 ;
coherence
proof
(x
`12 )
= ((x
`1 )
`2 ) by
MCART_1:def 15;
hence thesis;
end;
end
definition
let D1,D2,D3 be non
empty
set, x be
Element of
[:D1,
[:D2, D3:]:];
:: original:
`21
redefine
func x
`21 ->
Element of D2 ;
coherence
proof
(x
`21 )
= ((x
`2 )
`1 ) by
MCART_1:def 16;
hence thesis;
end;
:: original:
`22
redefine
func x
`22 ->
Element of D3 ;
coherence
proof
(x
`22 )
= ((x
`2 )
`2 ) by
MCART_1:def 17;
hence thesis;
end;
end
scheme ::
DOMAIN_1:sch10
AndScheme { A() -> non
empty
set , P,Q[
object] } :
{ a where a be
Element of A() : P[a] & Q[a] }
= ({ a1 where a1 be
Element of A() : P[a1] }
/\ { a2 where a2 be
Element of A() : Q[a2] });
set A = { a where a be
Element of A() : P[a] & Q[a] }, A1 = { a1 where a1 be
Element of A() : P[a1] }, A2 = { a2 where a2 be
Element of A() : Q[a2] };
thus A
c= (A1
/\ A2)
proof
let x be
object;
assume x
in A;
then
consider a be
Element of A() such that
A1: x
= a and
A2: P[a] & Q[a];
a
in A1 & a
in A2 by
A2;
hence thesis by
A1,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A3: x
in (A1
/\ A2);
then x
in A2 by
XBOOLE_0:def 4;
then
A4: ex a be
Element of A() st x
= a & Q[a];
x
in A1 by
A3,
XBOOLE_0:def 4;
then ex a be
Element of A() st x
= a & P[a];
hence thesis by
A4;
end;
registration
let A be non
empty
set;
cluster
c=-linear non
empty for
Subset of A;
existence
proof
set a = the
Element of A;
reconsider B =
{a} as non
empty
Subset of A;
take B;
B is
c=-linear
proof
let x,y be
set;
assume that
A1: x
in B and
A2: y
in B;
x
= a by
A1,
TARSKI:def 1;
hence thesis by
A2,
TARSKI:def 1;
end;
hence thesis;
end;
end