1. A : Type
2. B : Type
3. x : (A inj B)(A onto B)
  x  A bij B

By:	(3) Def of A inj B | A onto B THEN Witness'3: 0 with type 2 THEN Witness'3: 1 with type 2 THEN OnAllHyps Reduce

1

3. x :  3. i:2. if i=0 {f:(AB)| Inj(A; B; f) } else {f:(AB)| Surj(A; B; f) } fi 4. 0  2 5. y : {f:(AB)| Inj(A; B; f) } 6. y = x  {f:(AB)| Inj(A; B; f) } 7. 1  2 8. y1 : {f:(AB)| Surj(A; B; f) } 9. y1 = x  {f:(AB)| Surj(A; B; f) }   x  A bij B

5 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html