(* This is repaired to work with the June 22 upgrade, which reduces
the aggressiveness of the right equality rule. *)

(* 0 *)

hardcomment "empty set";



(* 1 *)  Definefunction 0 "Null" "Null" "{x1|~x1=x1}"; 
(* 2 *)  

(* 1 *)

hardcomment "singleton set";



(* 2 *)  Definefunction 1 "Sing" "Sing(x1)" "{x2|x2=x1}"; 
(* 3 *)  

(* 2 *)

hardcomment "the Frege natural number zero";



(* 3 *)  Definefunction 0 "Zero" "Zero" "Sing(Null)"; 
(* 4 *)  

(* 3 *)

hardcomment "The universal set";



(* 4 *)  Definefunction 0 "V" "V" "{x1|x1=x1}"; 
(* 5 *)  

(* 4 *)

hardcomment "The sethood predicate";



(* 5 *)  Definepredicate 1 "Set" "Set(x1)" "x1=Null v (Ex2.x2Ex1)"; 
(* 6 *)  

(* 5 *)

hardcomment "The subset relation:";



(* 5 *)

hardcomment "the sethood conditions are expensive";



(* 6 *)  Definepredicate 2 "c" "x1 c x2" "Set(x1)&Set(x2)&(Ax3.x3Ex1->x3Ex2)"; 
(* 7 *)  

(* 6 *)

hardcomment "The extension of an object (the set with the same elements)";



(* 7 *)  Definefunction 1 "Ext" "Ext(x1)" "{x2|x2Ex1}"; 
(* 8 *)  

(* 7 *)

hardcomment "The power set";



(* 8 *)  Definefunction 1 "Sc" "Sc(x1)" "{x2|x2 c x1}"; 
(* 9 *)  

(* 8 *)

hardcomment "The set of all one-element subsets";



(* 9 *)  Definefunction 1 "Usc" "Usc(x1)" "{Sing(x2)|x2 E x1}"; 
(* 10 *)  

(* 9 *)

hardcomment "x1 is a function from x2 to x3";



(* 10 *)  Definepredicate 3 "Function" "Function(x1,x2,x3)" "Set(x1)&Set(x2)&Set(x3)&(Ax4:x2.(Ex5:x3.[x4,x5]Ex1))&(Ax6:x1.(Ax7:x1.p1(x6)=p1(x7)->x6=x7))"; 
(* 11 *)  

(* 10 *)

hardcomment "The converse of a relation";



(* 11 *)  Definefunction 1 "Converse" "Converse(x1)" "{[x3,x2]|[x2,x3]Ex1}"; 
(* 12 *)  

(* 11 *)

hardcomment "x1 is a bijection from x2 to x3";



(* 12 *)  Definepredicate 3 "Bijection" "Bijection(x1,x2,x3)" "Function(x1,x2,x3)&Function(Converse(x1),x3,x2)"; 
(* 13 *)  

(* 12 *)

hardcomment "x1 and x2 are sets of the same size";



(* 13 *)  Definepredicate 2 "sim" "x1 sim x2" "(Ex3.Bijection(x3,x1,x2))"; 
(* 14 *)  

(* 13 *)

hardcomment "The relative product of two relations";



(* 14 *)  Definefunction 2 "Relprod" "x1 Relprod x2" "{[x3,x4]|(Ex5.[x3,x5]Ex1&[x5,x4]Ex2)}"; 
(* 15 *)  

(* 14 *)

hardcomment "The unordered pair";



(* 15 *)  Definefunction 2 "Couple" "x1Couple x2" "{x3|x3=x1vx3=x2}"; 
(* 16 *)  

(* 15 *)

hardcomment "The Kuratowski ordered pair";



(* 16 *)  Definefunction 2 "Kpair" "x1 Kpair x2" "Sing(x1) Couple x1 Couple x2"; 
(* 17 *)  

(* 16 *)

hardcomment "A theorem on equality of unordered pairs";



