Nuprl - Proof: nsub bij least preimage inverse 1 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub bij least preimage inverse 1 1 1 2

1. a :

2. f :

a bij

a
3. f

a onto

a
4. f

a
5. Bij(

a; f)
6. (

y.least x:

. f(x)=

a
7. Inj(

y.least x:

. f(x)=

y)
8. y :

f(least x:

. f(x)=

y) = y

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

Generated subgoals:

None

About:

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