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

save ax-riotaBAD in glbconN #4528

Merged
merged 3 commits into from
Jan 13, 2025
+48 −9
Merged

save ax-riotaBAD in glbconN #4528

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
046a140
save ax-riotaBAD in glbconN
icecream17 Jan 3, 2025
0eaddae
shorten amosym1, subsym1
icecream17 Jan 4, 2025
d58f851
remove discouraged tags
icecream17 Jan 10, 2025
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
Prev Previous commit
remove discouraged tags
@icecream17
icecream17 committed Jan 10, 2025
commit d58f851ca5403693c6c55a6b1a0a56a590ae115b
32 changes: 0 additions & 32 deletions discouraged
View file
Original file line number Diff line number Diff line change
@@ -1450,7 +1450,6 @@
"ax-pre-lttrn" is used by "axlttrn".
"ax-pre-mulgt0" is used by "axmulgt0".
"ax-pre-sup" is used by "axsup".
"ax-riotaBAD" is used by "riotaclbgBAD".
"ax10fromc7" is used by "axc5c711".
"ax10fromc7" is used by "equidq".
"ax10fromc7" is used by "hba1-o".
@@ -12596,31 +12595,8 @@
"ringcvalALTV" is used by "ringcbasALTV".
"ringcvalALTV" is used by "ringccofvalALTV".
"ringcvalALTV" is used by "ringchomfvalALTV".
"riotaclbBAD" is used by "cdlemk36".
"riotaclbBAD" is used by "glbconNOLD".
"riotaclbgBAD" is used by "riotaclbBAD".
"riotaclbgBAD" is used by "riotasvd".
"riotaocN" is used by "glbconN".
"riotaocN" is used by "glbconNOLD".
"riotasv" is used by "cdleme26e".
"riotasv" is used by "cdleme26eALTN".
"riotasv" is used by "cdleme26f".
"riotasv" is used by "cdleme26f2".
"riotasv" is used by "cdleme26f2ALTN".
"riotasv" is used by "cdleme26fALTN".
"riotasv2d" is used by "cdleme42b".
"riotasv2d" is used by "riotasv2s".
"riotasv3d" is used by "cdleme40m".
"riotasv3d" is used by "cdleme40n".
"riotasv3d" is used by "cdleme41sn3a".
"riotasv3d" is used by "cdleme43fsv1snlem".
"riotasv3d" is used by "cdlemefs32sn1aw".
"riotasv3d" is used by "cdlemkid".
"riotasv3d" is used by "dihvalcqpre".
"riotasvd" is used by "cdleme32a".
"riotasvd" is used by "riotasv".
"riotasvd" is used by "riotasv2d".
"riotasvd" is used by "riotasv3d".
"rnbra" is used by "bra11".
"rnbra" is used by "cnvbraval".
"rnelshi" is used by "hmopidmchi".
@@ -14670,7 +14646,6 @@ New usage of "ax-pre-lttri" is discouraged (1 uses).
New usage of "ax-pre-lttrn" is discouraged (1 uses).
New usage of "ax-pre-mulgt0" is discouraged (1 uses).
New usage of "ax-pre-sup" is discouraged (1 uses).
New usage of "ax-riotaBAD" is discouraged (1 uses).
New usage of "ax1" is discouraged (0 uses).
New usage of "ax10fromc7" is discouraged (3 uses).
New usage of "ax10w" is discouraged (0 uses).
@@ -18881,14 +18856,7 @@ New usage of "ringcinvALTV" is discouraged (1 uses).
New usage of "ringcisoALTV" is discouraged (0 uses).
New usage of "ringcsectALTV" is discouraged (1 uses).
New usage of "ringcvalALTV" is discouraged (3 uses).
New usage of "riotaclbBAD" is discouraged (2 uses).
New usage of "riotaclbgBAD" is discouraged (2 uses).
New usage of "riotaocN" is discouraged (2 uses).
New usage of "riotasv" is discouraged (6 uses).
New usage of "riotasv2d" is discouraged (2 uses).
New usage of "riotasv2s" is discouraged (0 uses).
New usage of "riotasv3d" is discouraged (7 uses).
New usage of "riotasvd" is discouraged (4 uses).
New usage of "rlimaddOLD" is discouraged (0 uses).
New usage of "rlimmulOLD" is discouraged (0 uses).
New usage of "rmoanimALT" is discouraged (0 uses).
19 changes: 8 additions & 11 deletions set.mm
View file
Original file line number Diff line number Diff line change
@@ -587191,14 +587191,14 @@ This axiom is _logically_ redundant in the (logically complete)
Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD
~ df-riota , CONFLICTS WITH (THE NEW) ~ df-riota AND MAKES THE SYSTEM IN
set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES
ARE ELIMINATED. (New usage is discouraged.) $)
ARE ELIMINATED. $)
ax-riotaBAD $a |- ( iota_ x e. A ph ) = if ( E! x e. A ph ,
( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) ) $.

