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

(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

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

1. a :

2. f :

a bij

a
3. f

a onto

a
4. f

a
5. Bij(

a; f) [not for witness]
6. (

y.least x:

. f(x)=

a
7. Inj(

y.least x:

. f(x)=

y) [not for witness]

InvFuns(

a;f;

y.least x:

. f(x)=

By:	Analyze THEN Reduce Concl

Generated subgoals:

1 5. Bij(a; a; f)
6. (y.least x:. f(x)=y)  aa
7. Inj(a; a; y.least x:. f(x)=y)
8. x : a
  (least x@0:. f(x@0)=f(x)) = x  a
4 steps

2 5. Bij(a; a; f)
6. (y.least x:. f(x)=y)  aa
7. Inj(a; a; y.least x:. f(x)=y)
8. 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

(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

1	5. Bij(a; a; f) 6. (y.least x:. f(x)=y) aa 7. Inj(a; a; y.least x:. f(x)=y) 8. x : a (least x@0:. f(x@0)=f(x)) = x a	4 steps
2	5. Bij(a; a; f) 6. (y.least x:. f(x)=y) aa 7. Inj(a; a; y.least x:. f(x)=y) 8. y : a f(least x:. f(x)=y) = y	1 step