(* 17 *)  StartSequent [] ["a1Couple a2 = a3Couple a4 -> a1=a3&a2=a4va1=a4&a2=a3"]; 
(* 18 *)  r(); r(); r(); gr 2; r(); l(); l(); l(); l(); r(); r(); l(); gl 1; gr 2; Done(); 
(* 33 *)  Done(); 
(* 34 *)  l(); l(); l(); gl 2; l(); r(); r(); l(); gr 2; rwr [1]; r(); rwr [1]; r(); gr 2; r(); l(); l(); l(); gr 2; r(); undo(); gl 2; l(); r(); gr 2; r(); l(); gr 2; rwr [1]; r(); rwr [1]; r(); l(); l(); l(); l(); r(); gr 2; r(); l(); Done(); 
(* 75 *)  gr 2; Done(); 
(* 77 *)  NameSequent 2 "CoupleEq"; 
(* 78 *)  

(* 77

CoupleEq:



1:  a1 Couple a2 = a3 Couple a4

|-

1:  a1 = a3 & a2 = a4 v a1 = a4
      & a2 = a3

*)



(* 77 *)

hardcomment "The main theorem about the usual ordered pair, only half proved";



(* 78 *)  StartSequent [] ["a1Kpair a2 = a3Kpair a4 -> a1=a3&a2=a4"]; 
(* 79 *)  r(); l(); l(); r(); l(); l(); l(); undo(); r(); su 5 "Sing(a3)"; 
(* 89 *)  l(); r(); r(); l(); Done(); 
(* 94 *)  gl 1; gr 2; Done(); 
(* 97 *)  gl 2; l(); r(); r(); l(); l(); l(); l(); l(); r(); gl 2; l(); gl 6; gr 1; Done(); 
(* 112 *)  gl 7; rwr [1]; r(); l(); l(); l(); l(); r(); l(); rwr [1]; r(); gl 2; l(); r(); gl 6; gr 2; Done(); 
(* 129 *)  gl 2; l(); su 5 "a2"; 
(* 132 *)  l(); gl 2; l(); r(); gr 2; r(); gl 9; l(); Done(); 
(* 141 *)  l(); rwr [1]; crwr [1]; gl 2; gr 1; Done(); 
(* 147 *)  gl 3; l(); su 5 "a2"; 
(* 150 *)  l(); gl 2; l(); r(); gr 2; r(); gl 3; l(); l(); l(); gl 2; l(); l(); undo(); r(); r(); Done(); 
(* 167 *)  

(* 167 *)  StartSequent [] ["~a1ENull"]; 
(* 168 *)  r(); r(); l(); l(); r(); NameSequent 1 "NullIsEmpty"; 
(* 174 *)  

(* 173

NullIsEmpty:



|-

1:  ~a1 E Null

*)



(* 173 *)

hardcomment "The empty set has no elements";



(* 174 *)  StartSequent [] ["a1EV"]; 
(* 175 *)  r(); r(); NameSequent 1 "VIsUniversal"; 
(* 178 *)  

(* 177

VIsUniversal:



|-

1:  a1 E V

*)



(* 177 *)

hardcomment "The universal set contains everything";



(* 178 *)  StartSequent [] ["Set(Ext(a1))"]; 
(* 179 *)  r(); r(); r(); r(); r(); r(); gr 2; r(); r(); Done(); 
(* 190 *)  l(); r(); NameSequent 1 "SetExt"; 
(* 193 *)  

(* 192

SetExt:



|-

1:  Set(Ext(a1))

*)



(* 192 *)

hardcomment "The extension of an object is a set";



(* 193 *)  StartSequent [] ["a1 c a2 & a2 c a1 -> Ext(a1)=Ext(a2)"]; 
(* 194 *)  r(); l(); r(); r(); l(); gl 2; l(); l(); gl 2; l(); gl 3; l(); gl 2; l(); r(); r(); r(); gl 3; l(); l(); gl 6; gr 1; Done(); 
(* 217 *)  Done(); 
(* 218 *)  gl 6; l(); l(); gl 3; gr 1; Done(); 
(* 224 *)  Done(); 
(* 225 *)  NameSequent 1 "SubAntiSymm"; 
(* 226 *)  