${
$d x A $.
$( Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised
by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.) $)
by Mario Carneiro, 24-Dec-2016.) $)
riotaclbgBAD $p |- ( A e. V
-> ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A ) ) $=
( wcel wreu crio riotacl wn cund cfv undefnel2 cv cio cab cif ax-riotaBAD
@@ -587207,8 +587207,7 @@ This axiom is _logically_ redundant in the (logically complete)
ZUOBOZJKZPURUJUMUIUPURSABCQCUQJBCTUAUBUCUDUEUFUG $.

riotaclb.1 $e |- A e. _V $.
$( Closure of restricted iota. (Contributed by NM, 15-Sep-2011.)
(New usage is discouraged.) $)
$( Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) $)
riotaclbBAD $p |- ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A ) $=
( cvv wcel wreu crio wb riotaclbgBAD ax-mp ) CEFABCGABCHCFIDABCEJK $.
$}
@@ -587220,8 +587219,7 @@ This axiom is _logically_ redundant in the (logically complete)
-> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) ) $.
riotasvd.2 $e |- ( ph -> D e. A ) $.
$( Deduction version of ~ riotasv . (Contributed by NM, 4-Mar-2013.)
(Revised by Mario Carneiro, 15-Oct-2016.)
(New usage is discouraged.) $)
(Revised by Mario Carneiro, 15-Oct-2016.) $)
riotasvd $p |- ( ( ph /\ A e. V ) -> ( ( y e. B /\ ps ) -> D = C ) ) $=
( vz wcel wa cv wceq wi wral adantr syl crio wsbc wreu eqeltrrd wb adantl
riotaclbgBAD mpbird riotasbc eqeq1 imbi2d ralbidv nfra1 nfcv nfeq2 ralbid
@@ -587246,7 +587244,7 @@ This axiom is _logically_ redundant in the (logically complete)
riotasv2d.9 $e |- ( ph -> ch ) $.
$( Value of description binder ` D ` for a single-valued class expression
` C ( y ) ` (as in e.g. ~ reusv2 ). Special case of ~ riota2f .
(Contributed by NM, 2-Mar-2013.) (New usage is discouraged.) $)
(Contributed by NM, 2-Mar-2013.) $)
riotasv2d $p |- ( ( ph /\ A e. V ) -> D = F ) $=
( wcel cvv wceq elex wa adantr cv wi eleq1 adantl anbi12d imbi12d adantlr
wb eqeq2d riotasvd nfv nfan nfcvd nfvd nfand wnfc wral crio nfra1 nfriota
@@ -587263,8 +587261,7 @@ This axiom is _logically_ redundant in the (logically complete)
$( The value of description binder ` D ` for a single-valued class
expression ` C ( y ) ` (as in e.g. ~ reusv2 ) in the form of a
substitution instance. Special case of ~ riota2f . (Contributed by NM,
3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
(New usage is discouraged.) $)
3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) $)
riotasv2s $p |- ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) )
-> D = [_ E / y ]_ C ) $=
( wcel wsbc wa w3a csb wceq cv nfan a1i adantl 3simpc simp1 wi wral nfra1
@@ -587282,7 +587279,7 @@ This axiom is _logically_ redundant in the (logically complete)
$( Value of description binder ` D ` for a single-valued class expression
` C ( y ) ` (as in e.g. ~ reusv2 ). Special case of ~ riota2f .
(Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro,
6-Dec-2016.) (New usage is discouraged.) $)
6-Dec-2016.) $)
riotasv $p |- ( ( D e. A /\ y e. B /\ ph ) -> D = C ) $=
( wcel cv wceq cvv wa wi wral crio a1i id riotasvd mpan2 3impib ) GDJZCKE
JZAGFLZUCDMJUDANUEOHUCABCDEFGMGABKFLOCEPBDQLUCIRUCSTUAUB $.
@@ -587302,7 +587299,7 @@ This axiom is _logically_ redundant in the (logically complete)
expression ` C ( y ) ` (see e.g. ~ reusv2 ) also holds for its
description binder ` D ` (in the form of property ` th ` ).
(Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro,
15-Oct-2016.) (New usage is discouraged.) $)
15-Oct-2016.) $)
riotasv3d $p |- ( ( ph /\ A e. V ) -> th ) $=
( wcel wa cvv elex wrex adantr wi wral nfv imp adantrl wceq riotasvd impr
cv wb eqcomd syldan mpbid exp45 ralrimd wnf r19.23t syl sylibd mpd sylan2