Nuprl - Proof: bijtype exteq inj isect surjtype 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bijtype exteq inj isect surjtype 1 2 1

1. A : Type
2. B : Type
3. x :
3.

2. if i=

{f:(A

B)| Inj(A; B; f) } else {f:(A

B)| Surj(A; B; f) } fi
4. 0

2
5. y : {f:(A

B)| Inj(A; B; f) }
6. y = x
7. 1

2
8. y1 : {f:(A

B)| Surj(A; B; f) }
9. y1 = x

A bij

By:	Analyze9 THEN Analyze6

Generated subgoal:

1 6. y = x  AB
7. Inj(A; B; y)
8. 1  2
9. y1 : {f:(AB)| Surj(A; B; f) }
10. y1 = x  AB
11. Surj(A; B; y1)
  x  A bij B
4 steps

About:

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