Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replaced |- ( [ x / y ] with |- ( [ y / x ] in set.mm, iset.mm and nf.mm #3571

Merged
merged 3 commits into from
Oct 13, 2023
Merged

Replaced |- ( [ x / y ] with |- ( [ y / x ] in set.mm, iset.mm and nf.mm #3571

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a713b25
replaced '|- ( [ x / y ]' with '|- ( [ y / x ]' in set.mm
GinoGiotto Oct 11, 2023
dad1c24
replaced '|- ( [ x / y ]' with '|- ( [ y / x ]' in iset.mm
GinoGiotto Oct 11, 2023
4f084ed
replaced '|- ( [ x / y ]' with '|- ( [ y / x ]' in nf.mm
GinoGiotto Oct 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
148 changes: 74 additions & 74 deletions iset.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15149,20 +15149,20 @@ Predicate calculus with distinct variables (cont.)
$}

${
$d y z $. $d x y $.
$d x z $. $d x y $.
$( Lemma for ~ equsb3 . (Contributed by NM, 4-Dec-2005.) (Proof shortened
by Andrew Salmon, 14-Jun-2011.) $)
equsb3lem $p |- ( [ x / y ] y = z <-> x = z ) $=
( cv wceq ax-17 equequ1 sbieh ) BDCDZEADIEZBAJBFBACGH $.
equsb3lem $p |- ( [ y / x ] x = z <-> y = z ) $=
( cv wceq ax-17 equequ1 sbieh ) ADCDZEBDIEZABJAFABCGH $.
$}

${
$d w y z $. $d w x $.
$d w x z $. $d w y $.
$( Substitution applied to an atomic wff. (Contributed by Raph Levien and
FL, 4-Dec-2005.) $)
equsb3 $p |- ( [ x / y ] y = z <-> x = z ) $=
( vw weq wsb equsb3lem sbbii ax-17 sbco2v 3bitr3i ) BCEZBDFZDAFDCEZDAFLBA
FACEMNDADBCGHLBADLDIJADCGK $.
equsb3 $p |- ( [ y / x ] x = z <-> y = z ) $=
( vw weq wsb equsb3lem sbbii ax-17 sbco2v 3bitr3i ) ACEZADFZDBFDCEZDBFLAB
FBCEMNDBADCGHLABDLDIJDBCGK $.
$}

${
Expand Down Expand Up @@ -15400,26 +15400,26 @@ Predicate calculus with distinct variables (cont.)
$}

${
$d w y z $. $d w x $.
$d w x z $. $d w y $.
$( Substitution applied to an atomic membership wff. (Contributed by NM,
7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $)
elsb3 $p |- ( [ x / y ] y e. z <-> x e. z ) $=
elsb3 $p |- ( [ y / x ] x e. z <-> y e. z ) $=
( vw wel wsb ax-17 elequ1 sbieh sbbii sbco2h bitr3i wb equsb1 sbimi ax-mp
weq sbbi mpbi sbh 3bitri ) BCEZBAFZDCEZDAFZACEZDAFZUFUCUDDBFZBAFUEUHUBBAU
DUBDBUBDGDBCHIJUDDABUDBGKLUDUFMZDAFZUEUGMDAQZDAFUJDANUKUIDADACHOPUDUFDARS
UFDAUFDGTUA $.
weq sbbi mpbi sbh 3bitri ) ACEZABFZDCEZDBFZBCEZDBFZUFUCUDDAFZABFUEUHUBABU
DUBDAUBDGDACHIJUDDBAUDAGKLUDUFMZDBFZUEUGMDBQZDBFUJDBNUKUIDBDBCHOPUDUFDBRS
UFDBUFDGTUA $.
$}

${
$d w y z $. $d w x $.
$d w x z $. $d w y $.
$( Substitution applied to an atomic membership wff. (Contributed by
Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon,
14-Jun-2011.) $)
elsb4 $p |- ( [ x / y ] z e. y <-> z e. x ) $=
elsb4 $p |- ( [ y / x ] z e. x <-> z e. y ) $=
( vw wel wsb ax-17 elequ2 sbieh sbbii sbco2h bitr3i wb equsb1 sbimi ax-mp
weq sbbi mpbi sbh 3bitri ) CBEZBAFZCDEZDAFZCAEZDAFZUFUCUDDBFZBAFUEUHUBBAU
DUBDBUBDGDBCHIJUDDABUDBGKLUDUFMZDAFZUEUGMDAQZDAFUJDANUKUIDADACHOPUDUFDARS
UFDAUFDGTUA $.
weq sbbi mpbi sbh 3bitri ) CAEZABFZCDEZDBFZCBEZDBFZUFUCUDDAFZABFUEUHUBABU
DUBDAUBDGDACHIJUDDBAUDAGKLUDUFMZDBFZUEUGMDBQZDBFUJDBNUKUIDBDBCHOPUDUFDBRS
UFDBUFDGTUA $.
$}

${
Expand Down Expand Up @@ -16097,7 +16097,7 @@ Predicate calculus with distinct variables (cont.)
( vz vw weq wb wal wex wsb weu nfv sb8 sbbi nfsb equsb3 nfxfr nfbi df-eu
sbequ cbval sblbis albii 3bitri exbii 3bitr4i ) ABEGZHZBIZEJABCKZCEGZHZCI
ZEJABLUKCLUJUNEUJUIBFKZFIUIBCKZCIUNUIBFUIFMNUOUPFCUOABFKZUHBFKZHCAUHBFOUQ
URCABFCDPURFEGZCFBEQUSCMRSRUPFMUIFCBUAUBUPUMCUHULABCCBEQUCUDUEUFABETUKCET
URCABFCDPURFEGZCBFEQUSCMRSRUPFMUIFCBUAUBUPUMCUHULABCBCEQUCUDUEUFABETUKCET
UG $.

$( Variable substitution for "at most one." (Contributed by Alexander van
Expand Down Expand Up @@ -16194,7 +16194,7 @@ Predicate calculus with distinct variables (cont.)
( vz vw weq wb wal wex wsb ax-17 sb8h sbbi hbsb equsb3 hbxfrbi hbbi df-eu
weu sbequ cbvalh sblbis albii 3bitri exbii 3bitr4i ) ABEGZHZBIZEJABCKZCEG
ZHZCIZEJABTUKCTUJUNEUJUIBFKZFIUIBCKZCIUNUIBFUIFLMUOUPFCUOABFKZUHBFKZHCAUH
BFNUQURCABFCDOURFEGZCFBEPUSCLQRQUPFLUIFCBUAUBUPUMCUHULABCCBEPUCUDUEUFABES
BFNUQURCABFCDOURFEGZCBFEPUSCLQRQUPFLUIFCBUAUBUPUMCUHULABCBCEPUCUDUEUFABES
UKCESUG $.
$}

Expand Down Expand Up @@ -17964,7 +17964,7 @@ of logic but rather presupposes the Axiom of Extensionality (see theorem
(Contributed by NM, 7-Nov-2006.) $)
cvjust $p |- x = { y | y e. x } $=
( vz cv wcel cab wceq wb dfcleq wsb df-clab elsb3 bitr2i mpgbir ) ADZBDOE
ZBFZGCDZOEZRQEZHCCOQITPBCJSPCBKCBALMN $.
ZBFZGCDZOEZRQEZHCCOQITPBCJSPCBKBCALMN $.
$}

${
Expand Down Expand Up @@ -18881,39 +18881,39 @@ This law is thought to have originated with Aristotle (_Metaphysics_,
( wcel wceq eleq2 biimpcd con3dimp ) ABDZBCEZACDZJIKBCAFGH $.

${
$d x y $. $d y A $.
$d x y $. $d x A $.
$( Lemma for ~ eqsb3 . (Contributed by Rodolfo Medina, 28-Apr-2010.)
(Proof shortened by Andrew Salmon, 14-Jun-2011.) $)
eqsb3lem $p |- ( [ x / y ] y = A <-> x = A ) $=
( cv wceq nfv eqeq1 sbie ) BDZCEADZCEZBAKBFIJCGH $.
eqsb3lem $p |- ( [ y / x ] x = A <-> y = A ) $=
( cv wceq nfv eqeq1 sbie ) ADZCEBDZCEZABKAFIJCGH $.
$}

${
$d y A $. $d w y $. $d w A $. $d x w $.
$d x A $. $d w x $. $d w A $. $d y w $.
$( Substitution applied to an atomic wff (class version of ~ equsb3 ).
(Contributed by Rodolfo Medina, 28-Apr-2010.) $)
eqsb3 $p |- ( [ x / y ] y = A <-> x = A ) $=
( vw cv wceq wsb eqsb3lem sbbii nfv sbco2 3bitr3i ) BECFZBDGZDAGDECFZDAGM
BAGAECFNODADBCHIMBADMDJKADCHL $.
eqsb3 $p |- ( [ y / x ] x = A <-> y = A ) $=
( vw cv wceq wsb eqsb3lem sbbii nfv sbco2 3bitr3i ) AECFZADGZDBGDECFZDBGM
ABGBECFNODBADCHIMABDMDJKDBCHL $.
$}

${
$d y A $. $d w y $. $d w A $. $d w x $.
$d x A $. $d w x $. $d w A $. $d w y $.
$( Substitution applied to an atomic wff (class version of ~ elsb3 ).
(Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by
Andrew Salmon, 14-Jun-2011.) $)
clelsb3 $p |- ( [ x / y ] y e. A <-> x e. A ) $=
( vw cv wcel wsb nfv sbco2 eleq1 sbie sbbii 3bitr3i ) DEZCFZDBGZBAGODAGBE
ZCFZBAGAEZCFZODABOBHIPRBAORDBRDHNQCJKLOTDATDHNSCJKM $.
clelsb3 $p |- ( [ y / x ] x e. A <-> y e. A ) $=
( vw cv wcel wsb nfv sbco2 eleq1 sbie sbbii 3bitr3i ) DEZCFZDAGZABGODBGAE
ZCFZABGBEZCFZODBAOAHIPRABORDARDHNQCJKLOTDBTDHNSCJKM $.
$}

${
$d y A $. $d w y $. $d w A $. $d w x $.
$d x A $. $d w x $. $d w A $. $d w y $.
$( Substitution applied to an atomic wff (class version of ~ elsb4 ).
(Contributed by Jim Kingdon, 22-Nov-2018.) $)
clelsb4 $p |- ( [ x / y ] A e. y <-> A e. x ) $=
( vw cv wcel wsb nfv sbco2 eleq2 sbie sbbii 3bitr3i ) CDEZFZDBGZBAGODAGCB
EZFZBAGCAEZFZODABOBHIPRBAORDBRDHNQCJKLOTDATDHNSCJKM $.
clelsb4 $p |- ( [ y / x ] A e. x <-> A e. y ) $=
( vw cv wcel wsb nfv sbco2 eleq2 sbie sbbii 3bitr3i ) CDEZFZDAGZABGODBGCA
EZFZABGCBEZFZODBAOAHIPRABORDARDHNQCJKLOTDBTDHNSCJKM $.
$}

${
Expand All @@ -18933,7 +18933,7 @@ This law is thought to have originated with Aristotle (_Metaphysics_,
5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) $)
hblem $p |- ( z e. A -> A. x z e. A ) $=
( cv wcel wsb wal hbsb clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAEJ
CBDKZOPAQLM $.
BCDKZOPAQLM $.
$}

${
Expand Down Expand Up @@ -19278,15 +19278,15 @@ effectively bound by a quantifier or something that expands to one (such
$}

${
$d w y $. $d w A $. $d w x $.
clelsb3f.1 $e |- F/_ y A $.
$d w x $. $d w A $. $d w y $.
clelsb3f.1 $e |- F/_ x A $.
$( Substitution applied to an atomic wff (class version of ~ elsb3 ).
(Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by
Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux,
13-Mar-2017.) $)
clelsb3f $p |- ( [ x / y ] y e. A <-> x e. A ) $=
( vw cv wcel wsb nfcri sbco2 nfv eleq1w sbie sbbii 3bitr3i ) EFCGZEBHZBAH
PEAHBFCGZBAHAFCGZPEABBECDIJQRBAPREBREKEBCLMNPSEASEKEACLMO $.
clelsb3f $p |- ( [ y / x ] x e. A <-> y e. A ) $=
( vw cv wcel wsb nfcri sbco2 nfv eleq1w sbie sbbii 3bitr3i ) EFCGZEAHZABH
PEBHAFCGZABHBFCGZPEBAAECDIJQRABPREAREKEACLMNPSEBSEKEBCLMO $.
$}

${
Expand Down Expand Up @@ -20707,7 +20707,7 @@ effectively bound by a quantifier or something that expands to one (such
nfraldya $p |- ( ph -> F/ x A. y e. A ps ) $=
( vz wral cv wcel wi wal df-ral wsb sbim clelsb3 nfv nfxfrd bitri 3bitr4i
imbi1i albii sb8 nfsbd nfraldxy ) BDEJDKELZBMZDNZACBDEOUJBDIPZIEJZACUIDIP
ZINIKELZUKMZINUJULUMUOIUMUHDIPZUKMUOUHBDIQUPUNUKIDERUCUAUDUIDIUIISUEUKIEO
ZINIKELZUKMZINUJULUMUOIUMUHDIPZUKMUOUHBDIQUPUNUKDIERUCUAUDUIDIUIISUEUKIEO
UBAUKCIEAISGABDICFHUFUGTT $.

$( Not-free for restricted existential quantification where ` y ` and ` A `
Expand All @@ -20716,7 +20716,7 @@ effectively bound by a quantifier or something that expands to one (such
nfrexdya $p |- ( ph -> F/ x E. y e. A ps ) $=
( vz wrex cv wcel wa wex df-rex wsb sban clelsb3 nfv nfxfrd bitri 3bitr4i
anbi1i exbii sb8e nfsbd nfrexdxy ) BDEJDKELZBMZDNZACBDEOUJBDIPZIEJZACUIDI
PZINIKELZUKMZINUJULUMUOIUMUHDIPZUKMUOUHBDIQUPUNUKIDERUCUAUDUIDIUIISUEUKIE
PZINIKELZUKMZINUJULUMUOIUMUHDIPZUKMUOUHBDIQUPUNUKDIERUCUAUDUIDIUIISUEUKIE
OUBAUKCIEAISGABDICFHUFUGTT $.
$}

Expand Down Expand Up @@ -22278,7 +22278,7 @@ deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.) $)
( vz cv wcel wa weu wreu wsb nfv sb8eu sban eubii df-reu anbi1i nfsb nfan
clelsb3 weq eleq1 sbequ sbie syl6bb anbi12d cbveu bitri 3bitri 3bitr4i )
CJEKZALZCMZDJZEKZBLZDMZACENBDENUQUPCIOZIMUOCIOZACIOZLZIMZVAUPCIUPIPQVBVEI
UOACIRSVFIJZEKZVDLZIMVAVEVIIVCVHVDICEUDUASVIUTIDVHVDDVHDPACIDFUBUCUTIPIDU
UOACIRSVFIJZEKZVDLZIMVAVEVIIVCVHVDCIEUDUASVIUTIDVHVDDVHDPACIDFUBUCUTIPIDU
EZVHUSVDBVGUREUFVJVDACDOBAIDCUGABCDGHUHUIUJUKULUMACETBDETUN $.

$( Change the bound variable of restricted "at most one" using implicit
Expand Down Expand Up @@ -22409,14 +22409,14 @@ deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.) $)
$}

${
$d x y z $. $d y z ph $. $d x z ps $.
$d x y z $. $d x z ph $. $d y z ps $.
sbralie.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
$( Implicit to explicit substitution that swaps variables in a quantified
expression. (Contributed by NM, 5-Sep-2004.) $)
sbralie $p |- ( [ x / y ] A. x e. y ph <-> A. y e. x ps ) $=
( vz cv wral wsb cbvralsv sbbii nfv raleq sbie bitri sbco2 ralbii ) ACDGZ
HZDCIZACFIZFCGZHZBDUBHZTUAFRHZDCIUCSUEDCACFRJKUEUCDCUCDLUAFRUBMNOUCUAFDIZ
DUBHUDUAFDUBJUFBDUBUFACDIBACDFAFLPABCDBCLENOQOO $.
sbralie $p |- ( [ y / x ] A. y e. x ph <-> A. x e. y ps ) $=
( vz cv wral wsb cbvralsv sbbii nfv raleq sbie bitri sbco2 equcoms ralbii
wb ) ADCGZHZCDIZADFIZFDGZHZBCUDHZUBUCFTHZCDIUEUAUGCDADFTJKUGUECDUECLUCFTU
DMNOUEUCFCIZCUDHUFUCFCUDJUHBCUDUHADCIBADCFAFLPABDCBDLABSCDEQNOROO $.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why does this proof become so much longer?

Copy link
Contributor Author

@GinoGiotto GinoGiotto Oct 12, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because I made the cosmetic choice of keeping x = y in the hypothesis instead of switching into y = x. Do you prefer to have y = x, but with the original proof length? (For me it's fine both ways).

Some useful data might be that currently x = y appears 486 times in iset.mm, while y = x appears only 19 times (and most of those 19 times are there to show commutation properties).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@GinoGiotto thank you for the explanation. We should not switch the antecedent in the hypothesis (x = y should be the preferred way), so we can keep the longer proof.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't really have an opinion about these renamings, as long as they are only renamings.
When we write x = y -> ( ph <-> ps ), this generally goes with DV(x,ps) and/or DV(y,ph), so if you swap x and y, do it consistently. (I haven't checked the present case.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When we write x = y -> ( ph <-> ps ), this generally goes with DV(x,ps) and/or DV(y,ph).

I didn't know that x is coupled with ps and y is coupled with ph. I'll try to fix this in a next PR.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I do not know what @benjub wants to say with his comment, and I don't see any need for a fix/change: DV(x,ps) means that x does not occur in ps, but of course y can (and usually should) occur in ps, analogously with ph. So we (usually) have ps(y) and ph(x). If the theorem is valid without DV conditions, they should not be added.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Of course, DV conditions should not be added if they are not necessary. What I mean is that when they are needed, it is usual to write that kind of hypotheses as x = y -> (ph(x) <-> ps(y)) (or sometimes x = y -> (ph(x,y) <-> ps(y)) or x = y -> (ph(x) <-> ps(x,y))), where I made explicit the variables that may occur instead of the variables that do not.

$}

${
Expand Down Expand Up @@ -24095,7 +24095,7 @@ deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.) $)
( vy cv wceq wal eqeq1 eqeq2 bibi1d albidv alrimiv wsb stdpc4 sbbi bibi2i
wb eqsb3 sylbi equsb1 bi1 mpi syl impbii vtoclbg ) EFZCGZAFZUGGZUICGZRZAH
ZBCGUIBGZUKRZAHEBDUGBCIUGBGZULUOAUPUJUNUKUGBUIJKLUHUMUHULAUGCUIJMUMULAENZ
UHULAEOUQUJAENZUKAENZRZUHUJUKAEPUTURUHRZUHUSUHUREACSQVAURUHAEUAURUHUBUCTT
UHULAEOUQUJAENZUKAENZRZUHUJUKAEPUTURUHRZUHUSUHURAECSQVAURUHAEUAURUHUBUCTT
UDUEUF $.
$}

Expand Down Expand Up @@ -24739,7 +24739,7 @@ deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.) $)
wmo weq df-rmo sban clelsb3f anbi2i an4 ancom imbi1i nfcri r19.21 3bitr2i
nfan mo3 3bitr4i ) ABDUABHDIZAJZBUBZAABCKZJZBCUCZLZCDMZBDMZABDUDURURBCKZJ
ZVBLZCNZBNUQVDLZBNUSVEVIVJBVICHDIZUQVCLZLZCNVLCDMVJVHVMCVHVKUQJZVAJZVBLVN
VCLVMVGVOVBVGURVKUTJZJUQVKJZVAJVOVFVPURVFUQBCKZUTJVPUQABCUEVRVKUTCBDEUFOP
VCLVMVGVOVBVGURVKUTJZJUQVKJZVAJVOVFVPURVFUQBCKZUTJVPUQABCUEVRVKUTBCDEUFOP
UGUQAVKUTUHVQVNVAUQVKUIOQUJVNVAVBRVKUQVCRQSVLCDTUQVCCDCBDFUKZULUMSURBCUQA
CVSGUNUOVDBDTUPP $.
$}
Expand Down Expand Up @@ -25485,7 +25485,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
(Contributed by Andrew Salmon, 29-Jun-2011.) $)
eqsbc3 $p |- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) ) $=
( vy cv wceq wsbc dfsbcq eqeq1 wsb sbsbc eqsb3 bitr3i vtoclbg ) AFCGZAEFZ
HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELEACMNO $.
HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELAECMNO $.
$}

${
Expand Down Expand Up @@ -25671,7 +25671,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
17-Aug-2018.) $)
sbcel1v $p |- ( [. A / x ]. x e. B <-> A e. B ) $=
( vy wcel wsbc cvv sbcex elex wsb dfsbcq2 eleq1 clelsb3 vtoclbg pm5.21nii
cv ) APCEZABFZBGEBCEZQABHBCIQADJDPZCERSDBGQADBKTBCLDACMNO $.
cv ) APCEZABFZBGEBCEZQABHBCIQADJDPZCERSDBGQADBKTBCLADCMNO $.
$}

${
Expand Down Expand Up @@ -25961,7 +25961,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
wal weq df-rmo sban clelsb3 anbi2i an4 ancom r19.21v 3bitr2i nfv nfan mo3
imbi1i 3bitr4i ) ABDFBGDHZAIZBJZAABCKZIZBCUAZLZCDMZBDMZABDUBUPUPBCKZIZUTL
ZCTZBTUOVBLZBTUQVCVGVHBVGCGDHZUOVALZLZCTVJCDMVHVFVKCVFVIUOIZUSIZUTLVLVALV
KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURCBDUDNOUEUOA
KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURBCDUDNOUEUOA
VIURUFVOVLUSUOVIUGNPUMVLUSUTQVIUOVAQPRVJCDSUOVACDUHUIRUPBCUOACUOCUJEUKULV
BBDSUNO $.
$}
Expand Down Expand Up @@ -39131,7 +39131,7 @@ this axiom (that is, Non-wellfounded Set Theory but in the absence of
S = _V ) $=
( cv wcel wi wal cvv wceq wsb wral clelsb3 ralbii df-ral imbi1i ax-setind
bitri albii sylbir eqv sylibr ) BDZADZEUBCEZFBGZUCCEZFZAGZUFAGZCHIUHUFABJ
ZBUCKZUFFZAGUIULUGAUKUEUFUKUDBUCKUEUJUDBUCBACLMUDBUCNQORUFBAPSACTUA $.
ZBUCKZUFFZAGUIULUGAUKUEUFUKUDBUCKUEUJUDBUCABCLMUDBUCNQORUFBAPSACTUA $.
$}