(* 225

SubAntiSymm:



|-

1:  a1 c a2 & a2 c a1
      -> Ext(a1) = Ext(a2)

*)



(* 225 *)

hardcomment "subset relation is antisymmetric in a weak sense";



(* 225 *)

hardcomment "Inclusion is actually strictly antisymmetric, not just up to extension";



(* 226 *)  StartSequent [] ["a1 c a2 & a2 c a1 -> a1=a2"]; 
(* 227 *)  r(); l(); gl 1; l(); gl 2; l(); gl 1; l(); gl 3; l(); gl 2; l(); gl 4; l(); l(); l(); gl 4; l(); l(); rwr [1]; gl 4; gr 1; Done(); 
(* 250 *)  l(); r(); gl 1; gr 2; Done(); 
(* 255 *)  r(); r(); gl 3; l(); l(); gl 6; gr 1; Done(); 
(* 263 *)  Done(); 
(* 264 *)  gl 6; l(); l(); gl 3; gr 1; Done(); 
(* 270 *)  Done(); 
(* 271 *)  l(); r(); Done(); 
(* 274 *)  r(); r(); gl 6; l(); l(); gl 3; gr 1; Done(); 
(* 282 *)  Done(); 
(* 283 *)  gl 3; l(); l(); gl 6; gr 1; Done(); 
(* 289 *)  Done(); 
(* 290 *)  NameSequent 1 "StrictSubAntiSymm"; 
(* 291 *)  

(* 290

StrictSubAntiSymm:



|-

1:  a1 c a2 & a2 c a1 -> a1 = a2

*)



(* 290 *)

hardcomment "Power sets are sets";



(* 291 *)  StartSequent [] ["Set(Sc(a1))"]; 
(* 292 *)  r(); r(); r(); r(); r(); r(); gr 2; r(); r(); Done(); 
(* 301 *)  l(); r(); NameSequent 1 "SetSc"; 
(* 304 *)  

(* 303

SetSc:



|-

1:  Set(Sc(a1))

*)



(* 303 *)

hardcomment "The class of one-element subsets is a set";



(* 304 *)  StartSequent [] ["Set(Usc(a1))"]; 
(* 305 *)  r(); r(); r(); r(); r(); r(); l(); gr 2; r(); su 4 "a2"; 
(* 314 *)  r(); Done(); 
(* 316 *)  gl 2; gr 1; Done(); 
(* 319 *)  l(); l(); r(); NameSequent 1 "SetUsc"; 
(* 323 *)  

(* 322

SetUsc:



|-

1:  Set(Usc(a1))

*)



(* 322 *)

hardcomment "The class of one element subsets is a subset of the power set";



(* 323 *)  StartSequent [] ["Usc(a1) c Sc(a1)"]; 
(* 324 *)  r(); r(); UseThm "SetUsc" [] [1]; 
(* 327 *)  r(); UseThm "SetSc" [] [1]; 
(* 329 *)  r(); r(); l(); r(); r(); r(); r(); r(); gr 2; r(); su 4 "a3"; 
(* 340 *)  rwr [1]; r(); r(); r(); r(); r(); gr 2; r(); gl 2; gr 1; Done(); 
(* 351 *)  r(); l(); undo(); r(); gl 2; rwl [1]; gl2 3; rwl [1]; gl 2; l(); rwl [1]; crwl [1]; gl 2; gr 1; Done(); 
(* 366 *)  NameSequent 1 "UsccSc"; 
(* 367 *)  

(* 366

UsccSc:



|-

1:  Usc(a1) c Sc(a1)

*)



(* 366 *)

hardcomment "Singleton sets are sets";



