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

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

1. a :

2. (

f.<f,

y.least x:

. f(x)=

y>)

(

a bij

a
3. (

fg.fg/f,g. f)

(

a bij

a
4. f :

a
5. g :

a
6. InvFuns(

a;f;g)
7. f

a onto

a
8. (

y.least x:

. f(x)=

InvFuns(

a;f;

y.least x:

. f(x)=

By:	Def THEN Reduce Concl

Generated subgoals:

1 9. x : a
(least x@0:. f(x@0)=f(x)) = x a
4 steps

2 9. y : a
f(least x:. f(x)=y) = y
1 step

About:

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

1	9. x : a (least x@0:. f(x@0)=f(x)) = x a	4 steps
2	9. y : a f(least x:. f(x)=y) = y	1 step