:: SUBSET_1 semantic presentation
begin
registration
let X be set ;
cluster bool X -> non empty ;
coherence
not bool X is empty by ZFMISC_1:def_1;
end;
registration
let x1, x2, x3 be set ;
cluster{x1,x2,x3} -> non empty ;
coherence
not {x1,x2,x3} is empty by ENUMSET1:def_1;
let x4 be set ;
cluster{x1,x2,x3,x4} -> non empty ;
coherence
not {x1,x2,x3,x4} is empty by ENUMSET1:def_2;
let x5 be set ;
cluster{x1,x2,x3,x4,x5} -> non empty ;
coherence
not {x1,x2,x3,x4,x5} is empty by ENUMSET1:def_3;
let x6 be set ;
cluster{x1,x2,x3,x4,x5,x6} -> non empty ;
coherence
not {x1,x2,x3,x4,x5,x6} is empty by ENUMSET1:def_4;
let x7 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7} -> non empty ;
coherence
not {x1,x2,x3,x4,x5,x6,x7} is empty by ENUMSET1:def_5;
let x8 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8} -> non empty ;
coherence
not {x1,x2,x3,x4,x5,x6,x7,x8} is empty by ENUMSET1:def_6;
let x9 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8,x9} -> non empty ;
coherence
not {x1,x2,x3,x4,x5,x6,x7,x8,x9} is empty by ENUMSET1:def_7;
let x10 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> non empty ;
coherence
not {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is empty by ENUMSET1:def_8;
end;
definition
let X be set ;
mode Element of X -> set means :Def1: :: SUBSET_1:def 1
it in X if not X is empty
otherwise it is empty ;
existence
( ( not X is empty implies ex b1 being set st b1 in X ) & ( X is empty implies ex b1 being set st b1 is empty ) ) by XBOOLE_0:def_1;
consistency
for b1 being set holds verum ;
sethood
( ( not X is empty & ex b1 being set st
for b2 being set st b2 in X holds
b2 in b1 ) or ( X is empty & ex b1 being set st
for b2 being set st b2 is empty holds
b2 in b1 ) )
proof
percases ( not X is empty or X is empty ) ;
case not X is empty ; ::_thesis: ex b1 being set st
for b2 being set st b2 in X holds
b2 in b1
take X ; ::_thesis: for b1 being set st b1 in X holds
b1 in X
thus for b1 being set st b1 in X holds
b1 in X ; ::_thesis: verum
end;
case X is empty ; ::_thesis: ex b1 being set st
for b2 being set st b2 is empty holds
b2 in b1
take {{}} ; ::_thesis: for b1 being set st b1 is empty holds
b1 in {{}}
let y be set ; ::_thesis: ( y is empty implies y in {{}} )
thus ( y is empty implies y in {{}} ) by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def1 defines Element SUBSET_1:def_1_:_
for X being set
for b2 being set holds
( ( not X is empty implies ( b2 is Element of X iff b2 in X ) ) & ( X is empty implies ( b2 is Element of X iff b2 is empty ) ) );
definition
let X be set ;
mode Subset of X is Element of bool X;
end;
registration
let X be non empty set ;
cluster non empty for Element of bool X;
existence
not for b1 being Subset of X holds b1 is empty
proof
X in bool X by ZFMISC_1:def_1;
then X is Subset of X by Def1;
hence not for b1 being Subset of X holds b1 is empty ; ::_thesis: verum
end;
end;
registration
let X1, X2 be non empty set ;
cluster[:X1,X2:] -> non empty ;
coherence
not [:X1,X2:] is empty
proof
consider x2 being set such that
A1: x2 in X2 by XBOOLE_0:def_1;
consider x1 being set such that
A2: x1 in X1 by XBOOLE_0:def_1;
[x1,x2] in [:X1,X2:] by A2, A1, ZFMISC_1:def_2;
hence not [:X1,X2:] is empty ; ::_thesis: verum
end;
end;
registration
let X1, X2, X3 be non empty set ;
cluster[:X1,X2,X3:] -> non empty ;
coherence
not [:X1,X2,X3:] is empty ;
end;
registration
let X1, X2, X3, X4 be non empty set ;
cluster[:X1,X2,X3,X4:] -> non empty ;
coherence
not [:X1,X2,X3,X4:] is empty ;
end;
definition
let D be non empty set ;
let X be non empty Subset of D;
:: original: Element
redefine mode Element of X -> Element of D;
coherence
for b1 being Element of X holds b1 is Element of D
proof
let x be Element of X; ::_thesis: x is Element of D
X in bool D by Def1;
then A1: X c= D by ZFMISC_1:def_1;
x in X by Def1;
then x in D by A1, TARSKI:def_3;
hence x is Element of D by Def1; ::_thesis: verum
end;
end;
Lm1: for E being set
for X being Subset of E
for x being set st x in X holds
x in E
proof
let E be set ; ::_thesis: for X being Subset of E
for x being set st x in X holds
x in E
let X be Subset of E; ::_thesis: for x being set st x in X holds
x in E
let x be set ; ::_thesis: ( x in X implies x in E )
assume A1: x in X ; ::_thesis: x in E
X in bool E by Def1;
then X c= E by ZFMISC_1:def_1;
hence x in E by A1, TARSKI:def_3; ::_thesis: verum
end;
registration
let E be set ;
cluster empty for Element of bool E;
existence
ex b1 being Subset of E st b1 is empty
proof
{} c= E by XBOOLE_1:2;
then {} in bool E by ZFMISC_1:def_1;
then {} is Subset of E by Def1;
hence ex b1 being Subset of E st b1 is empty ; ::_thesis: verum
end;
end;
definition
let E be set ;
func {} E -> Subset of E equals :: SUBSET_1:def 2
{} ;
coherence
{} is Subset of E
proof
{} c= E by XBOOLE_1:2;
then {} in bool E by ZFMISC_1:def_1;
hence {} is Subset of E by Def1; ::_thesis: verum
end;
correctness
;
func [#] E -> Subset of E equals :: SUBSET_1:def 3
E;
coherence
E is Subset of E
proof
E in bool E by ZFMISC_1:def_1;
hence E is Subset of E by Def1; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem defines {} SUBSET_1:def_2_:_
for E being set holds {} E = {} ;
:: deftheorem defines [#] SUBSET_1:def_3_:_
for E being set holds [#] E = E;
registration
let E be set ;
cluster {} E -> empty ;
coherence
{} E is empty ;
end;
theorem :: SUBSET_1:1
for X being set holds {} is Subset of X
proof
let X be set ; ::_thesis: {} is Subset of X
{} X = {} ;
hence {} is Subset of X ; ::_thesis: verum
end;
theorem Th2: :: SUBSET_1:2
for E being set
for A, B being Subset of E st ( for x being Element of E st x in A holds
x in B ) holds
A c= B
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E st x in A holds
x in B ) holds
A c= B
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E st x in A holds
x in B ) implies A c= B )
assume A1: for x being Element of E st x in A holds
x in B ; ::_thesis: A c= B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume A2: x in A ; ::_thesis: x in B
then x in E by Lm1;
then x is Element of E by Def1;
hence x in B by A1, A2; ::_thesis: verum
end;
theorem Th3: :: SUBSET_1:3
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( x in A iff x in B ) ) holds
A = B
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E holds
( x in A iff x in B ) ) holds
A = B
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff x in B ) ) implies A = B )
assume for x being Element of E holds
( x in A iff x in B ) ; ::_thesis: A = B
hence ( A c= B & B c= A ) by Th2; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
theorem Th4: :: SUBSET_1:4
for E being set
for A being Subset of E st A <> {} holds
ex x being Element of E st x in A
proof
let E be set ; ::_thesis: for A being Subset of E st A <> {} holds
ex x being Element of E st x in A
let A be Subset of E; ::_thesis: ( A <> {} implies ex x being Element of E st x in A )
assume A <> {} ; ::_thesis: ex x being Element of E st x in A
then consider x being set such that
A1: x in A by XBOOLE_0:def_1;
x in E by A1, Lm1;
then x is Element of E by Def1;
hence ex x being Element of E st x in A by A1; ::_thesis: verum
end;
definition
let E be set ;
let A be Subset of E;
funcA ` -> Subset of E equals :: SUBSET_1:def 4
E \ A;
coherence
E \ A is Subset of E
proof
E \ A c= E by XBOOLE_1:36;
then E \ A in bool E by ZFMISC_1:def_1;
hence E \ A is Subset of E by Def1; ::_thesis: verum
end;
correctness
;
involutiveness
for b1, b2 being Subset of E st b1 = E \ b2 holds
b2 = E \ b1
proof
let S, T be Subset of E; ::_thesis: ( S = E \ T implies T = E \ S )
assume A1: S = E \ T ; ::_thesis: T = E \ S
T in bool E by Def1;
then T c= E by ZFMISC_1:def_1;
hence T = {} \/ (E /\ T) by XBOOLE_1:28
.= (E \ E) \/ (E /\ T) by XBOOLE_1:37
.= E \ S by A1, XBOOLE_1:52 ;
::_thesis: verum
end;
let B be Subset of E;
:: original: \/
redefine funcA \/ B -> Subset of E;
coherence
A \/ B is Subset of E
proof
B in bool E by Def1;
then A2: B c= E by ZFMISC_1:def_1;
A in bool E by Def1;
then A c= E by ZFMISC_1:def_1;
then A \/ B c= E by A2, XBOOLE_1:8;
then A \/ B in bool E by ZFMISC_1:def_1;
hence A \/ B is Subset of E by Def1; ::_thesis: verum
end;
:: original: \+\
redefine funcA \+\ B -> Subset of E;
coherence
A \+\ B is Subset of E
proof
B in bool E by Def1;
then ( B \ A c= B & B c= E ) by XBOOLE_1:36, ZFMISC_1:def_1;
then A3: B \ A c= E by XBOOLE_1:1;
A in bool E by Def1;
then ( A \ B c= A & A c= E ) by XBOOLE_1:36, ZFMISC_1:def_1;
then A \ B c= E by XBOOLE_1:1;
then (A \ B) \/ (B \ A) c= E by A3, XBOOLE_1:8;
then A \+\ B in bool E by ZFMISC_1:def_1;
hence A \+\ B is Subset of E by Def1; ::_thesis: verum
end;
end;
:: deftheorem defines ` SUBSET_1:def_4_:_
for E being set
for A being Subset of E holds A ` = E \ A;
definition
let X, Y be set ;
:: original: \
redefine funcX \ Y -> Subset of X;
coherence
X \ Y is Subset of X
proof
X \ Y c= X by XBOOLE_1:36;
then X \ Y in bool X by ZFMISC_1:def_1;
hence X \ Y is Subset of X by Def1; ::_thesis: verum
end;
end;
definition
let E be set ;
let A be Subset of E;
let X be set ;
:: original: \
redefine funcA \ X -> Subset of E;
coherence
A \ X is Subset of E
proof
A in bool E by Def1;
then ( A \ X c= A & A c= E ) by XBOOLE_1:36, ZFMISC_1:def_1;
then A \ X c= E by XBOOLE_1:1;
then A \ X in bool E by ZFMISC_1:def_1;
hence A \ X is Subset of E by Def1; ::_thesis: verum
end;
end;
definition
let E be set ;
let A be Subset of E;
let X be set ;
:: original: /\
redefine funcA /\ X -> Subset of E;
coherence
A /\ X is Subset of E
proof
A in bool E by Def1;
then ( A /\ X c= A & A c= E ) by XBOOLE_1:17, ZFMISC_1:def_1;
then A /\ X c= E by XBOOLE_1:1;
then A /\ X in bool E by ZFMISC_1:def_1;
hence A /\ X is Subset of E by Def1; ::_thesis: verum
end;
end;
definition
let E, X be set ;
let A be Subset of E;
:: original: /\
redefine funcX /\ A -> Subset of E;
coherence
X /\ A is Subset of E
proof
A /\ X is Subset of E ;
hence X /\ A is Subset of E ; ::_thesis: verum
end;
end;
theorem :: SUBSET_1:5
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B or x in C ) ) ) holds
A = B \/ C
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B or x in C ) ) ) holds
A = B \/ C
let A, B, C be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff ( x in B or x in C ) ) ) implies A = B \/ C )
assume A1: for x being Element of E holds
( x in A iff ( x in B or x in C ) ) ; ::_thesis: A = B \/ C
now__::_thesis:_for_x_being_Element_of_E_st_x_in_A_holds_
x_in_B_\/_C
let x be Element of E; ::_thesis: ( x in A implies x in B \/ C )
assume x in A ; ::_thesis: x in B \/ C
then ( x in B or x in C ) by A1;
hence x in B \/ C by XBOOLE_0:def_3; ::_thesis: verum
end;
hence A c= B \/ C by Th2; :: according to XBOOLE_0:def_10 ::_thesis: B \/ C c= A
now__::_thesis:_for_x_being_Element_of_E_st_x_in_B_\/_C_holds_
x_in_A
let x be Element of E; ::_thesis: ( x in B \/ C implies x in A )
assume x in B \/ C ; ::_thesis: x in A
then ( x in B or x in C ) by XBOOLE_0:def_3;
hence x in A by A1; ::_thesis: verum
end;
hence B \/ C c= A by Th2; ::_thesis: verum
end;
theorem :: SUBSET_1:6
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B & x in C ) ) ) holds
A = B /\ C
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B & x in C ) ) ) holds
A = B /\ C
let A, B, C be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff ( x in B & x in C ) ) ) implies A = B /\ C )
assume A1: for x being Element of E holds
( x in A iff ( x in B & x in C ) ) ; ::_thesis: A = B /\ C
now__::_thesis:_for_x_being_Element_of_E_st_x_in_A_holds_
x_in_B_/\_C
let x be Element of E; ::_thesis: ( x in A implies x in B /\ C )
assume x in A ; ::_thesis: x in B /\ C
then ( x in B & x in C ) by A1;
hence x in B /\ C by XBOOLE_0:def_4; ::_thesis: verum
end;
hence A c= B /\ C by Th2; :: according to XBOOLE_0:def_10 ::_thesis: B /\ C c= A
now__::_thesis:_for_x_being_Element_of_E_st_x_in_B_/\_C_holds_
x_in_A
let x be Element of E; ::_thesis: ( x in B /\ C implies x in A )
assume x in B /\ C ; ::_thesis: x in A
then ( x in B & x in C ) by XBOOLE_0:def_4;
hence x in A by A1; ::_thesis: verum
end;
hence B /\ C c= A by Th2; ::_thesis: verum
end;
theorem :: SUBSET_1:7
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B & not x in C ) ) ) holds
A = B \ C
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B & not x in C ) ) ) holds
A = B \ C
let A, B, C be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff ( x in B & not x in C ) ) ) implies A = B \ C )
assume A1: for x being Element of E holds
( x in A iff ( x in B & not x in C ) ) ; ::_thesis: A = B \ C
now__::_thesis:_for_x_being_Element_of_E_st_x_in_A_holds_
x_in_B_\_C
let x be Element of E; ::_thesis: ( x in A implies x in B \ C )
assume x in A ; ::_thesis: x in B \ C
then ( x in B & not x in C ) by A1;
hence x in B \ C by XBOOLE_0:def_5; ::_thesis: verum
end;
hence A c= B \ C by Th2; :: according to XBOOLE_0:def_10 ::_thesis: B \ C c= A
now__::_thesis:_for_x_being_Element_of_E_st_x_in_B_\_C_holds_
x_in_A
let x be Element of E; ::_thesis: ( x in B \ C implies x in A )
assume x in B \ C ; ::_thesis: x in A
then ( x in B & not x in C ) by XBOOLE_0:def_5;
hence x in A by A1; ::_thesis: verum
end;
hence B \ C c= A by Th2; ::_thesis: verum
end;
theorem :: SUBSET_1:8
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) holds
A = B \+\ C
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) holds
A = B \+\ C
let A, B, C be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) implies A = B \+\ C )
assume A1: for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ; ::_thesis: A = B \+\ C
now__::_thesis:_for_x_being_Element_of_E_st_x_in_A_holds_
x_in_B_\+\_C
let x be Element of E; ::_thesis: ( x in A implies x in B \+\ C )
assume x in A ; ::_thesis: x in B \+\ C
then ( ( x in B & not x in C ) or ( x in C & not x in B ) ) by A1;
then ( x in B \ C or x in C \ B ) by XBOOLE_0:def_5;
hence x in B \+\ C by XBOOLE_0:def_3; ::_thesis: verum
end;
hence A c= B \+\ C by Th2; :: according to XBOOLE_0:def_10 ::_thesis: B \+\ C c= A
now__::_thesis:_for_x_being_Element_of_E_st_x_in_B_\+\_C_holds_
x_in_A
let x be Element of E; ::_thesis: ( x in B \+\ C implies x in A )
assume x in B \+\ C ; ::_thesis: x in A
then ( x in B \ C or x in C \ B ) by XBOOLE_0:def_3;
then ( ( x in B & not x in C ) or ( x in C & not x in B ) ) by XBOOLE_0:def_5;
hence x in A by A1; ::_thesis: verum
end;
hence B \+\ C c= A by Th2; ::_thesis: verum
end;
theorem :: SUBSET_1:9
for E being set holds [#] E = ({} E) ` ;
theorem Th10: :: SUBSET_1:10
for E being set
for A being Subset of E holds A \/ (A `) = [#] E
proof
let E be set ; ::_thesis: for A being Subset of E holds A \/ (A `) = [#] E
let A be Subset of E; ::_thesis: A \/ (A `) = [#] E
A in bool E by Def1;
then A c= E by ZFMISC_1:def_1;
hence A \/ (A `) = [#] E by XBOOLE_1:45; ::_thesis: verum
end;
theorem :: SUBSET_1:11
for E being set
for A being Subset of E holds A \/ ([#] E) = [#] E
proof
let E be set ; ::_thesis: for A being Subset of E holds A \/ ([#] E) = [#] E
let A be Subset of E; ::_thesis: A \/ ([#] E) = [#] E
A in bool E by Def1;
then A c= E by ZFMISC_1:def_1;
hence A \/ ([#] E) = [#] E by XBOOLE_1:12; ::_thesis: verum
end;
theorem Th12: :: SUBSET_1:12
for E being set
for A, B being Subset of E holds
( A c= B iff B ` c= A ` )
proof
let E be set ; ::_thesis: for A, B being Subset of E holds
( A c= B iff B ` c= A ` )
let A, B be Subset of E; ::_thesis: ( A c= B iff B ` c= A ` )
thus ( A c= B implies B ` c= A ` ) by XBOOLE_1:34; ::_thesis: ( B ` c= A ` implies A c= B )
A1: E \ (B `) = (B `) `
.= B ;
E \ (A `) = (A `) `
.= A ;
hence ( B ` c= A ` implies A c= B ) by A1, XBOOLE_1:34; ::_thesis: verum
end;
theorem :: SUBSET_1:13
for E being set
for A, B being Subset of E holds A \ B = A /\ (B `)
proof
let E be set ; ::_thesis: for A, B being Subset of E holds A \ B = A /\ (B `)
let A, B be Subset of E; ::_thesis: A \ B = A /\ (B `)
A in bool E by Def1;
then A1: A c= E by ZFMISC_1:def_1;
thus A /\ (B `) = (A /\ E) \ B by XBOOLE_1:49
.= A \ B by A1, XBOOLE_1:28 ; ::_thesis: verum
end;
theorem :: SUBSET_1:14
for E being set
for A, B being Subset of E holds (A \ B) ` = (A `) \/ B
proof
let E be set ; ::_thesis: for A, B being Subset of E holds (A \ B) ` = (A `) \/ B
let A, B be Subset of E; ::_thesis: (A \ B) ` = (A `) \/ B
B in bool E by Def1;
then A1: B c= E by ZFMISC_1:def_1;
thus (A \ B) ` = (E \ A) \/ (E /\ B) by XBOOLE_1:52
.= (A `) \/ B by A1, XBOOLE_1:28 ; ::_thesis: verum
end;
theorem :: SUBSET_1:15
for E being set
for A, B being Subset of E holds (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))
proof
let E be set ; ::_thesis: for A, B being Subset of E holds (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))
let A, B be Subset of E; ::_thesis: (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))
A in bool E by Def1;
then A1: A c= E by ZFMISC_1:def_1;
thus (A \+\ B) ` = (E \ (A \/ B)) \/ ((E /\ A) /\ B) by XBOOLE_1:102
.= (A /\ B) \/ (E \ (A \/ B)) by A1, XBOOLE_1:28
.= (A /\ B) \/ ((A `) /\ (B `)) by XBOOLE_1:53 ; ::_thesis: verum
end;
theorem :: SUBSET_1:16
for E being set
for A, B being Subset of E st A c= B ` holds
B c= A `
proof
let E be set ; ::_thesis: for A, B being Subset of E st A c= B ` holds
B c= A `
let A, B be Subset of E; ::_thesis: ( A c= B ` implies B c= A ` )
assume A c= B ` ; ::_thesis: B c= A `
then (B `) ` c= A ` by Th12;
hence B c= A ` ; ::_thesis: verum
end;
theorem :: SUBSET_1:17
for E being set
for A, B being Subset of E st A ` c= B holds
B ` c= A
proof
let E be set ; ::_thesis: for A, B being Subset of E st A ` c= B holds
B ` c= A
let A, B be Subset of E; ::_thesis: ( A ` c= B implies B ` c= A )
assume A ` c= B ; ::_thesis: B ` c= A
then B ` c= (A `) ` by Th12;
hence B ` c= A ; ::_thesis: verum
end;
theorem :: SUBSET_1:18
for E being set
for A being Subset of E holds
( A c= A ` iff A = {} E )
proof
let E be set ; ::_thesis: for A being Subset of E holds
( A c= A ` iff A = {} E )
let A be Subset of E; ::_thesis: ( A c= A ` iff A = {} E )
thus ( A c= A ` implies A = {} E ) by XBOOLE_1:38; ::_thesis: ( A = {} E implies A c= A ` )
A in bool E by Def1;
hence ( A = {} E implies A c= A ` ) by ZFMISC_1:def_1; ::_thesis: verum
end;
theorem :: SUBSET_1:19
for E being set
for A being Subset of E holds
( A ` c= A iff A = [#] E )
proof
let E be set ; ::_thesis: for A being Subset of E holds
( A ` c= A iff A = [#] E )
let A be Subset of E; ::_thesis: ( A ` c= A iff A = [#] E )
thus ( A ` c= A implies A = [#] E ) ::_thesis: ( A = [#] E implies A ` c= A )
proof
assume A ` c= A ; ::_thesis: A = [#] E
hence A = A \/ (A `) by XBOOLE_1:12
.= [#] E by Th10 ;
::_thesis: verum
end;
assume A = [#] E ; ::_thesis: A ` c= A
then A ` = {} by XBOOLE_1:37;
hence A ` c= A by XBOOLE_1:2; ::_thesis: verum
end;
theorem :: SUBSET_1:20
for E, X being set
for A being Subset of E st X c= A & X c= A ` holds
X = {} by XBOOLE_1:67, XBOOLE_1:79;
theorem :: SUBSET_1:21
for E being set
for A, B being Subset of E holds (A \/ B) ` c= A `
proof
let E be set ; ::_thesis: for A, B being Subset of E holds (A \/ B) ` c= A `
let A, B be Subset of E; ::_thesis: (A \/ B) ` c= A `
A c= A \/ B by XBOOLE_1:7;
hence (A \/ B) ` c= A ` by Th12; ::_thesis: verum
end;
theorem :: SUBSET_1:22
for E being set
for A, B being Subset of E holds A ` c= (A /\ B) `
proof
let E be set ; ::_thesis: for A, B being Subset of E holds A ` c= (A /\ B) `
let A, B be Subset of E; ::_thesis: A ` c= (A /\ B) `
A /\ B c= A by XBOOLE_1:17;
hence A ` c= (A /\ B) ` by Th12; ::_thesis: verum
end;
theorem Th23: :: SUBSET_1:23
for E being set
for A, B being Subset of E holds
( A misses B iff A c= B ` )
proof
let E be set ; ::_thesis: for A, B being Subset of E holds
( A misses B iff A c= B ` )
let A, B be Subset of E; ::_thesis: ( A misses B iff A c= B ` )
thus ( A misses B implies A c= B ` ) ::_thesis: ( A c= B ` implies A misses B )
proof
assume A1: A misses B ; ::_thesis: A c= B `
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ` )
assume A2: x in A ; ::_thesis: x in B `
then A3: not x in B by A1, XBOOLE_0:3;
x in E by A2, Lm1;
hence x in B ` by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A4: A c= B ` ; ::_thesis: A misses B
assume A meets B ; ::_thesis: contradiction
then consider x being set such that
A5: x in A and
A6: x in B by XBOOLE_0:3;
x in E \ B by A4, A5, TARSKI:def_3;
hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: SUBSET_1:24
for E being set
for A, B being Subset of E holds
( A misses B ` iff A c= B )
proof
let E be set ; ::_thesis: for A, B being Subset of E holds
( A misses B ` iff A c= B )
let A, B be Subset of E; ::_thesis: ( A misses B ` iff A c= B )
(B `) ` = B ;
hence ( A misses B ` iff A c= B ) by Th23; ::_thesis: verum
end;
theorem :: SUBSET_1:25
for E being set
for A, B being Subset of E st A misses B & A ` misses B ` holds
A = B `
proof
let E be set ; ::_thesis: for A, B being Subset of E st A misses B & A ` misses B ` holds
A = B `
let A, B be Subset of E; ::_thesis: ( A misses B & A ` misses B ` implies A = B ` )
assume that
A1: A misses B and
A2: A ` misses B ` ; ::_thesis: A = B `
A3: A in bool E by Def1;
thus A c= B ` :: according to XBOOLE_0:def_10 ::_thesis: B ` c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ` )
assume A4: x in A ; ::_thesis: x in B `
then A5: not x in B by A1, XBOOLE_0:3;
A c= E by A3, ZFMISC_1:def_1;
then x in E by A4, TARSKI:def_3;
hence x in B ` by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B ` or x in A )
A6: ( x in A ` implies not x in B ` ) by A2, XBOOLE_0:3;
assume A7: x in B ` ; ::_thesis: x in A
then x in E by XBOOLE_0:def_5;
hence x in A by A7, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: SUBSET_1:26
for E being set
for A, B, C being Subset of E st A c= B & C misses B holds
A c= C `
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st A c= B & C misses B holds
A c= C `
let A, B, C be Subset of E; ::_thesis: ( A c= B & C misses B implies A c= C ` )
assume ( A c= B & C misses B ) ; ::_thesis: A c= C `
then A misses C by XBOOLE_1:63;
hence A c= C ` by Th23; ::_thesis: verum
end;
theorem :: SUBSET_1:27
for E being set
for A, B being Subset of E st ( for a being Element of A holds a in B ) holds
A c= B
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for a being Element of A holds a in B ) holds
A c= B
let A, B be Subset of E; ::_thesis: ( ( for a being Element of A holds a in B ) implies A c= B )
assume A1: for a being Element of A holds a in B ; ::_thesis: A c= B
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in B )
assume a in A ; ::_thesis: a in B
then a is Element of A by Def1;
hence a in B by A1; ::_thesis: verum
end;
theorem :: SUBSET_1:28
for E being set
for A being Subset of E st ( for x being Element of E holds x in A ) holds
E = A
proof
let E be set ; ::_thesis: for A being Subset of E st ( for x being Element of E holds x in A ) holds
E = A
let A be Subset of E; ::_thesis: ( ( for x being Element of E holds x in A ) implies E = A )
assume A1: for x being Element of E holds x in A ; ::_thesis: E = A
thus E c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= E
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in E or a in A )
assume a in E ; ::_thesis: a in A
then a is Element of E by Def1;
hence a in A by A1; ::_thesis: verum
end;
A in bool E by Def1;
hence A c= E by ZFMISC_1:def_1; ::_thesis: verum
end;
theorem :: SUBSET_1:29
for E being set st E <> {} holds
for B being Subset of E
for x being Element of E st not x in B holds
x in B `
proof
let E be set ; ::_thesis: ( E <> {} implies for B being Subset of E
for x being Element of E st not x in B holds
x in B ` )
assume A1: E <> {} ; ::_thesis: for B being Subset of E
for x being Element of E st not x in B holds
x in B `
let B be Subset of E; ::_thesis: for x being Element of E st not x in B holds
x in B `
let x be Element of E; ::_thesis: ( not x in B implies x in B ` )
assume A2: not x in B ; ::_thesis: x in B `
x in E by A1, Def1;
hence x in B ` by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th30: :: SUBSET_1:30
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( x in A iff not x in B ) ) holds
A = B `
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E holds
( x in A iff not x in B ) ) holds
A = B `
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff not x in B ) ) implies A = B ` )
assume A1: for x being Element of E holds
( x in A iff not x in B ) ; ::_thesis: A = B `
thus A c= B ` :: according to XBOOLE_0:def_10 ::_thesis: B ` c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ` )
assume A2: x in A ; ::_thesis: x in B `
A in bool E by Def1;
then A c= E by ZFMISC_1:def_1;
then x in E by A2, TARSKI:def_3;
then x is Element of E by Def1;
then A3: not x in B by A1, A2;
x in E by A2, Lm1;
hence x in B ` by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B ` or x in A )
assume A4: x in B ` ; ::_thesis: x in A
B ` in bool E by Def1;
then B ` c= E by ZFMISC_1:def_1;
then x in E by A4, TARSKI:def_3;
then reconsider x = x as Element of E by Def1;
not x in B by A4, XBOOLE_0:def_5;
hence x in A by A1; ::_thesis: verum
end;
theorem :: SUBSET_1:31
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( not x in A iff x in B ) ) holds
A = B `
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E holds
( not x in A iff x in B ) ) holds
A = B `
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E holds
( not x in A iff x in B ) ) implies A = B ` )
assume for x being Element of E holds
( not x in A iff x in B ) ; ::_thesis: A = B `
then for x being Element of E holds
( x in A iff not x in B ) ;
hence A = B ` by Th30; ::_thesis: verum
end;
theorem :: SUBSET_1:32
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( ( x in A & not x in B ) or ( x in B & not x in A ) ) ) holds
A = B `
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E holds
( ( x in A & not x in B ) or ( x in B & not x in A ) ) ) holds
A = B `
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E holds
( ( x in A & not x in B ) or ( x in B & not x in A ) ) ) implies A = B ` )
assume for x being Element of E holds
( ( x in A & not x in B ) or ( x in B & not x in A ) ) ; ::_thesis: A = B `
then for x being Element of E holds
( x in A iff not x in B ) ;
hence A = B ` by Th30; ::_thesis: verum
end;
theorem :: SUBSET_1:33
for X being set
for x1 being Element of X st X <> {} holds
{x1} is Subset of X
proof
let X be set ; ::_thesis: for x1 being Element of X st X <> {} holds
{x1} is Subset of X
let x1 be Element of X; ::_thesis: ( X <> {} implies {x1} is Subset of X )
assume X <> {} ; ::_thesis: {x1} is Subset of X
then A1: x1 in X by Def1;
{x1} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1} or x in X )
assume x in {x1} ; ::_thesis: x in X
hence x in X by A1, TARSKI:def_1; ::_thesis: verum
end;
then {x1} in bool X by ZFMISC_1:def_1;
hence {x1} is Subset of X by Def1; ::_thesis: verum
end;
theorem :: SUBSET_1:34
for X being set
for x1, x2 being Element of X st X <> {} holds
{x1,x2} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2 being Element of X st X <> {} holds
{x1,x2} is Subset of X
let x1, x2 be Element of X; ::_thesis: ( X <> {} implies {x1,x2} is Subset of X )
assume X <> {} ; ::_thesis: {x1,x2} is Subset of X
then A1: ( x1 in X & x2 in X ) by Def1;
{x1,x2} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2} or x in X )
assume x in {x1,x2} ; ::_thesis: x in X
hence x in X by A1, TARSKI:def_2; ::_thesis: verum
end;
then {x1,x2} in bool X by ZFMISC_1:def_1;
hence {x1,x2} is Subset of X by Def1; ::_thesis: verum
end;
theorem :: SUBSET_1:35
for X being set
for x1, x2, x3 being Element of X st X <> {} holds
{x1,x2,x3} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3 being Element of X st X <> {} holds
{x1,x2,x3} is Subset of X
let x1, x2, x3 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3} is Subset of X
then A2: x3 in X by Def1;
A3: ( x1 in X & x2 in X ) by A1, Def1;
{x1,x2,x3} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3} or x in X )
assume x in {x1,x2,x3} ; ::_thesis: x in X
hence x in X by A3, A2, ENUMSET1:def_1; ::_thesis: verum
end;
then {x1,x2,x3} in bool X by ZFMISC_1:def_1;
hence {x1,x2,x3} is Subset of X by Def1; ::_thesis: verum
end;
theorem :: SUBSET_1:36
for X being set
for x1, x2, x3, x4 being Element of X st X <> {} holds
{x1,x2,x3,x4} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4 being Element of X st X <> {} holds
{x1,x2,x3,x4} is Subset of X
let x1, x2, x3, x4 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4} is Subset of X
then A2: ( x3 in X & x4 in X ) by Def1;
A3: ( x1 in X & x2 in X ) by A1, Def1;
{x1,x2,x3,x4} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4} or x in X )
assume x in {x1,x2,x3,x4} ; ::_thesis: x in X
hence x in X by A3, A2, ENUMSET1:def_2; ::_thesis: verum
end;
then {x1,x2,x3,x4} in bool X by ZFMISC_1:def_1;
hence {x1,x2,x3,x4} is Subset of X by Def1; ::_thesis: verum
end;
theorem :: SUBSET_1:37
for X being set
for x1, x2, x3, x4, x5 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4, x5 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5} is Subset of X
let x1, x2, x3, x4, x5 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4,x5} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4,x5} is Subset of X
{x1,x2,x3,x4,x5} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5} or x in X )
A2: ( not x in {x1,x2,x3,x4,x5} or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) by ENUMSET1:def_3;
assume x in {x1,x2,x3,x4,x5} ; ::_thesis: x in X
hence x in X by A1, A2, Def1; ::_thesis: verum
end;
then {x1,x2,x3,x4,x5} in bool X by ZFMISC_1:def_1;
hence {x1,x2,x3,x4,x5} is Subset of X by Def1; ::_thesis: verum
end;
theorem :: SUBSET_1:38
for X being set
for x1, x2, x3, x4, x5, x6 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4, x5, x6 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6} is Subset of X
let x1, x2, x3, x4, x5, x6 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4,x5,x6} is Subset of X
{x1,x2,x3,x4,x5,x6} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5,x6} or x in X )
A2: ( not x in {x1,x2,x3,x4,x5,x6} or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) by ENUMSET1:def_4;
assume x in {x1,x2,x3,x4,x5,x6} ; ::_thesis: x in X
hence x in X by A1, A2, Def1; ::_thesis: verum
end;
then {x1,x2,x3,x4,x5,x6} in bool X by ZFMISC_1:def_1;
hence {x1,x2,x3,x4,x5,x6} is Subset of X by Def1; ::_thesis: verum
end;
theorem :: SUBSET_1:39
for X being set
for x1, x2, x3, x4, x5, x6, x7 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4, x5, x6, x7 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7} is Subset of X
let x1, x2, x3, x4, x5, x6, x7 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} is Subset of X
{x1,x2,x3,x4,x5,x6,x7} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5,x6,x7} or x in X )
A2: ( not x in {x1,x2,x3,x4,x5,x6,x7} or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) by ENUMSET1:def_5;
assume x in {x1,x2,x3,x4,x5,x6,x7} ; ::_thesis: x in X
hence x in X by A1, A2, Def1; ::_thesis: verum
end;
then {x1,x2,x3,x4,x5,x6,x7} in bool X by ZFMISC_1:def_1;
hence {x1,x2,x3,x4,x5,x6,x7} is Subset of X by Def1; ::_thesis: verum
end;
theorem :: SUBSET_1:40
for X being set
for x1, x2, x3, x4, x5, x6, x7, x8 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4, x5, x6, x7, x8 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
let x1, x2, x3, x4, x5, x6, x7, x8 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
{x1,x2,x3,x4,x5,x6,x7,x8} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5,x6,x7,x8} or x in X )
A2: ( not x in {x1,x2,x3,x4,x5,x6,x7,x8} or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) by ENUMSET1:def_6;
assume x in {x1,x2,x3,x4,x5,x6,x7,x8} ; ::_thesis: x in X
hence x in X by A1, A2, Def1; ::_thesis: verum
end;
then {x1,x2,x3,x4,x5,x6,x7,x8} in bool X by ZFMISC_1:def_1;
hence {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X by Def1; ::_thesis: verum
end;
theorem :: SUBSET_1:41
for x, X being set st x in X holds
{x} is Subset of X
proof
let x, X be set ; ::_thesis: ( x in X implies {x} is Subset of X )
assume x in X ; ::_thesis: {x} is Subset of X
then {x} c= X by ZFMISC_1:31;
then {x} in bool X by ZFMISC_1:def_1;
hence {x} is Subset of X by Def1; ::_thesis: verum
end;
scheme :: SUBSET_1:sch 1
SubsetEx{ F1() -> set , P1[ set ] } :
ex X being Subset of F1() st
for x being set holds
( x in X iff ( x in F1() & P1[x] ) )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch_1();
X c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in F1() )
thus ( not x in X or x in F1() ) by A1; ::_thesis: verum
end;
then X in bool F1() by ZFMISC_1:def_1;
then reconsider X = X as Subset of F1() by Def1;
take X ; ::_thesis: for x being set holds
( x in X iff ( x in F1() & P1[x] ) )
thus for x being set holds
( x in X iff ( x in F1() & P1[x] ) ) by A1; ::_thesis: verum
end;
scheme :: SUBSET_1:sch 2
SubsetEq{ F1() -> set , F2() -> Subset of F1(), F3() -> Subset of F1(), P1[ set ] } :
F2() = F3()
provided
A1: for y being Element of F1() holds
( y in F2() iff P1[y] ) and
A2: for y being Element of F1() holds
( y in F3() iff P1[y] )
proof
for x being Element of F1() holds
( x in F2() iff x in F3() )
proof
let x be Element of F1(); ::_thesis: ( x in F2() iff x in F3() )
hereby ::_thesis: ( x in F3() implies x in F2() )
assume x in F2() ; ::_thesis: x in F3()
then P1[x] by A1;
hence x in F3() by A2; ::_thesis: verum
end;
assume x in F3() ; ::_thesis: x in F2()
then P1[x] by A2;
hence x in F2() by A1; ::_thesis: verum
end;
hence F2() = F3() by Th3; ::_thesis: verum
end;
definition
let X, Y be non empty set ;
:: original: misses
redefine predX misses Y;
irreflexivity
for X being non empty set holds R5(b1,b1)
proof
let A be non empty set ; ::_thesis: R5(A,A)
ex x being set st x in A by XBOOLE_0:def_1;
hence R5(A,A) by XBOOLE_0:3; ::_thesis: verum
end;
end;
definition
let X, Y be non empty set ;
:: original: misses
redefine predX meets Y;
reflexivity
for X being non empty set holds R5(b1,b1)
proof
let A be non empty set ; ::_thesis: R5(A,A)
thus not A misses A ; ::_thesis: verum
end;
end;
definition
let S be set ;
func choose S -> Element of S equals :: SUBSET_1:def 5
the Element of S;
correctness
coherence
the Element of S is Element of S;
;
end;
:: deftheorem defines choose SUBSET_1:def_5_:_
for S being set holds choose S = the Element of S;
begin
Lm2: for X, Y being set st ( for x being set st x in X holds
x in Y ) holds
X is Subset of Y
proof
let X, Y be set ; ::_thesis: ( ( for x being set st x in X holds
x in Y ) implies X is Subset of Y )
assume for x being set st x in X holds
x in Y ; ::_thesis: X is Subset of Y
then X c= Y by TARSKI:def_3;
then X in bool Y by ZFMISC_1:def_1;
hence X is Subset of Y by Def1; ::_thesis: verum
end;
Lm3: for x, E being set
for A being Subset of E st x in A holds
x is Element of E
proof
let x, E be set ; ::_thesis: for A being Subset of E st x in A holds
x is Element of E
let A be Subset of E; ::_thesis: ( x in A implies x is Element of E )
assume x in A ; ::_thesis: x is Element of E
then x in E by Lm1;
hence x is Element of E by Def1; ::_thesis: verum
end;
scheme :: SUBSET_1:sch 3
SubsetEx{ F1() -> non empty set , P1[ set ] } :
ex B being Subset of F1() st
for x being Element of F1() holds
( x in B iff P1[x] )
proof
consider B being set such that
A1: for x being set holds
( x in B iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch_1();
for x being set st x in B holds
x in F1() by A1;
then reconsider B = B as Subset of F1() by Lm2;
take B ; ::_thesis: for x being Element of F1() holds
( x in B iff P1[x] )
let x be Element of F1(); ::_thesis: ( x in B iff P1[x] )
x in F1() by Def1;
hence ( x in B iff P1[x] ) by A1; ::_thesis: verum
end;
scheme :: SUBSET_1:sch 4
SubComp{ F1() -> set , F2() -> Subset of F1(), F3() -> Subset of F1(), P1[ set ] } :
F2() = F3()
provided
A1: for X being Element of F1() holds
( X in F2() iff P1[X] ) and
A2: for X being Element of F1() holds
( X in F3() iff P1[X] )
proof
thus F2() c= F3() :: according to XBOOLE_0:def_10 ::_thesis: F3() c= F2()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F2() or x in F3() )
assume A3: x in F2() ; ::_thesis: x in F3()
then reconsider X = x as Element of F1() by Lm3;
P1[X] by A1, A3;
hence x in F3() by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F3() or x in F2() )
assume A4: x in F3() ; ::_thesis: x in F2()
then reconsider X = x as Element of F1() by Lm3;
P1[X] by A2, A4;
hence x in F2() by A1; ::_thesis: verum
end;
theorem :: SUBSET_1:42
for E being set
for A, B being Subset of E st A ` = B ` holds
A = B
proof
let E be set ; ::_thesis: for A, B being Subset of E st A ` = B ` holds
A = B
let A, B be Subset of E; ::_thesis: ( A ` = B ` implies A = B )
assume A ` = B ` ; ::_thesis: A = B
hence A = (B `) `
.= B ;
::_thesis: verum
end;
registration
let X be empty set ;
cluster -> empty for Element of bool X;
coherence
for b1 being Subset of X holds b1 is empty
proof
let Y be Subset of X; ::_thesis: Y is empty
Y in bool X by Def1;
then Y c= X by ZFMISC_1:def_1;
hence Y is empty by XBOOLE_1:3; ::_thesis: verum
end;
end;
definition
let E be set ;
let A be Subset of E;
attrA is proper means :: SUBSET_1:def 6
A <> E;
end;
:: deftheorem defines proper SUBSET_1:def_6_:_
for E being set
for A being Subset of E holds
( A is proper iff A <> E );
registration
let E be set ;
cluster [#] E -> non proper ;
coherence
not [#] E is proper
proof
thus [#] E = E ; :: according to SUBSET_1:def_6 ::_thesis: verum
end;
end;
registration
let E be set ;
cluster non proper for Element of bool E;
existence
not for b1 being Subset of E holds b1 is proper
proof
take [#] E ; ::_thesis: not [#] E is proper
thus not [#] E is proper ; ::_thesis: verum
end;
end;
registration
let E be non empty set ;
cluster non proper -> non empty for Element of bool E;
coherence
for b1 being Subset of E st not b1 is proper holds
not b1 is empty
proof
let A be Subset of E; ::_thesis: ( not A is proper implies not A is empty )
assume A = E ; :: according to SUBSET_1:def_6 ::_thesis: not A is empty
hence not A is empty ; ::_thesis: verum
end;
cluster empty -> proper for Element of bool E;
coherence
for b1 being Subset of E st b1 is empty holds
b1 is proper ;
end;
registration
let E be non empty set ;
cluster proper for Element of bool E;
existence
ex b1 being Subset of E st b1 is proper
proof
take {} E ; ::_thesis: {} E is proper
thus {} E <> E ; :: according to SUBSET_1:def_6 ::_thesis: verum
end;
end;
registration
let E be empty set ;
cluster -> non proper for Element of bool E;
coherence
for b1 being Subset of E holds not b1 is proper
proof
let A be Subset of E; ::_thesis: not A is proper
thus A = E ; :: according to SUBSET_1:def_6 ::_thesis: verum
end;
end;
theorem :: SUBSET_1:43
for X, Y, A, z being set st z in A & A c= [:X,Y:] holds
ex x being Element of X ex y being Element of Y st z = [x,y]
proof
let X, Y, A be set ; ::_thesis: for z being set st z in A & A c= [:X,Y:] holds
ex x being Element of X ex y being Element of Y st z = [x,y]
let z be set ; ::_thesis: ( z in A & A c= [:X,Y:] implies ex x being Element of X ex y being Element of Y st z = [x,y] )
assume ( z in A & A c= [:X,Y:] ) ; ::_thesis: ex x being Element of X ex y being Element of Y st z = [x,y]
then consider x, y being set such that
A1: x in X and
A2: y in Y and
A3: z = [x,y] by ZFMISC_1:84;
reconsider y = y as Element of Y by A2, Def1;
reconsider x = x as Element of X by A1, Def1;
take x ; ::_thesis: ex y being Element of Y st z = [x,y]
take y ; ::_thesis: z = [x,y]
thus z = [x,y] by A3; ::_thesis: verum
end;
theorem :: SUBSET_1:44
for X being non empty set
for A, B being non empty Subset of X st A c< B holds
ex p being Element of X st
( p in B & A c= B \ {p} )
proof
let X be non empty set ; ::_thesis: for A, B being non empty Subset of X st A c< B holds
ex p being Element of X st
( p in B & A c= B \ {p} )
let A, B be non empty Subset of X; ::_thesis: ( A c< B implies ex p being Element of X st
( p in B & A c= B \ {p} ) )
assume A1: A c< B ; ::_thesis: ex p being Element of X st
( p in B & A c= B \ {p} )
then consider p being Element of X such that
A2: p in B \ A by Th4, XBOOLE_1:105;
A3: not p in A by A2, XBOOLE_0:def_5;
take p ; ::_thesis: ( p in B & A c= B \ {p} )
A c= B by A1, XBOOLE_0:def_8;
hence ( p in B & A c= B \ {p} ) by A2, A3, XBOOLE_0:def_5, ZFMISC_1:34; ::_thesis: verum
end;
definition
let X be non empty set ;
redefine attr X is trivial means :: SUBSET_1:def 7
for x, y being Element of X holds x = y;
compatibility
( X is trivial iff for x, y being Element of X holds x = y )
proof
thus ( X is trivial implies for x, y being Element of X holds x = y ) ::_thesis: ( ( for x, y being Element of X holds x = y ) implies X is trivial )
proof
assume A1: X is trivial ; ::_thesis: for x, y being Element of X holds x = y
let x, y be Element of X; ::_thesis: x = y
( x in X & y in X ) by Def1;
hence x = y by A1, ZFMISC_1:def_10; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x = y ; ::_thesis: X is trivial
let x, y be set ; :: according to ZFMISC_1:def_10 ::_thesis: ( not x in X or not y in X or x = y )
assume ( x in X & y in X ) ; ::_thesis: x = y
then ( x is Element of X & y is Element of X ) by Def1;
hence x = y by A2; ::_thesis: verum
end;
end;
:: deftheorem defines trivial SUBSET_1:def_7_:_
for X being non empty set holds
( X is trivial iff for x, y being Element of X holds x = y );
registration
let X be non empty set ;
cluster non empty trivial for Element of bool X;
existence
ex b1 being Subset of X st
( not b1 is empty & b1 is trivial )
proof
the Element of X in X by Def1;
then { the Element of X} c= X by ZFMISC_1:31;
then { the Element of X} in bool X by ZFMISC_1:def_1;
then reconsider A = { the Element of X} as Subset of X by Def1;
take A ; ::_thesis: ( not A is empty & A is trivial )
thus not A is empty ; ::_thesis: A is trivial
let x, y be set ; :: according to ZFMISC_1:def_10 ::_thesis: ( not x in A or not y in A or x = y )
assume ( x in A & y in A ) ; ::_thesis: x = y
then ( x = the Element of X & y = the Element of X ) by TARSKI:def_1;
hence x = y ; ::_thesis: verum
end;
end;
registration
let X be trivial set ;
cluster -> trivial for Element of bool X;
coherence
for b1 being Subset of X holds b1 is trivial
proof
let Y be Subset of X; ::_thesis: Y is trivial
let x, y be set ; :: according to ZFMISC_1:def_10 ::_thesis: ( not x in Y or not y in Y or x = y )
assume ( x in Y & y in Y ) ; ::_thesis: x = y
then ( x in X & y in X ) by Lm1;
hence x = y by ZFMISC_1:def_10; ::_thesis: verum
end;
end;
registration
let X be non trivial set ;
cluster non trivial for Element of bool X;
existence
not for b1 being Subset of X holds b1 is trivial
proof
take [#] X ; ::_thesis: not [#] X is trivial
thus not [#] X is trivial ; ::_thesis: verum
end;
end;
theorem :: SUBSET_1:45
for D being set
for A being Subset of D st not A is trivial holds
ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
proof
let D be set ; ::_thesis: for A being Subset of D st not A is trivial holds
ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
let A be Subset of D; ::_thesis: ( not A is trivial implies ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 ) )
assume not A is trivial ; ::_thesis: ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
then consider d1, d2 being set such that
A1: ( d1 in A & d2 in A ) and
A2: d1 <> d2 by ZFMISC_1:def_10;
( d1 in D & d2 in D ) by A1, Lm1;
then reconsider d1 = d1, d2 = d2 as Element of D by Def1;
take d1 ; ::_thesis: ex d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
take d2 ; ::_thesis: ( d1 in A & d2 in A & d1 <> d2 )
thus ( d1 in A & d2 in A & d1 <> d2 ) by A1, A2; ::_thesis: verum
end;
theorem Th46: :: SUBSET_1:46
for X being non empty trivial set ex x being Element of X st X = {x}
proof
let X be non empty trivial set ; ::_thesis: ex x being Element of X st X = {x}
consider x being set such that
A1: X = {x} by ZFMISC_1:131;
x in X by A1, TARSKI:def_1;
then reconsider x = x as Element of X by Def1;
take x ; ::_thesis: X = {x}
thus X = {x} by A1; ::_thesis: verum
end;
theorem :: SUBSET_1:47
for X being non empty set
for A being non empty Subset of X st A is trivial holds
ex x being Element of X st A = {x}
proof
let X be non empty set ; ::_thesis: for A being non empty Subset of X st A is trivial holds
ex x being Element of X st A = {x}
let A be non empty Subset of X; ::_thesis: ( A is trivial implies ex x being Element of X st A = {x} )
assume A is trivial ; ::_thesis: ex x being Element of X st A = {x}
then ex s being Element of A st A = {s} by Th46;
hence ex x being Element of X st A = {x} ; ::_thesis: verum
end;
theorem :: SUBSET_1:48
for X being non trivial set
for x being Element of X ex y being set st
( y in X & x <> y )
proof
let X be non trivial set ; ::_thesis: for x being Element of X ex y being set st
( y in X & x <> y )
let x be Element of X; ::_thesis: ex y being set st
( y in X & x <> y )
consider d1, d2 being set such that
A1: ( d1 in X & d2 in X ) and
A2: d1 <> d2 by ZFMISC_1:def_10;
( x <> d1 or x <> d2 ) by A2;
hence ex y being set st
( y in X & x <> y ) by A1; ::_thesis: verum
end;