(* 367 *)  StartSequent [] ["Set(Sing(a1))"]; 
(* 368 *)  r(); r(); gr 2; r(); su 2 "a1"; 
(* 373 *)  r(); r(); NameSequent 1 "SetSing"; 
(* 376 *)  

(* 375

SetSing:



|-

1:  Set(Sing(a1))

*)



(* 375 *)

hardcomment "Reflexivity of equinumerousness";



(* 376 *)  StartSequent [] ["Set(a1)->a1 sim a1"]; 
(* 377 *)  r(); r(); r(); w 1 "{[x1,x1]|x1Ea1}"; 
(* 381 *)  r(); r(); r(); r(); r(); r(); r(); r(); r(); r(); l(); gr 2; r(); r(); Done(); 
(* 395 *)  gl 2; gr 1; Done(); 
(* 398 *)  l(); l(); r(); r(); Done(); 
(* 403 *)  r(); Done(); 
(* 405 *)  r(); r(); r(); Done(); 
(* 409 *)  r(); r(); Done(); 
(* 412 *)  r(); l(); r(); l(); rwr []; gl 3; rwr []; r(); rwr []; r(); r(); r(); r(); r(); r(); r(); r(); r(); l(); gl 2; l(); l(); gr 2; r(); r(); gl 5; gr 1; Done(); 
(* 439 *)  r(); rwr [1]; gl 2; rwr [1]; r(); gl 3; gr 1; Done(); 
(* 447 *)  l(); l(); r(); r(); Done(); 
(* 452 *)  r(); Done(); 
(* 454 *)  r(); r(); r(); Done(); 
(* 458 *)  r(); r(); r(); r(); Done(); 
(* 463 *)  r(); l(); r(); l(); rwr []; gl 3; rwr []; gl 2; l(); l(); rwr []; gl 2; rwr []; gl 4; rwr []; gl 2; l(); l(); rwr []; gl 2; rwr []; r(); rwr []; r(); NameSequent 1 "SimSelf"; 
(* 488 *)  

(* 487

SimSelf:



|-

1:  Set(a1) -> a1 sim a1

*)

(* when I made the right equality rule less aggressive, I seemed
to be forced to write a quite different proof here *)

(* 488 *)  StartSequent [] ["Set(a1)->a1=Converse(Converse(a1))"]; 
r();l();l();

rwr nil;r();r();r();r();l();l();r();

l();Gl 2;Gl 2;l(); r();

l();r();r();Done();

r();r();r();r();r();r();r();r();Done();

l();Gl 2;l();rf();rf();gl 3;rwr nil;Triv 2 1;



(* (* 489 *)  r(); r(); r(); r(); l(); l(); rwr []; r(); r(); r(); l(); l(); r(); l(); gl 2; l(); gl 2; l(); l(); r(); l(); r(); r(); Done(); 
(* 511 *)  r(); r(); r(); NextGoal(); 
(* 515 *)  NextGoal(); 
(* 516 *)  su 12 "p2(a10)"; 
(* 517 *)  su 11 "p1(a10)"; 
(* 518 *)  r(); NextGoal(); 
(* 520 *)  NextGoal(); 
(* 521 *)  r(); NextGoal(); 
(* 523 *)  l(); RewriteFree(); l(); l(); RewriteFree(); RewriteFree(); Done(); 
(* 530 *)  r(); Done(); *)


(* 532 *)  NameSequent 2 "Converse2"; 
(* 533 *)  

(* 532

Converse2:



1:  Set(a1)

|-

1:  a1 = Converse(Converse(a1))

*)



(* 532 *)

hardcomment "The converse of the converse is the relation itself";



