Logiweb aspects of lemma union(bs/r) is bs in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma union(bs/r) is bs as text unicode start of text unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode small u unicode small n unicode small i unicode small o unicode small n unicode left parenthesis unicode small b unicode small s unicode slash unicode small r unicode right parenthesis unicode space unicode small i unicode small s unicode space unicode small b unicode small s unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma union(bs/r) is bs as text unicode start of text unicode capital u unicode small n unicode small i unicode small o unicode small n unicode capital i unicode small d unicode small e unicode small n unicode small t unicode small i unicode small t unicode small y unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma union(bs/r) is bs as system zf infer all metavar var r end metavar indeed all metavar var big set end metavar indeed quote object var var s end var end quote avoid zero quote metavar var r end metavar end quote endorse quote object var var s end var end quote avoid zero quote metavar var big set end metavar end quote endorse quote object var var t end var end quote avoid zero quote metavar var r end metavar end quote endorse quote object var var t end var end quote avoid zero quote metavar var big set end metavar end quote endorse quote object var var u end var end quote avoid zero quote metavar var r end metavar end quote endorse quote object var var u end var end quote avoid zero quote metavar var big set end metavar end quote endorse not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar infer union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union zermelo is metavar var big set end metavar end define

The user defined "the proof aspect" aspect

define proof of lemma union(bs/r) is bs as lambda var c dot lambda var x dot proof expand quote system zf infer all metavar var r end metavar indeed all metavar var big set end metavar indeed quote object var var s end var end quote avoid zero quote metavar var r end metavar end quote endorse quote object var var s end var end quote avoid zero quote metavar var big set end metavar end quote endorse quote object var var t end var end quote avoid zero quote metavar var r end metavar end quote endorse quote object var var t end var end quote avoid zero quote metavar var big set end metavar end quote endorse quote object var var u end var end quote avoid zero quote metavar var r end metavar end quote endorse quote object var var u end var end quote avoid zero quote metavar var big set end metavar end quote endorse not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar infer lemma bs subset union(bs/r) modus probans quote object var var s end var end quote avoid zero quote metavar var r end metavar end quote modus probans quote object var var s end var end quote avoid zero quote metavar var big set end metavar end quote modus probans quote object var var t end var end quote avoid zero quote metavar var r end metavar end quote modus probans quote object var var t end var end quote avoid zero quote metavar var big set end metavar end quote modus probans quote object var var u end var end quote avoid zero quote metavar var r end metavar end quote modus probans quote object var var u end var end quote avoid zero quote metavar var big set end metavar end quote conclude not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply object var var s end var zermelo in metavar var big set end metavar imply object var var s end var zermelo in union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union cut 1rule mp modus ponens not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply object var var s end var zermelo in metavar var big set end metavar imply object var var s end var zermelo in union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union modus ponens not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar conclude object var var s end var zermelo in metavar var big set end metavar imply object var var s end var zermelo in union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union cut lemma union(bs/r) subset bs modus probans quote object var var s end var end quote avoid zero quote metavar var big set end metavar end quote modus probans quote object var var s end var end quote avoid zero quote metavar var r end metavar end quote modus probans quote object var var t end var end quote avoid zero quote metavar var r end metavar end quote modus probans quote object var var t end var end quote avoid zero quote metavar var big set end metavar end quote modus probans quote object var var u end var end quote avoid zero quote metavar var r end metavar end quote modus probans quote object var var u end var end quote avoid zero quote metavar var big set end metavar end quote conclude not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply object var var s end var zermelo in union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union imply object var var s end var zermelo in metavar var big set end metavar cut 1rule mp modus ponens not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply object var var s end var zermelo in union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union imply object var var s end var zermelo in metavar var big set end metavar modus ponens not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar conclude object var var s end var zermelo in union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union imply object var var s end var zermelo in metavar var big set end metavar cut lemma set equality suff condition modus ponens object var var s end var zermelo in union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union imply object var var s end var zermelo in metavar var big set end metavar modus ponens object var var s end var zermelo in metavar var big set end metavar imply object var var s end var zermelo in union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union conclude union the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set end union zermelo is metavar var big set end metavar end quote state proof state cache var c end expand end define