Nuprl - Proof: card nsub inj vs lopped 1 1 3 1 2 1 2

(31steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card nsub inj vs lopped 1 1 3 1 2 1 2

1. a :

2. b :

3. (

f.<f(a-1),f>)

(

a inj

b)

(i:

b

(a-1) inj

{x:

b|

x = i })
4. (

ie.ie/i,e.

x.if x=

a-1

i else e(x) fi)
4.

(i:

b

(a-1) inj

{x:

b|

x = i })

a inj

b
5. f :

a

b
6. Inj(

a;

b; f)
7. a1 :

a
8. a2 :

a
9. f(a1) = f(a-1)
10. a1

a-1
11. a2 = a-1

a1 = a2

By:	FwdThru: Inj(a; b; f) on [ Hyp:-3 ]

Generated subgoals:

None

About:

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

(31steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc