Nuprl - Proof: delete fenum value is fenum gen 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

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) }

Bij({u:

| P(u) &

u = m }; {v:

| Q(v) &

v = k };

Bij(Replace value k by f(m) in f)

By:

Analyze

Generated subgoals:

1   Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
  Inj(Replace value k by f(m) in f)
1 step

2   Surj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
  Surj(Replace value k by f(m) in f)
9 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	Inj({u:\| P(u) & u = m }; {v:\| Q(v) & v = k }; Inj(Replace value k by f(m) in f)	1 step
2	Surj({u:\| P(u) & u = m }; {v:\| Q(v) & v = k }; Surj(Replace value k by f(m) in f)	9 steps