${
Expand Down Expand Up @@ -39178,7 +39178,7 @@ this axiom (that is, Non-wellfounded Set Theory but in the absence of
AZVMARZMVNWFWGVLWFAENVIWDWGVLVIWDWGUBZVIVLVIWDWGUCWHAVMDZVLLZVIVLLZWDVIWJ
WGWDWIVLWCWJCAVMVTARWAWIWBVLVTAVMOVTAVKOUDPUEUFWGVIWJWKUGWDWGWIVIVLVMAAUH
UJUIUKQULUMVNVMVJDZWGVNVMEDWLMBUNVMEVJUOUPBAVAUQSVBURVRWEBVQWDVNVQWAVPLZC
IWDVPCVMUSWMWCCVPWBWACBVKUTVCTVDVETSVNCBVFVGVNVLBAAVMAVKOPQVIAENVH $.
IWDVPCVMUSWMWCCVPWBWABCVKUTVCTVDVETSVNCBVFVGVNVLBAAVMAVKOPQVIAENVH $.
$}

$( Epsilon irreflexivity of ordinals: no ordinal class is a member of itself.
Expand Down Expand Up @@ -39291,7 +39291,7 @@ class of all ordinal numbers to be a set (so instead it is a proper
WGAWEEZABGVCWGXPXQLZWGXPXRFXPXRJAGWENXPXROUGUHUISRZRWDWSXCWGWDWSXCUKZWBWG
WBWCWSXCVDXTAWHEZWGJZWBWGJZWSWDYBXCWSYAWGWRYBDAWHWOAKWPYAWQWGWOAWHPWOAWFP
ULQUNUOXCWDYBYCUPWSXCYAWBWGWHBAUQURUSUTTVAVBXBXCVOVEWIWHWEEZXDWIWHGEYDLCV
FZWHGWENVGWHABYEVHVIVJVKVLWMWTCWLWSWIWLWPWKJZDIWSWKDWHVMYFWRDWKWQWPDCWFVN
FZWHGWENVGWHABYEVHVIVJVKVLWMWTCWLWSWIWLWPWKJZDIWSWKDWHVMYFWRDWKWQWPCDWFVN
VPVQVRVSVQVJWIDCVTSWBWJWGJWCWIWGCABWHAWFPQRTXSWA $.
$}

Expand Down Expand Up @@ -39541,7 +39541,7 @@ class of all ordinal numbers to be a set (so instead it is a proper
wss ax-setind dfss2 sylibr sylbir df-frfor mpbir mpgbir ) AEFAEBGZHZBAEBI
URCGZDGZEUAZCBJZKZCALZDBJZKZDALZAUQUIZKVGUTAMZVEKZDCNZCUTLZVJKZDQZVHVNVLV
EKZDALZVGVNVIVOKZDQVPVMVQDVLVIVEUBUCVODAUDOVOVFDAVLVDVEVLCDJZVBKZCALZVDVL
USAMZVBKZCUTLVTVKWBCUTVKVIDCNZVEDCNZKWBVIVEDCUEWCWAWDVBCDAPCDUQPUFRSVBCUT
USAMZVBKZCUTLVTVKWBCUTVKVIDCNZVEDCNZKWBVIVEDCUEWCWAWDVBDCAPDCUQPUFRSVBCUT
AUGRVCVSCAVAVRVBCDUHTSOTSRVNVJDQVHVJCDUJDAUQUKULUMDCAEUQUNUOUP $.
$}

Expand Down Expand Up @@ -39678,7 +39678,7 @@ can deduce (outside the formal system, since we cannot quantify over
VJWPWCCVIBRUCWCWGCUDUEOMNWJWEAWBWIWDWAWHCVQVRJZVSHVQWCJZVSHZWAWHWRWQVSWRV
QVRVQWCUFWRVRHZAWTAKZCDUGXACKUHCADUIUJPPVAQVQVRVSSWSVQWCVSHHWHVQWCVSSVQWC
VSUKNULUMQUMUNUOWFWDAKZVNWFWDACTZCVIIZWDHZAKXBXEWEAXDWBWDXDVTCVIIWBXCVTCV
IXCWCACTZVKACTZHVTWCVKACVBXFVRXGVSCADUPCABUPUQNURVTCVILNOMWDCAUSUTADBRVCV
IXCWCACTZVKACTZHVTWCVKACVBXFVRXGVSACDUPACBUPUQNURVTCVILNOMWDCAUSUTADBRVCV
DVOVHVNJBDVEVFVG $.
$}

Expand Down Expand Up @@ -39860,7 +39860,7 @@ The natural numbers (i.e. finite ordinals)
peano1 $p |- (/) e. _om $=
( vy vx vz c0 cv wcel csuc wral wa cab com wi 0ex elint wsb df-clab simpl
cint sbimi clelsb4 sylib sylbi mpgbir dfom3 eleqtrri ) DDAEZFZBEGUFFBUFHZ
IZAJZRZKDUKFCEZUJFZDULFZLCCDUJMNUMUIACOZUNUICAPUOUGACOUNUIUGACUGUHQSCADTU
IZAJZRZKDUKFCEZUJFZDULFZLCCDUJMNUMUIACOZUNUICAPUOUGACOUNUIUGACUGUHQSACDTU
AUBUCABUDUE $.
$( $j usage 'peano1' avoids 'ax-iinf' 'ax-setind'; $)
$}
Expand All @@ -39871,17 +39871,17 @@ The natural numbers (i.e. finite ordinals)
five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring]
p. 42. (Contributed by NM, 3-Sep-2003.) $)
peano2 $p |- ( A e. _om -> suc A e. _om ) $=
( vy vx vz cvv wcel com csuc cv wa wi wb imbi12d adantl wsb wal sylib nfv
wral nfan elex c0 cint simpl wceq eleq1 suceq eleq1d df-clab simpr df-ral
cab sbimi sbim elsb4 clelsb4 imbi12i bitri sbalv sylbi 19.21bi nfra1 nfvd
nfsab nfcvd vtocldf ralrimiva ralim elintg sucexg syl syl5ibr mpd 3imtr4g
dfom3 eleq2i mpcom ) AEFZAGFZAHZGFZAGUAVRAUBBIZFZCIZHZWBFZCWBSZJZBULZUCZF
ZVTWJFZVSWAVRADIZFZVTWMFZKZDWISZWKWLKZVRWPDWIVRWMWIFZJZWDWMFZWEWMFZKZWPCA
EVRWSUDWDAUEZXCWPLWTXDXAWNXBWOWDAWMUFXDWEVTWMWDAUGUHMNWSXCVRWSXCCWSWHBDOZ
XCCPZWHDBUIXEWDWBFZWFKZCPZBDOXFWHXIBDWHWGXIWCWGUJWFCWBUKQUMXHXCBDCXHBDOXG
BDOZWFBDOZKXCXGWFBDUNXJXAXKXBDBCUODBWEUPUQURUSQUTVANVRWSCVRCRWHCBDWCWGCWC
CRWFCWBVBTVDTWTCAVEWTWPCVCVFVGWQWRVRWNDWISZWODWISZKWNWODWIVHVRWKXLWLXMDAW
IEVIVRVTEFWLXMLAEVJDVTWIEVIVKMVLVMGWJABCVOZVPGWJVTXNVPVNVQ $.
( vy vx vz cvv wcel com csuc cv wral wa wi imbi12d adantl wsb wal clelsb4
wb sylib nfv elex c0 cab cint simpl wceq eleq1 suceq eleq1d df-clab simpr
df-ral sbimi sbim imbi12i bitri sbalv sylbi 19.21bi nfra1 nfan nfsab nfvd
nfcvd vtocldf ralrimiva ralim elintg sucexg syl syl5ibr mpd dfom3 3imtr4g
eleq2i mpcom ) AEFZAGFZAHZGFZAGUAVQAUBBIZFZCIZHZWAFZCWAJZKZBUCZUDZFZVSWIF
ZVRVTVQADIZFZVSWLFZLZDWHJZWJWKLZVQWODWHVQWLWHFZKZWCWLFZWDWLFZLZWOCAEVQWRU
EWCAUFZXBWORWSXCWTWMXAWNWCAWLUGXCWDVSWLWCAUHUIMNWRXBVQWRXBCWRWGBDOZXBCPZW
GDBUJXDWCWAFZWELZCPZBDOXEWGXHBDWGWFXHWBWFUKWECWAULSUMXGXBBDCXGBDOXFBDOZWE
BDOZLXBXFWEBDUNXIWTXJXABDWCQBDWDQUOUPUQSURUSNVQWRCVQCTWGCBDWBWFCWBCTWECWA
UTVAVBVAWSCAVDWSWOCVCVEVFWPWQVQWMDWHJZWNDWHJZLWMWNDWHVGVQWJXKWKXLDAWHEVHV
QVSEFWKXLRAEVIDVSWHEVHVJMVKVLGWIABCVMZVOGWIVSXMVOVNVP $.
$( $j usage 'peano2' avoids 'ax-iinf' 'ax-setind'; $)
$}

