Skip to content

Commit 42f12cb

Browse files
wlammenwlammen
authored
bj-denotes to main (#4983)
* move bj-denotes to main, minimalistic * typo * more typos * yet another typo * restore messed up ralima * discouraged
1 parent 21f3b09 commit 42f12cb

File tree

3 files changed

+89
-44
lines changed

3 files changed

+89
-44
lines changed

‎changes-set.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,8 @@ make a github issue.)
9292

9393
DONE:
9494
Date Old New Notes
95+
17-Aug-25 bj-denotes iseqsetv-clel Moved from BJ's mathbox to main
96+
17-Aug-25 bj-issettru issettru Moved from BJ's mathbox to main set.mm
9597
9-Aug-25 frobrhm [same] Moved from TA's mathbox to main set.mm
9698
28-Jul-25 spcimgft spcimgfi1 Is a kind of inference form
9799
27-Jul-25 fnimatp fnimatpd Moved from TA's mathbox to main set.mm

‎discouraged‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15022,7 +15022,6 @@ New usage of "bj-currypeirce" is discouraged (0 uses).
1502215022
New usage of "bj-denot" is discouraged (0 uses).
1502315023
New usage of "bj-dfid2ALT" is discouraged (0 uses).
1502415024
New usage of "bj-elabd2ALT" is discouraged (0 uses).
15025-
New usage of "bj-elissetALT" is discouraged (0 uses).
1502615025
New usage of "bj-elpwgALT" is discouraged (0 uses).
1502715026
New usage of "bj-equsalhv" is discouraged (0 uses).
1502815027
New usage of "bj-eximALT" is discouraged (1 uses).
@@ -20165,7 +20164,7 @@ Proof modification of "bj-consensusALT" is discouraged (30 steps).
2016520164
Proof modification of "bj-csbprc" is discouraged (47 steps).
2016620165
Proof modification of "bj-currypara" is discouraged (16 steps).
2016720166
Proof modification of "bj-currypeirce" is discouraged (16 steps).
20168-
Proof modification of "bj-denotes" is discouraged (26 steps).
20167+
Proof modification of "bj-denotesALTV" is discouraged (26 steps).
2016920168
Proof modification of "bj-denoteslem" is discouraged (33 steps).
2017020169
Proof modification of "bj-df-ifc" is discouraged (60 steps).
2017120170
Proof modification of "bj-dfid2ALT" is discouraged (157 steps).
@@ -20181,7 +20180,6 @@ Proof modification of "bj-dvelimv" is discouraged (25 steps).
2018120180
Proof modification of "bj-eeanvw" is discouraged (32 steps).
2018220181
Proof modification of "bj-elabd2ALT" is discouraged (100 steps).
2018320182
Proof modification of "bj-elabtru" is discouraged (25 steps).
20184-
Proof modification of "bj-elissetALT" is discouraged (24 steps).
2018520183
Proof modification of "bj-elpwgALT" is discouraged (29 steps).
2018620184
Proof modification of "bj-endbase" is discouraged (81 steps).
2018720185
Proof modification of "bj-endcomp" is discouraged (81 steps).
@@ -20224,7 +20222,7 @@ Proof modification of "bj-imn3ani" is discouraged (18 steps).
2022420222
Proof modification of "bj-inrab2" is discouraged (48 steps).
2022520223
Proof modification of "bj-isseti" is discouraged (15 steps).
2022620224
Proof modification of "bj-issetiv" is discouraged (15 steps).
20227-
Proof modification of "bj-issettru" is discouraged (26 steps).
20225+
Proof modification of "bj-issettruALTV" is discouraged (26 steps).
2022820226
Proof modification of "bj-issetw" is discouraged (21 steps).
2022920227
Proof modification of "bj-issetwt" is discouraged (63 steps).
2023020228
Proof modification of "bj-jarrii" is discouraged (10 steps).
@@ -21124,6 +21122,9 @@ Proof modification of "iscsgrpALT" is discouraged (57 steps).
2112421122
Proof modification of "isdomn2OLD" is discouraged (222 steps).
2112521123
Proof modification of "isdrngdOLD" is discouraged (603 steps).
2112621124
Proof modification of "isdrngrdOLD" is discouraged (334 steps).
21125+
Proof modification of "iseqsetv-clel" is discouraged (26 steps).
21126+
Proof modification of "iseqsetv-cleq" is discouraged (27 steps).
21127+
Proof modification of "iseqsetvlem" is discouraged (15 steps).
2112721128
Proof modification of "iseriALT" is discouraged (54 steps).
2112821129
Proof modification of "isghmOLD" is discouraged (447 steps).
2112921130
Proof modification of "isinfOLD" is discouraged (588 steps).

