Nuprl - Proof: delete fenum value is fenum gen 1 2 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: delete fenum value is fenum gen 1 2 1 1

1. P :

Prop
2. Q :

Prop
3. f : {u:

| P(u) }

{v:

| Q(v) }
4. Inj({u:

| P(u) }; {v:

| Q(v) }; f)
5. Surj({u:

| P(u) }; {v:

| Q(v) }; f)
6. m : {u:

| P(u) }
7. k : {v:

| Q(v) }
8. (Replace value k by f(m) in f)

{u:

| P(u) &

u = m }

{v:

| Q(v) &

v = k }
9. b : {v:

| Q(v) &

v = k }
10. a : {u:

| P(u) }
11. f(a) = b
12. c : {u:

| P(u) }
13. f(c) = k

a:{u:

| P(u) &

u = m }. (Replace value k by f(m) in f)(a) = b

By:	Decide: a = m

Generated subgoals:

1 14. a = m
a:{u:| P(u) & u = m }. (Replace value k by f(m) in f)(a) = b
3 steps

2 14. a = m
a:{u:| P(u) & u = m }. (Replace value k by f(m) in f)(a) = b
3 steps

About:

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

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

1	14. a = m a:{u:\| P(u) & u = m }. (Replace value k by f(m) in f)(a) = b	3 steps
2	14. a = m a:{u:\| P(u) & u = m }. (Replace value k by f(m) in f)(a) = b	3 steps