:: TARSKI semantic presentation begin theorem :: TARSKI:1 for X, Y being set st ( for x being set holds ( x in X iff x in Y ) ) holds X = Y ; definition let y be set ; func{y} -> set means :: TARSKI:def 1 for x being set holds ( x in it iff x = y ); correctness existence ex b1 being set st for x being set holds ( x in b1 iff x = y ); uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x = y ) ) & ( for x being set holds ( x in b2 iff x = y ) ) holds b1 = b2; ; let z be set ; func{y,z} -> set means :: TARSKI:def 2 for x being set holds ( x in it iff ( x = y or x = z ) ); correctness existence ex b1 being set st for x being set holds ( x in b1 iff ( x = y or x = z ) ); uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = y or x = z ) ) ) & ( for x being set holds ( x in b2 iff ( x = y or x = z ) ) ) holds b1 = b2; ; commutativity for b1, y, z being set st ( for x being set holds ( x in b1 iff ( x = y or x = z ) ) ) holds for x being set holds ( x in b1 iff ( x = z or x = y ) ) ; end; :: deftheorem defines { TARSKI:def_1_:_ for y, b2 being set holds ( b2 = {y} iff for x being set holds ( x in b2 iff x = y ) ); :: deftheorem defines { TARSKI:def_2_:_ for y, z, b3 being set holds ( b3 = {y,z} iff for x being set holds ( x in b3 iff ( x = y or x = z ) ) ); definition let X, Y be set ; predX c= Y means :: TARSKI:def 3 for x being set st x in X holds x in Y; reflexivity for X, x being set st x in X holds x in X ; end; :: deftheorem defines c= TARSKI:def_3_:_ for X, Y being set holds ( X c= Y iff for x being set st x in X holds x in Y ); definition let X be set ; func union X -> set means :: TARSKI:def 4 for x being set holds ( x in it iff ex Y being set st ( x in Y & Y in X ) ); correctness existence ex b1 being set st for x being set holds ( x in b1 iff ex Y being set st ( x in Y & Y in X ) ); uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex Y being set st ( x in Y & Y in X ) ) ) & ( for x being set holds ( x in b2 iff ex Y being set st ( x in Y & Y in X ) ) ) holds b1 = b2; ; end; :: deftheorem defines union TARSKI:def_4_:_ for X, b2 being set holds ( b2 = union X iff for x being set holds ( x in b2 iff ex Y being set st ( x in Y & Y in X ) ) ); theorem :: TARSKI:2 for x, X being set st x in X holds ex Y being set st ( Y in X & ( for x being set holds ( not x in X or not x in Y ) ) ) ; scheme :: TARSKI:sch 1 Fraenkel{ F1() -> set , P1[ set , set ] } : ex X being set st for x being set holds ( x in X iff ex y being set st ( y in F1() & P1[y,x] ) ) provided for x, y, z being set st P1[x,y] & P1[x,z] holds y = z proof thus ex X being set st for x being set holds ( x in X iff ex y being set st ( y in F1() & P1[y,x] ) ) ; ::_thesis: verum end; definition let x, y be set ; func[x,y] -> set equals :: TARSKI:def 5 {{x,y},{x}}; correctness coherence {{x,y},{x}} is set ; ; end; :: deftheorem defines [ TARSKI:def_5_:_ for x, y being set holds [x,y] = {{x,y},{x}}; definition let X, Y be set ; predX,Y are_equipotent means :: TARSKI:def 6 ex Z being set st ( ( for x being set st x in X holds ex y being set st ( y in Y & [x,y] in Z ) ) & ( for y being set st y in Y holds ex x being set st ( x in X & [x,y] in Z ) ) & ( for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds ( x = z iff y = u ) ) ); end; :: deftheorem defines are_equipotent TARSKI:def_6_:_ for X, Y being set holds ( X,Y are_equipotent iff ex Z being set st ( ( for x being set st x in X holds ex y being set st ( y in Y & [x,y] in Z ) ) & ( for y being set st y in Y holds ex x being set st ( x in X & [x,y] in Z ) ) & ( for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds ( x = z iff y = u ) ) ) ); theorem :: TARSKI:3 for N being set ex M being set st ( N in M & ( for X, Y being set st X in M & Y c= X holds Y in M ) & ( for X being set st X in M holds ex Z being set st ( Z in M & ( for Y being set st Y c= X holds Y in Z ) ) ) & ( for X being set holds ( not X c= M or X,M are_equipotent or X in M ) ) ) ;