By: |
|
1 |
2. Q : Prop 3. f : {u:| P(u) }{v:| Q(v) } 4. Inj({u:| P(u) }; {v:| Q(v) }; f) 5. m : {u:| P(u) } 6. k : {v:| Q(v) } 7. (Replace value k by f(m) in f) {u:| P(u) & u = m }{v:| Q(v) & v = k } 7. & Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k }; 7. & Inj(Replace value k by f(m) in f) Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k }; Inj(Replace value k by f(m) in f) | 1 step |
About: