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

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

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)=

a
9. InvFuns(

a;f;

y.least x:

. f(x)=

y)
10. g = (

y.least x:

. f(x)=

<f,

y.least x:

. f(x)=

y> = <f,g>

By:	Repeat (Analyze THEN Reduce Concl)

Generated subgoals:

None

About:

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