(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. 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 }
  a:{u:P(u) & u = m }. (Replace value k by f(m) in f)(a) = b


By: Witness5: b THEN Analyze-1 THEN Witness5: k THEN New:c Analyze-1


Generated subgoal:

1 10. a : {u:P(u) }
11. f(a) = b  {v:Q(v) }
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

7 steps

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

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