Nuprl - Proof: nsub bij ooc invpair 1 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub bij ooc invpair 1 1 1 1 1 1

1. a :

2. f :

a bij

a
3. f

a
4. Bij(

a; f)
5. y :

(least x:

. f(x)=

By:	BackThru: Thm* f:(a onto b), y:b. (least x:. f(x)=y) a

Generated subgoals:

None

About:

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