Logiweb aspects of lemma all disjoint in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma all disjoint 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 a unicode small l unicode small l unicode space unicode small d unicode small i unicode small s unicode small j unicode small o unicode small i unicode small n unicode small t unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma all disjoint as text unicode start of text unicode capital a unicode small l unicode small l unicode capital d unicode small i unicode small s unicode small j unicode small o unicode small i unicode small n unicode small t unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma all disjoint as system zf infer not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in object var var big set end var 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 object var var r end var 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 object var var big set end var imply object var var t end var zermelo in object var var big set end var 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 object var var r end var 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 object var var r end var 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 object var var big set end var imply object var var t end var zermelo in object var var big set end var imply object var var u end var zermelo in object var var big set end var 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 object var var r end var 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 object var var r end var 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 object var var r end var infer object var var x end var zermelo in the set of ph in power object var var big set end var end power such that not0 existential var var t end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 object var var r end var end set zermelo is placeholder-var var b end var end set infer object var var y end var zermelo in the set of ph in power object var var big set end var end power such that not0 existential var var t end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 object var var r end var end set zermelo is placeholder-var var b end var end set infer not0 object var var x end var zermelo is object var var y end var infer the set of ph in union zermelo pair zermelo pair object var var x end var comma object var var x end var end pair comma zermelo pair object var var y end var comma object var var y end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var x end var imply not0 placeholder-var var c end var zermelo in object var var y end var end set zermelo is zermelo empty set end define

The user defined "the proof aspect" aspect

define proof of lemma all disjoint as lambda var c dot lambda var x dot proof expand quote system zf infer not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in object var var big set end var 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 object var var r end var 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 object var var big set end var imply object var var t end var zermelo in object var var big set end var 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 object var var r end var 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 object var var r end var 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 object var var big set end var imply object var var t end var zermelo in object var var big set end var imply object var var u end var zermelo in object var var big set end var 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 object var var r end var 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 object var var r end var 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 object var var r end var infer object var var x end var zermelo in the set of ph in power object var var big set end var end power such that not0 existential var var t end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 object var var r end var end set zermelo is placeholder-var var b end var end set infer object var var y end var zermelo in the set of ph in power object var var big set end var end power such that not0 existential var var t end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 object var var r end var end set zermelo is placeholder-var var b end var end set infer not0 object var var x end var zermelo is object var var y end var infer lemma separation2formula modus ponens object var var x end var zermelo in the set of ph in power object var var big set end var end power such that not0 existential var var t end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 object var var r end var end set zermelo is placeholder-var var b end var end set conclude not0 object var var x end var zermelo in power object var var big set end var end power imply not0 not0 existential var var a end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set zermelo is object var var x end var cut prop lemma second conjunct modus ponens not0 object var var x end var zermelo in power object var var big set end var end power imply not0 not0 existential var var a end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set zermelo is object var var x end var conclude not0 existential var var a end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set zermelo is object var var x end var cut prop lemma first conjunct modus ponens not0 existential var var a end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set zermelo is object var var x end var conclude existential var var a end var zermelo in object var var big set end var cut prop lemma second conjunct modus ponens not0 existential var var a end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set zermelo is object var var x end var conclude the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set zermelo is object var var x end var cut lemma =symmetry modus ponens the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set zermelo is object var var x end var conclude object var var x end var zermelo is the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set cut lemma separation2formula modus ponens object var var y end var zermelo in the set of ph in power object var var big set end var end power such that not0 existential var var t end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 object var var r end var end set zermelo is placeholder-var var b end var end set conclude not0 object var var y end var zermelo in power object var var big set end var end power imply not0 not0 existential var var b end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set zermelo is object var var y end var cut prop lemma second conjunct modus ponens not0 object var var y end var zermelo in power object var var big set end var end power imply not0 not0 existential var var b end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set zermelo is object var var y end var conclude not0 existential var var b end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set zermelo is object var var y end var cut prop lemma first conjunct modus ponens not0 existential var var b end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set zermelo is object var var y end var conclude existential var var b end var zermelo in object var var big set end var cut prop lemma second conjunct modus ponens not0 existential var var b end var zermelo in object var var big set end var imply not0 the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set zermelo is object var var y end var conclude the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set zermelo is object var var y end var cut lemma =symmetry modus ponens the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set zermelo is object var var y end var conclude object var var y end var zermelo is the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set cut lemma transfer ~is modus ponens not0 object var var x end var zermelo is object var var y end var modus ponens object var var x end var zermelo is the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set modus ponens object var var y end var zermelo is the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set conclude not0 the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set zermelo is the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set cut lemma equivalence classes are disjoint modus ponens existential var var a end var zermelo in object var var big set end var modus ponens existential var var b end var zermelo in object var var big set end var modus ponens not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in object var var big set end var 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 object var var r end var 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 object var var big set end var imply object var var t end var zermelo in object var var big set end var 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 object var var r end var 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 object var var r end var 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 object var var big set end var imply object var var t end var zermelo in object var var big set end var imply object var var u end var zermelo in object var var big set end var 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 object var var r end var 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 object var var r end var 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 object var var r end var modus ponens not0 the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set zermelo is the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set conclude the set of ph in union zermelo pair zermelo pair the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set comma the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set end pair comma zermelo pair the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set comma the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set end pair end pair end union such that not0 placeholder-var var c end var zermelo in the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set imply not0 placeholder-var var c end var zermelo in the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set end set zermelo is zermelo empty set cut lemma same intersection modus ponens object var var x end var zermelo is the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set modus ponens object var var y end var zermelo is the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set conclude the set of ph in union zermelo pair zermelo pair object var var x end var comma object var var x end var end pair comma zermelo pair object var var y end var comma object var var y end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var x end var imply not0 placeholder-var var c end var zermelo in object var var y end var end set zermelo is the set of ph in union zermelo pair zermelo pair the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set comma the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set end pair comma zermelo pair the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set comma the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set end pair end pair end union such that not0 placeholder-var var c end var zermelo in the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set imply not0 placeholder-var var c end var zermelo in the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set end set cut lemma =transitivity modus ponens the set of ph in union zermelo pair zermelo pair object var var x end var comma object var var x end var end pair comma zermelo pair object var var y end var comma object var var y end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var x end var imply not0 placeholder-var var c end var zermelo in object var var y end var end set zermelo is the set of ph in union zermelo pair zermelo pair the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set comma the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set end pair comma zermelo pair the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set comma the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set end pair end pair end union such that not0 placeholder-var var c end var zermelo in the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set imply not0 placeholder-var var c end var zermelo in the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set end set modus ponens the set of ph in union zermelo pair zermelo pair the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set comma the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set end pair comma zermelo pair the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set comma the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set end pair end pair end union such that not0 placeholder-var var c end var zermelo in the set of ph in object var var big set end var 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 a end var end pair end pair zermelo in object var var r end var end set imply not0 placeholder-var var c end var zermelo in the set of ph in object var var big set end var 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 b end var end pair end pair zermelo in object var var r end var end set end set zermelo is zermelo empty set conclude the set of ph in union zermelo pair zermelo pair object var var x end var comma object var var x end var end pair comma zermelo pair object var var y end var comma object var var y end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var x end var imply not0 placeholder-var var c end var zermelo in object var var y end var end set zermelo is zermelo empty set end quote state proof state cache var c end expand end define