(* 533 *)  StartSequent [] ["a1 sim a2 -> a2 sim a1"]; 
(* 534 *)  r(); l(); l(); r(); r(); su 4 "Converse(a3)"; 
(* 540 *)  l(); l(); r(); r(); gl 2; gr 1; Done(); 
(* 547 *)  ThmCut "Converse2"; 
(* 548 *)  su 4 "a3"; 
(* 549 *)  l(); l(); Done(); 
(* 552 *)  rwr []; crwr []; crwr []; gl 2; gr 1; Done(); 
(* 558 *)  NameSequent 1 "SimSymm"; 
(* 559 *)  

(* 558

SimSymm:



|-

1:  a1 sim a2 -> a2 sim a1

*)



(* 558 *)

hardcomment "Relative products of functions with appropriate domain and range are functions";



(* 559 *)  StartSequent [] ["Function(a1,a3,a4)&Function(a2,a4,a5)->Function(a1 Relprod a2,a3,a5)"]; 
(* 560 *)  r(); r(); r(); r(); r(); r(); r(); r(); r(); l(); RewriteFree(); gr 2; r(); su 9 "[a7,a8]"; 
(* 573 *)  r(); r(); Done(); 
(* 576 *)  l(); l(); r(); AutoPrune(); NameSequent 4 "RelProdSet"; 
(* 581 *)  

(* 580

RelProdSet:



|-

1:  Set(a1 Relprod a2)

*)


(* Sequent snapshot:


1:  Function(a1,a3,a4) & Function(a2,a4,a5)

|-

1:  Set(a3)
      & Set(a5) & 
     (A x5 : a3.(E x6 : a5.[x5,x6] E a1 Relprod a2)) & (A 
     x7 : a1 Relprod a2.(A x8 : a1
      Relprod a2.p1(x7) = p1(x8)
      -> x7 = x8))


*)



(* 580 *)

hardcomment "Relative products are sets";


(* Sequent snapshot:


1:  Function(a1,a3,a4) & Function(a2,a4,a5)

|-

1:  Set(a3)
      & Set(a5) & 
     (A x5 : a3.(E x6 : a5.[x5,x6] E a1 Relprod a2)) & (A 
     x7 : a1 Relprod a2.(A x8 : a1
      Relprod a2.p1(x7) = p1(x8)
      -> x7 = x8))


*)

r(); l(); l(); l(); gl 2; l(); Done(); 
(* 588 *)  r(); l(); gl 2; l(); l(); gl 2; l(); gl 2; l(); Done(); 
(* 598 *)  r(); r(); gl 2; l(); l(); l(); pl 1; l(); pl 1; l(); pl 1; l(); l(); gl 4; gr 1; Done(); 
(* 614 *)  l(); AutoPrune(); gl 5; l(); l(); pl 1; l(); pl 1; l(); pl 1; l(); l(); gl 4; gr 1; Done(); 
(* 629 *)  l(); r(); Done(); 
(* 632 *)  r(); r(); r(); r(); gl 7; gr 1; Done(); 
(* 639 *)  gl 2; gr 1; Done(); 
(* 642 *)  r(); r(); l(); RewriteFree(); gl 2; l(); RewriteFree(); r(); gl 2; l(); gl 3; l(); gl 2; RewriteFree(); l(); gl 4; l(); gl 5; l(); l(); gl 2; l(); pl 1; undo(); l(); pl 1; l(); pl 1; l(); pl 1; l(); pl 1; gl 6; l(); pl 1; l(); pl 1; l(); pl 1; l(); pl 1; l(); gl 3; gr 1; Done(); 
(* 687 *)  l(); gl 6; gr 1; Done(); 
(* 691 *)  l(); r(); l(); RewriteFree(); RewriteFree(); gl 3; l(); gl 3; gr 1; Done(); 
(* 701 *)  l(); gl 6; gr 1; Done(); 
(* 705 *)  l(); r(); l(); RewriteFree(); RewriteFree(); r(); NameSequent 1 "Comp"; 
(* 712 *)  

(* 711

Comp:



|-

1:  
     Function(a1,a3,a4) & Function(a2,a4,a5) -> Function(a1
      Relprod a2,a3,a5)

*)