Logiweb aspects of lemma same intersection in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma same intersection 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 s unicode small a unicode small m unicode small e unicode space unicode small i unicode small n unicode small t unicode small e unicode small r unicode small s unicode small e unicode small c 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 lemma same intersection as text unicode start of text unicode capital s unicode small a unicode small m unicode small e unicode capital i unicode small n unicode small t unicode small e unicode small r unicode small s unicode small e unicode small c 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 lemma same intersection as system zf infer 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 infer 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 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 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 end define

The user defined "the proof aspect" aspect

define proof of lemma same intersection as lambda var c dot lambda var x dot proof expand quote system zf infer 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 infer 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 infer lemma same binary union 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 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 zermelo is 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 cut lemma intersection subset 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 imply 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 imply 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 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 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 cut prop lemma mp2 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 imply 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 imply 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 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 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 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 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 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 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 cut lemma =symmetry 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 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 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 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 intersection subset 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 imply 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 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 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 imply 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 cut prop lemma mp2 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 imply 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 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 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 imply 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 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 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 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 imply 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 cut prop lemma join conjuncts modus ponens 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 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 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 modus ponens 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 imply 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 conclude not0 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 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 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 imply not0 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 imply 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 cut lemma same separation modus ponens 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 zermelo is 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 modus ponens not0 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 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 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 imply not0 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 imply 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 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 1rule repetition 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 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 end quote state proof state cache var c end expand end define