Logiweb aspects of theorem eq-system is partition in pyk

Up Help

The predefined "pyk" aspect

define pyk of theorem eq-system is partition as text unicode start of text unicode small t unicode small h unicode small e unicode small o unicode small r unicode small e unicode small m unicode space unicode small e unicode small q unicode hyphen unicode small s unicode small y unicode small s unicode small t unicode small e unicode small m unicode space unicode small i unicode small s unicode space unicode small p unicode small a unicode small r unicode small t unicode small i unicode small t unicode small i unicode small o unicode small n unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of theorem eq-system is partition as text unicode start of text unicode capital e unicode small q unicode capital s unicode small y unicode small s unicode capital i unicode small s unicode capital p unicode small a unicode small r unicode small t unicode small i unicode small t unicode small i unicode small o unicode small n unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of theorem eq-system is partition 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 not0 not0 for all objects object var var s end var indeed object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set 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 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set imply not0 union 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 end union zermelo is object var var big set end var end define

The user defined "the proof aspect" aspect

define proof of theorem eq-system is partition 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 lemma eq-system not empty 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 conclude 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 imply not0 object var var x end var zermelo is zermelo empty set cut 1rule deduction 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 imply not0 object var var x end var zermelo is zermelo empty set conclude object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set cut 1rule gen modus ponens object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set conclude for all objects object var var s end var indeed object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set cut lemma all disjoint-imply conclude 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 imply object var var s 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set 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 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 imply object var var s 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set 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 conclude object var var s 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set cut 1rule gen modus ponens object var var s 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set conclude for all objects object var var t end var indeed object var var s 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set cut 1rule gen modus ponens for all objects object var var t end var indeed object var var s 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set conclude 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 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set cut lemma union(bs/r) is bs 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 conclude union 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 end union zermelo is object var var big set end var cut prop lemma join conjuncts modus ponens for all objects object var var s end var indeed object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set modus ponens 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 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set conclude not0 for all objects object var var s end var indeed object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set 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 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set cut prop lemma join conjuncts modus ponens not0 for all objects object var var s end var indeed object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set 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 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set modus ponens union 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 end union zermelo is object var var big set end var conclude not0 not0 for all objects object var var s end var indeed object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set 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 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set imply not0 union 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 end union zermelo is object var var big set end var cut 1rule repetition modus ponens not0 not0 for all objects object var var s end var indeed object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set 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 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set imply not0 union 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 end union zermelo is object var var big set end var conclude not0 not0 for all objects object var var s end var indeed object var var s 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 imply not0 object var var s end var zermelo is zermelo empty set 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 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 imply object var var t 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 imply not0 object var var s end var zermelo is object var var t end var imply the set of ph in union 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 t end var comma object var var t end var end pair end pair end union such that not0 placeholder-var var c end var zermelo in object var var s end var imply not0 placeholder-var var c end var zermelo in object var var t end var end set zermelo is zermelo empty set imply not0 union 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 end union zermelo is object var var big set end var end quote state proof state cache var c end expand end define