Nuprl - Proof: nsub bij ooc invpair 1 3 2

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

1. a :

2. (

f.<f,

y.least x:

. f(x)=

y>)

(

a bij

a
3. (

fg.fg/f,g. f)

(

a bij

y:(

a). (

f.<f,

y.least x:

. f(x)=

y>)((

fg.fg/f,g. f)(y)) = y

By:	Analyze THEN Analyze-1 THEN New:[f \| g] Analyze-2 THEN Reduce Hyp:-1

Generated subgoal:

1 4. f : aa
5. g : aa
6. InvFuns(a;a;f;g)
(f.<f,y.least x:. f(x)=y>)((fg.fg/f,g. f)(<f,g>)) = <f,g> aa
13 steps

About:

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