‎set.mm‎

Lines changed: 82 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -25871,6 +25871,31 @@ the definition of class equality ( ~ df-cleq ). Its forward implication
2587125871
EBGLMPORPCFAHLMN $.
2587225872
$}
2587325873

25874+
${
25875+
$d x z A $.
25876+
$( Lemma for ~ iseqsetv-cleq . (Contributed by Wolf Lammen, 17-Aug-2025.)
25877+
(Proof modification is discouraged.) $)
25878+
iseqsetvlem $p |- ( E. x x = A <-> E. z z = A ) $=
25879+
( cv wceq eqeq1 cbvexvw ) ADZCEBDZCEABHICFG $.
25880+
25881+
$d y A $. $d y z $.
25882+
$( Alternate proof of ~ iseqsetv-clel . The expression ` E. x x = A ` does
25883+
not depend on a particular choice of the set variable. The proof here
25884+
avoids ~ df-clab , ~ df-clel and ~ ax-8 , but instead is based on
25885+
~ ax-9 , ~ ax-ext and ~ df-cleq . In particular it still accepts
25886+
` x e. A ` being a primitive syntax term, not assuming any specific
25887+
semantics (like elementhood in some form).
25888+
25889+
Use it in contexts where you want to avoid ~ df-clab , or you need
25890+
~ df-cleq anyway. See the alternative version , not using ~ df-cleq or
25891+
~ ax-ext or ~ ax-9 . (Contributed by Wolf Lammen, 6-Aug-2025.)
25892+
(Proof modification is discouraged.) $)
25893+
iseqsetv-cleq $p |- ( E. x x = A <-> E. y y = A ) $=
25894+
( vz cv wceq wex iseqsetvlem bitr4i ) AECFAGDECFDGBECFBGADCHBDCHI $.
25895+
$( $j usage 'iseqsetv-cleq' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
25896+
'df-clab'; $)
25897+
$}
25898+
2587425899
${
2587525900
$d ph y $. $d ps y $. $d x y $.
2587625901
$( Equivalent formulas yield equal class abstractions (closed form). This
@@ -26056,6 +26081,31 @@ the definition of class equality ( ~ df-cleq ). Its forward implication
2605626081
$( $j usage 'elex2' avoids 'ax-9' 'df-clab' 'ax-ext'; $)
2605726082
$}
2605826083

26084+
${
26085+
$d A x $. $d x y $.
26086+
$( Weak version of ~ isset . (Contributed by BJ, 24-Apr-2024.) $)
26087+
issettru $p |- ( E. x x = A <-> A e. { y | T. } ) $=
26088+
( cv wceq wex wtru cab wcel wa vextru biantru exbii dfclel bitr4i ) ADZCE
26089+
ZAFQPGBHZIZJZAFCRIQTASQBAKLMACRNO $.
26090+
$( $j usage 'issettru' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
26091+
'ax-ext' 'df-cleq'; $)
26092+
$}
26093+
26094+
${
26095+
$d x z A $. $d y z A $.
26096+
$( Alternate proof of ~ iseqsetv-cleq . The expression ` E. x x = A ` does
26097+
not depend on a particular choice of the set variable. Use this theorem
26098+
in contexts where ~ df-cleq or ~ ax-ext is not referenced elsewhere in
26099+
your proof. It is proven from a specific implementation (class builder,
26100+
axiom ~ df-clab ) of the primitive term ` x e. A ` . (Contributed by
26101+
BJ, 29-Apr-2019.) (Proof modification is discouraged.) $)
26102+
iseqsetv-clel $p |- ( E. x x = A <-> E. y y = A ) $=
26103+
( vz cv wceq wex wtru cab wcel issettru bitr4i ) AECFAGCHDIJBECFBGADCKBDC
26104+
KL $.
26105+
$( $j usage 'iseqsetv-clel' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
26106+
'ax-ext' 'df-cleq'; $)
26107+
$}
26108+
2605926109
${
2606026110
$d A x $. $d V x $.
2606126111
issetlem.1 $e |- x e. V $.
@@ -26086,8 +26136,8 @@ the definition of class equality ( ~ df-cleq ). Its forward implication
2608626136
by NM, 1-May-1995.) Reduce dependencies on axioms. (Revised by BJ,
2608726137
29-Apr-2019.) $)
2608826138
elisset $p |- ( A e. V -> E. x x = A ) $=
26089-
( vy vz wcel cv wceq wex elissetv wtru cab vextru issetlem bitr3i sylib )
26090-
BCFDGBHDIZAGBHAIZDBCJQBKELZFRDBSEDMNABSEAMNOP $.
26139+
( vz wcel cv wceq wex elissetv iseqsetv-clel sylib ) BCEDFBGDHAFBGAHDBCID
26140+
ABJK $.
2609126141
$( $j usage 'elisset' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
2609226142
'ax-ext' 'df-cleq'; $)
2609326143
$}
@@ -26735,11 +26785,11 @@ generally appear in a single form (either definitional, but more often
2673526785
~ ax-11 , see ~ sbc5ALT for more details. (Revised by SN,
2673626786
2-Sep-2024.) $)
2673726787
clelab $p |- ( A e. { x | ph } <-> E. x ( x = A /\ ph ) ) $=
26738-
( vy cab wcel cv wex wa elissetv exsimpl eqeq1 cbvexvw sylib wb eleq1 weq
26788+
( vy cab wcel cv wex wa elissetv exsimpl iseqsetv-cleq sylib wb eleq1 weq
2673926789
wceq wsb df-clab sb5 bitri anbi1d exbidv bitrid bitr3d exlimiv pm5.21nii
26740-
eqeq2 ) CABEZFZDGZCRZDHZBGZCRZAIZBHZDCUJJURUPBHUNUPABKUPUMBDUOULCLMNUMUKU
26741-
RODUMULUJFZUKURULCUJPUSBDQZAIZBHZUMURUSABDSVBADBTABDUAUBUMVAUQBUMUTUPAULC
26742-
UOUIUCUDUEUFUGUH $.
26790+
eqeq2 ) CABEZFZDGZCQZDHZBGZCQZAIZBHZDCUIJUQUOBHUMUOABKBDCLMULUJUQNDULUKUI
26791+
FZUJUQUKCUIOURBDPZAIZBHZULUQURABDRVAADBSABDTUAULUTUPBULUSUOAUKCUNUHUBUCUD
26792+
UEUFUG $.
2674326793
$( $j usage 'clelab' avoids 'ax-11'; $)
2674426794

