Nuprl - Proof: bijtype exteq inj isect surjtype 1 2 1 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

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. Inj(A; B; y)
8. 1

2
9. y1 : {f:(A

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

A bij

By:	Def THEN Def of Bij(A; B; f)

Generated subgoal:

1 x {f:(AB)| Inj(A; B; f) & Surj(A; B; f) }
3 steps

About:

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