Expand Down Expand Up @@ -45103,8 +45103,8 @@ Definite description binder (inverted iota)
( vz vw weq wal cab cuni wsb cio nfv sb8 sbbi nfsb equsb3 nfxfr dfiota2
wb nfbi sbequ cbval sblbis albii 3bitri abbii unieqi 3eqtr4i ) ABEGZTZBHZ
EIZJABCKZCEGZTZCHZEIZJABLUNCLUMURULUQEULUKBFKZFHUKBCKZCHUQUKBFUKFMNUSUTFC
USABFKZUJBFKZTCAUJBFOVAVBCABFCDPVBFEGZCFBEQVCCMRUARUTFMUKFCBUBUCUTUPCUJUO
ABCCBEQUDUEUFUGUHABESUNCESUI $.
USABFKZUJBFKZTCAUJBFOVAVBCABFCDPVBFEGZCBFEQVCCMRUARUTFMUKFCBUBUCUTUPCUJUO
ABCBCEQUDUEUFUGUHABESUNCESUI $.
$}

${
Expand Down Expand Up @@ -143148,7 +143148,7 @@ with definitions ( ` B ` is the definiendum that one wants to prove
bdcab ax-mp ) BCHZAIZBJZABCKZUAVGBLZUBZVHFKVJUCZGFHZMZFNZGLVKVOGABFOZVMMZ
FVIUDZVOVQFCVPVMABFDUEGFUFUGUHVRVGBFOZVMMZFNZVOVRFCHZVPIZVMMZFNZWAVRWBVQM
ZFNWEVQFVIUIWFWDFWDWFWBVPVMUJPQRWDVTFWCVSVMVSWCVSVFBFOZVPIWCVFABFULWGWBVP
FBVIUKUMRPSQRVTVNFVSVLVMVLVSVGFBUNPSQRUOVDGFVJUPTVGBUQZVHVKURABVIUSWHEABV
BFVIUKUMRPSQRVTVNFVSVLVMVLVSVGFBUNPSQRUOVDGFVJUPTVGBUQZVHVKURABVIUSWHEABV
IUTVAVGBVBVETABVIVCT $.
$}

Expand Down
Loading