2674526795
$( Obsolete version of ~ clelab as of 2-Sep-2024. (Contributed by NM,
@@ -69791,8 +69841,8 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more
6979169841
$d ph y $. $d ps x $. $d F x y $. $d B x y $.
6979269842
ralima.x $e |- ( x = ( F ` y ) -> ( ph <-> ps ) ) $.
6979369843
$( Universal quantification under an image in terms of the base set.
69794-
(Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Matthew House,
69795-
14-Aug-2025.) $)
69844+
(Contributed by Stefan O'Rear, 21-Jan-2015.) Reduce DV conditions.
69845+
(Revised by Matthew House, 14-Aug-2025.) $)
6979669846
ralima $p |- ( ( F Fn A /\ B C_ A ) ->
6979769847
( A. x e. ( F " B ) ph <-> A. y e. B ps ) ) $=
6979869848
( wfn cdm wss cima wral wb fnfun wa cv wcel wceq wrex funfnd fndm biimpar
@@ -69802,8 +69852,8 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more
6980269852
UIUJVFABNVAHUKULUM $.
6980369853

6980469854
$( Existential quantification under an image in terms of the base set.
69805-
(Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Matthew House,
69806-
14-Aug-2025.) $)
69855+
(Contributed by Stefan O'Rear, 21-Jan-2015.) Reduce DV conditions.
69856+
(Revised by Matthew House, 14-Aug-2025.) $)
6980769857
rexima $p |- ( ( F Fn A /\ B C_ A ) ->
6980869858
( E. x e. ( F " B ) ph <-> E. y e. B ps ) ) $=
6980969859
( wfn wss wa wn cima wral wrex cv cfv wceq notbid dfrex2 ralima 3bitr4g )
@@ -587409,7 +587459,9 @@ with by (1) and (2a). Note that in order to prove ~ eliminable2a ,
587409587459

587410587460
${
587411587461
$d A x $. $d x y $.
587412-
$( Lemma for ~ bj-denotes . (Contributed by BJ, 24-Apr-2024.)
587462+
$( Duplicate of ~ issettru and ~ bj-issettruALTV .
587463+
587464+
Lemma for ~ bj-denotesALTV . (Contributed by BJ, 24-Apr-2024.)
587413587465
(Proof modification is discouraged.) $)
587414587466
bj-denoteslem $p |- ( E. x x = A <-> A e. { y | T. } ) $=
587415587467
( cv wceq wex wtru cab wcel wa vextru biantru exbii dfclel bitr4i ) ADZCE
@@ -587418,7 +587470,9 @@ with by (1) and (2a). Note that in order to prove ~ eliminable2a ,
587418587470

587419587471
${
587420587472
$d x A $. $d y A $. $d x z $. $d y z $.
587421-
$( This would be the justification theorem for the definition of the unary
587473+
$( Moved to main as ~ iseqsetv-clel and kept for the comments.
587474+
587475+
This would be the justification theorem for the definition of the unary
587422587476
predicate "E!" by ` |- ( ` E! ` A <-> E. x x = A ) ` which could be
587423587477
interpreted as " ` A ` exists" (as a set) or " ` A ` denotes" (in the
587424587478
sense of free logic).
@@ -587450,21 +587504,23 @@ with by (1) and (2a). Note that in order to prove ~ eliminable2a ,
587450587504

587451587505
(Contributed by BJ, 29-Apr-2019.)
587452587506
(Proof modification is discouraged.) $)
587453-
bj-denotes $p |- ( E. x x = A <-> E. y y = A ) $=
587507+
bj-denotesALTV $p |- ( E. x x = A <-> E. y y = A ) $=
587454587508
( vz cv wceq wex wtru cab wcel bj-denoteslem bitr4i ) AECFAGCHDIJBECFBGAD
587455587509
CKBDCKL $.
587456-
$( $j usage 'bj-denotes' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
587510+
$( $j usage 'bj-denotesALTV' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
587457587511
'ax-ext' 'df-cleq'; $)
587458587512
$}
587459587513

587460587514
${
587461587515
$d A x $. $d A z $. $d y z $.
587462-
$( Weak version of ~ isset without ~ ax-ext . (Contributed by BJ,
587516+
$( Moved to main as ~ issettru and kept for the comments.
587517+
587518+
Weak version of ~ isset without ~ ax-ext . (Contributed by BJ,
587463587519
24-Apr-2024.) (Proof modification is discouraged.) $)
587464-
bj-issettru $p |- ( E. x x = A <-> A e. { y | T. } ) $=
587465-
( vz cv wceq wex wtru cab wcel bj-denotes bj-denoteslem bitri ) AECFAGDEC
587466-
FDGCHBIJADCKDBCLM $.
587467-
$( $j usage 'bj-issettru' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
587520+
bj-issettruALTV $p |- ( E. x x = A <-> A e. { y | T. } ) $=
587521+
( vz cv wceq wex wtru cab wcel iseqsetv-clel issettru bitri ) AECFAGDECFD
587522+
GCHBIJADCKDBCLM $.
587523+
$( $j usage 'bj-issettruALTV' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
587468587524
'ax-ext' 'df-cleq'; $)
587469587525
$}
587470587526

@@ -587474,8 +587530,8 @@ with by (1) and (2a). Note that in order to prove ~ eliminable2a ,
587474587530
"universal" class without ~ ax-ext . (Contributed by BJ, 24-Apr-2024.)
587475587531
(Proof modification is discouraged.) $)
587476587532
bj-elabtru $p |- ( A e. { x | T. } <-> A e. { y | T. } ) $=
587477-
( vz wtru cab wcel cv wceq wex bj-denoteslem bitr3i ) CEAFGDHCIDJCEBFGDAC
587478-
KDBCKL $.
587533+
( vz wtru cab wcel cv wceq wex issettru bitr3i ) CEAFGDHCIDJCEBFGDACKDBCK
587534+
L $.
587479587535
$( $j usage 'bj-elabtru' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
587480587536
'ax-ext' 'df-cleq'; $)
587481587537
$}
@@ -587485,9 +587541,9 @@ with by (1) and (2a). Note that in order to prove ~ eliminable2a ,
587485587541
$( Closed form of ~ bj-issetw . (Contributed by BJ, 29-Apr-2019.)
587486587542
(Proof modification is discouraged.) $)
587487587543
bj-issetwt $p |- ( A. x ph -> ( A e. { x | ph } <-> E. y y = A ) ) $=
587488-
( vz wal cab wcel cv wceq wa wex wb dfclel a1i biantrud bicomd bj-denotes
587489-
vexwt exbidv 3bitrd ) ABFZDABGZHZEIZDJZUEUCHZKZELZUFELZCIDJCLZUDUIMUBEDUC
587490-
NOUBUHUFEUBUFUHUBUGUFABESPQTUJUKMUBECDROUA $.
587544+
( vz wal cab wcel cv wceq wa wex wb dfclel a1i vexwt bicomd iseqsetv-clel
587545+
biantrud exbidv 3bitrd ) ABFZDABGZHZEIZDJZUEUCHZKZELZUFELZCIDJCLZUDUIMUBE
587546+
DUCNOUBUHUFEUBUFUHUBUGUFABEPSQTUJUKMUBECDROUA $.
587491587547
$( $j usage 'bj-issetwt' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
587492587548
'ax-ext' 'df-cleq'; $)
587493587549
$}
@@ -587506,20 +587562,6 @@ with by (1) and (2a). Note that in order to prove ~ eliminable2a ,
587506587562
'ax-ext' 'df-cleq'; $)
587507587563
$}
587508587564

587509-
${
587510-
$d x A $. $d y A $. $d y V $.
587511-
$( Alternate proof of ~ elisset . This is essentially the same proof as
587512-
seen by inlining ~ bj-denotes and ~ bj-denoteslem . Use ~ elissetv
587513-
instead when sufficient (in particular when ` V ` is substituted for
587514-
` _V ` ). (Contributed by BJ, 29-Apr-2019.)
587515-
(Proof modification is discouraged.) (New usage is discouraged.) $)
587516-
bj-elissetALT $p |- ( A e. V -> E. x x = A ) $=
587517-
( vy wcel cv wceq wex elissetv bj-denotes sylib ) BCEDFBGDHAFBGAHDBCIDABJ
587518-
K $.
587519-
$( $j usage 'bj-elissetALT' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
587520-
'ax-ext' 'df-cleq'; $)
587521-
$}
587522-
587523587565
${
587524587566
$d x A $. $d x V $.
587525587567
bj-issetiv.1 $e |- A e. V $.
@@ -588038,8 +588080,8 @@ but the latter requires a domain with at least two objects (hence uses
588038588080
as a byproduct, this dispenses with ~ ax-11 and ~ ax-13 ). (Contributed
588039588081
by BJ, 30-Apr-2019.) (Proof modification is discouraged.) $)
588040588082
bj-vtoclg1f1 $p |- ( E. y y = A -> ps ) $=
588041-
( cv wceq wex bj-denotes bj-exlimmpi sylbi ) DIEJDKCIEJZCKBDCELABOCFGHMN
588042-
$.
588083+
( cv wceq wex iseqsetv-clel bj-exlimmpi sylbi ) DIEJDKCIEJZCKBDCELABOCFGH
588084+
MN $.
588043588085
$}
588044588086

588045588087
${

0 commit comments

Comments
 (0)