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

Moving theorems to the main #4564

Open
wants to merge 5 commits into
base: develop
Choose a base branch
from
+51 −115
Open

Moving theorems to the main #4564

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
4493138
disjcsn/bnj521 to main
mazsa Jan 12, 2025
6774571
undif5 to main
mazsa Jan 12, 2025
f2d0fc0
ceqsrexv2 ceqsralv2 to main
mazsa Jan 12, 2025
8a8e0be
deleted ceqsrexv2; ceqsralv2 -> ceqsralbv
mazsa Jan 12, 2025
566ecee
Minor
mazsa Jan 12, 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
3 changes: 0 additions & 3 deletions discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2441,8 +2441,6 @@
"bnj518" is used by "bnj546".
"bnj519" is used by "bnj535".
"bnj519" is used by "bnj97".
"bnj521" is used by "bnj535".
"bnj521" is used by "bnj927".
"bnj523" is used by "bnj600".
"bnj523" is used by "bnj908".
"bnj523" is used by "bnj934".
Expand Down Expand Up @@ -15157,7 +15155,6 @@ New usage of "bnj446" is discouraged (3 uses).
New usage of "bnj517" is discouraged (1 uses).
New usage of "bnj518" is discouraged (2 uses).
New usage of "bnj519" is discouraged (2 uses).
New usage of "bnj521" is discouraged (2 uses).
New usage of "bnj523" is discouraged (3 uses).
New usage of "bnj524" is discouraged (0 uses).
New usage of "bnj525" is discouraged (7 uses).
Expand Down
163 changes: 51 additions & 112 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33834,6 +33834,13 @@ general is seen either by substitution (when the variable ` V ` has no
( wcel cv wceq wa wrex r19.42v eleq1 adantr pm5.32ri bicomi baib ceqsrexv
wb rexbiia pm5.32i 3bitr3i ) DEGZCHZDIZAJZJZCEKUCUFCEKZJUHUCBJUCUFCELUGUF
CEUGUDEGZUFUIUFJUGUFUIUCUEUIUCSAUDDEMNOPQTUCUHBABCDEFRUAUB $.

$( Alternate elimination of a restricted universal quantifier, using
implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) $)
ceqsralbv $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $=
( cv wceq wi wral wcel wn wa wrex notbid ceqsrexbv rexanali annim 3bitr3i
con4bii ) CGDHZAICEJZDEKZBIZUAALZMCENUCBLZMUBLUDLUEUFCDEUAABFOPUAACEQUCBR
ST $.
$}

${
Expand Down Expand Up @@ -41684,6 +41691,11 @@ disjoint classes (see ~ disjdif ). Part of proof of Corollary 6K of
( wss cun wceq cdif ssequn1 undif2 eqeq1i bitr4i ) ABCABDZBEABAFDZBEABGLKBA
BHIJ $.

$( An equality involving class union and class difference. (Contributed by
Thierry Arnoux, 26-Jun-2024.) $)
undif5 $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $=
( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $.

$( A subset of a difference does not intersect the subtrahend. (Contributed
by Jeff Hankins, 1-Sep-2013.) (Proof shortened by Mario Carneiro,
24-Aug-2015.) $)
Expand Down Expand Up @@ -99316,6 +99328,12 @@ is that it denies the existence of a set containing itself ( ~ elirrv ).
( cv wnel cab cvv vprc nelir wceq wb ruv neleq1 ax-mp mpbir ) ABZNCADZECZEE
CZEEFGOEHPQIAJOEEKLM $.

$( A class is disjoint from its singleton. A consequence of regularity.
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by BJ,
4-Apr-2019.) $)
disjcsn $p |- ( A i^i { A } ) = (/) $=
( csn cin c0 wceq wcel wn elirr disjsn mpbir ) AABCDEAAFGAHAAIJ $.

${
$d x y A $.
$( The membership relation is well-founded on any class. (Contributed by
Expand Down Expand Up @@ -473556,11 +473574,6 @@ Class abstractions (a.k.a. class builders)
( wceq wss wa cdif c0 eqss ssdif0 anbi12i sylbbr ) ABCABDZBADZEABFGCZBAFGCZ
EABHLNMOABIBAIJK $.

$( An equality involving class union and class difference. (Contributed by
Thierry Arnoux, 26-Jun-2024.) $)
undif5 $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $=
( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $.

$( Two ways to express equality relative to a class ` A ` . (Contributed by
Thierry Arnoux, 23-Jun-2024.) $)
indifbi $p |- ( ( A i^i B ) = ( A i^i C ) <-> ( A \ B ) = ( A \ C ) ) $=
Expand Down Expand Up @@ -513604,17 +513617,6 @@ conditions of the Five Segment Axiom ( ~ axtg5seg ). See ~ df-ofs .
( cvv wcel cop csn wfun funsng mpan ) ADEBDEABFGHCABDDIJ $.
$}

${
$d A x $.
$( First-order logic and set theory. (Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.) $)
bnj521 $p |- ( A i^i { A } ) = (/) $=
( vx csn cin c0 wne wn wceq cv wcel wex elirr wa elin velsn eleq1 biimpac
sylan2b sylbi exlimiv mto n0 mtbir nne mpbi ) AACZDZEFZGUGEHUHBIZUGJZBKZU
KAAJZALUJULBUJUIAJZUIUFJZMULUIAUFNUNUMUIAHZULBAOUOUMULUIAAPQRSTUABUGUBUCU
GEUDUE $.
$}

${
bnj524.1 $e |- ( ph <-> ps ) $.
bnj524.2 $e |- A e. _V $.
Expand Down Expand Up @@ -513905,10 +513907,10 @@ conditions of the Five Segment Axiom ( ~ axtg5seg ). See ~ df-ofs .
$( First-order logic and set theory. (Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.) $)
bnj927 $p |- ( ( p = suc n /\ f Fn n ) -> G Fn p ) $=
( cv csuc wceq wfn wa csn cun cop simpr vex fnsn a1i cin c0 bnj521 fneq1i
fnund sylibr df-suc eqeq2i biimpi adantr fneq2d mpbird ) EHZCHZIZJZBHZUMK
ZLZDULKDUMUMMZNZKZURUPUMAOMZNZUTKVAURUMUSUPVBUOUQPVBUSKURUMACQGRSUMUSTUAJ
URUMUBSUDUTDVCFUCUEURULUTDUOULUTJZUQUOVDUNUTULUMUFUGUHUIUJUK $.
( cv csuc wceq wfn wa csn cun cop simpr vex fnsn a1i cin c0 disjcsn fnund
fneq1i sylibr df-suc eqeq2i biimpi adantr fneq2d mpbird ) EHZCHZIZJZBHZUM
KZLZDULKDUMUMMZNZKZURUPUMAOMZNZUTKVAURUMUSUPVBUOUQPVBUSKURUMACQGRSUMUSTUA
JURUMUBSUCUTDVCFUDUEURULUTDUOULUTJZUQUOVDUNUTULUMUFUGUHUIUJUK $.
$}

${
Expand Down Expand Up @@ -515466,12 +515468,12 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a
n ) $=
( cv wfn cvv w-bnj15 csn cun wceq w-bnj17 bnj422 bnj251 bitri cfv c-bnj14
ciun cop wcel wfun wral fvex bnj518 iunexg sylancr vex bnj519 syl dmsnopg
wa cdm bnj1422 cin c0 bnj521 mpan2 sylan2 fneq1i sylibr fneq2 syl5ibr imp
fnun sylbi ) DEUAZAIRZHRZWAUBZUCZUDZFRZWASZUEZWDWFVSAVDZVDZVDZJVTSZWGWDWF
VSAUEWJVSAWDWFUFWDWFVSAUGUHWDWIWKWIWKWDJWCSZWIWEWACKRZWEUIZDECRUJZUKZULUB
ZUCZWCSZWLWHWFWQWBSZWSWHWQWBWHWPTUMZWQUNWHWNTUMWOTUMCWNUOXAWMWEUPLMABCDEF
GHKNOQUQCWNWOTTURUSZWAWPHUTVAVBWHXAWQVEWBUDXBWAWPTVCVBVFWFWTVDWAWBVGVHUDW
SWAVIWAWBWEWQVQVJVKWCJWRPVLVMVTWCJVNVOVPVR $.
wa cdm bnj1422 cin c0 disjcsn fnun mpan2 sylan2 fneq1i sylibr syl5ibr imp
fneq2 sylbi ) DEUAZAIRZHRZWAUBZUCZUDZFRZWASZUEZWDWFVSAVDZVDZVDZJVTSZWGWDW
FVSAUEWJVSAWDWFUFWDWFVSAUGUHWDWIWKWIWKWDJWCSZWIWEWACKRZWEUIZDECRUJZUKZULU
BZUCZWCSZWLWHWFWQWBSZWSWHWQWBWHWPTUMZWQUNWHWNTUMWOTUMCWNUOXAWMWEUPLMABCDE
FGHKNOQUQCWNWOTTURUSZWAWPHUTVAVBWHXAWQVEWBUDXBWAWPTVCVBVFWFWTVDWAWBVGVHUD
WSWAVIWAWBWEWQVJVKVLWCJWRPVMVNVTWCJVQVOVPVR $.
$}

${
Expand Down Expand Up @@ -532429,15 +532431,6 @@ Real and complex numbers (cont.)
brtpid3 $p |- A { C , D , <. A , B >. } B $=
( cop ctp wbr wcel opex tpid3 df-br mpbir ) ABCDABEZFZGMNHCDMABIJABNKL $.

${
$d A x $. $d B x $. $d ps x $.
ceqsrexv2.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
$( Alternate elimitation of a restricted existential quantifier, using
implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) $)
ceqsrexv2 $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $=
( ceqsrexbv ) ABCDEFG $.
$}

${
$d x V $. $d A y $. $d ps y $. $d x y $.
iota5f.1 $e |- F/ x ph $.
Expand All @@ -532452,17 +532445,6 @@ Real and complex numbers (cont.)
GUEVEUTUNBVCDUMTUBUFVCDUQTUCBCIUGUHUIUJ $.
$}

${
$d x A $. $d x B $. $d ps x $.
ceqsralv2.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
$( Alternate elimination of a restricted universal quantifier, using
implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) $)
ceqsralv2 $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $=
( cv wceq wi wral wcel wn wa wrex notbid ceqsrexv2 rexanali annim 3bitr3i
con4bii ) CGDHZAICEJZDEKZBIZUAALZMCENUCBLZMUBLUDLUEUFCDEUAABFOPUAACEQUCBR
ST $.
$}

$( A class is ordinal iff it is a subclass of ` On ` and transitive.
(Contributed by Scott Fenton, 21-Nov-2021.) $)
dford5 $p |- ( Ord A <-> ( A C_ On /\ Tr A ) ) $=
Expand Down Expand Up @@ -555369,15 +555351,9 @@ FOL part ( ~ bj-ru0 ) and then two versions ( ~ bj-ru1 and ~ bj-ru ).
( c0 wne cv wcel wex n0 mpbi ) BDEAFBGAHCABIJ $.
$}

$( A class is disjoint from its singleton. A consequence of regularity.
Shorter proof than ~ bnj521 and does not depend on ~ df-ne . (Contributed
by BJ, 4-Apr-2019.) $)
bj-disjcsn $p |- ( A i^i { A } ) = (/) $=
( csn cin c0 wceq wcel wn elirr disjsn mpbir ) AABCDEAAFGAHAAIJ $.

$( Disjointness of the singletons containing 0 and 1. This is a consequence
of ~ bj-disjcsn but the present proof does not use regularity.
(Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.) $)
of ~ disjcsn but the present proof does not use regularity. (Contributed
by BJ, 4-Apr-2019.) (Proof modification is discouraged.) $)
bj-disjsn01 $p |- ( { (/) } i^i { 1o } ) = (/) $=
( c0 c1o wne csn cin wceq 1n0 necomi disjsn2 ax-mp ) ABCADBDEAFBAGHABIJ $.

Expand Down Expand Up @@ -581130,7 +581106,7 @@ A collection of theorems for commuting equalities (or
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

$( Contents: ~ https://us.metamath.org/mpeuni/mmtheorems.html#dtl:20.21 $)
$( Contents: ~ https://us.metamath.org/mpeuni/mmtheorems.html#dtl:20.22 $)


$(
Expand Down Expand Up @@ -581511,24 +581487,10 @@ A collection of theorems for commuting equalities (or
suceqsneq $p |- ( A e. V -> ( suc A = suc B <-> { A } = { B } ) ) $=
( wcel csuc wceq csn suc11reg sneqbg bitr4id ) ACDAEBEFABFAGBGFABHABCIJ $.

$( A class is disjoint from its singleton. A consequence of regularity.
Shorter proof than ~ bnj521 and does not depend on ~ df-ne . (Temporary:
as soon as this Mathbox only PR is accepted, I'll open a PR to place this
to the main. PM) (Contributed by BJ, 4-Apr-2019.) $)
disjcsn $p |- ( A i^i { A } ) = (/) $=
( csn cin c0 wceq wcel wn elirr disjsn mpbir ) AABCDEAAFGAHAAIJ $.

$( An equality involving class union and class difference. (Temporary: as
soon as this Mathbox only PR is accepted, I'll open a PR to place this to
the main. PM) (Contributed by Thierry Arnoux, 26-Jun-2024.) $)
undif5TEMP $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $=
( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $.

$( Absorption of union with a singleton by difference. (Contributed by Peter
Mazsa, 24-Jul-2024.) $)
sucdifsn2 $p |- ( ( A u. { A } ) \ { A } ) = A $=
( csn cin c0 wceq cun cdif disjcsn undif5TEMP ax-mp ) AABZCDEAKFKGAEAHAKIJ
$.
( csn cin c0 wceq cun cdif disjcsn undif5 ax-mp ) AABZCDEAKFKGAEAHAKIJ $.

$( The difference between the successor and the singleton of a class is the
class. (Contributed by Peter Mazsa, 20-Sep-2024.) $)
Expand Down Expand Up @@ -582200,38 +582162,16 @@ equivalence of domain elementhood (equivalence is not necessary as
HUFUEUHPBUCUDQRSTUBUA $.
$}

${
$d A x $. $d B x $. $d ps x $.
ceqsrexv2TEMP.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
$( Alternate elimitation of a restricted existential quantifier, using
implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) $)
ceqsrexv2TEMP $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $=
( ceqsrexbv ) ABCDEFG $.
$}

${
$d x A $. $d x B $. $d ps x $.
ceqsralv2TEMP.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
$( Alternate elimination of a restricted universal quantifier, using
implicit substitution. (Temporary: as soon as this Mathbox only PR is
accepted, I'll open a PR to place this to the main. PM) (Contributed by
Scott Fenton, 7-Dec-2020.) $)
ceqsralv2TEMP $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $=
( cv wceq wi wral wcel wrex notbid ceqsrexv2TEMP rexanali 3bitr3i con4bii
wn wa annim ) CGDHZAICEJZDEKZBIZUAARZSCELUCBRZSUBRUDRUEUFCDEUAABFMNUAACEO
UCBTPQ $.
$}

${
$d A x y $. $d B x y $. $d R x y $.
$( Two ways to say that an intersection of the identity relation with a
Cartesian product is a subclass. (Contributed by Peter Mazsa,
12-Dec-2023.) $)
ref5 $p |- ( ( _I i^i ( A X. B ) ) C_ R <-> A. x e. ( A i^i B ) x R x ) $=
( vy cv wceq wbr wi wral wcel cid cxp cin wss equcom imbi1i ceqsralv2TEMP
ralbii breq2 bitr3i idinxpss ralin 3bitr4i ) AFZEFZGZUEUFDHZIZECJZABJUECK
UEUEDHZIZABJLBCMNDOUKABCNJUJULABUJUFUEGZUHIZECJULUNUIECUMUGUHEAPQSUHUKEUE
CUFUEUEDTRUASAEBCDUBUKABCUCUD $.
( vy cv wceq wbr wral wcel cid cxp cin wss equcom imbi1i ralbii ceqsralbv
wi breq2 bitr3i idinxpss ralin 3bitr4i ) AFZEFZGZUEUFDHZSZECIZABIUECJUEUE
DHZSZABIKBCLMDNUKABCMIUJULABUJUFUEGZUHSZECIULUNUIECUMUGUHEAOPQUHUKEUECUFU
EUEDTRUAQAEBCDUBUKABCUCUD $.
$}

${
Expand Down Expand Up @@ -587076,8 +587016,8 @@ the null class is disjoint (which it is, see ~ disjALTV0 ). (Contributed
eqvrel1cossinidres $p |- EqvRel ,~ ( R i^i ( _I |` A ) ) $=
( cid cres cin disjALTVinidres disjimi ) BCADEABFG $.

$( The cosets by a tail Cartesian product with a restricted identity relation
are in equivalence relation. (Contributed by Peter Mazsa,
$( The cosets by a range Cartesian product with a restricted identity
relation are in equivalence relation. (Contributed by Peter Mazsa,
31-Dec-2021.) $)
eqvrel1cossxrnidres $p |- EqvRel ,~ ( R |X. ( _I |` A ) ) $=
( cid cres cxrn disjALTVxrnidres disjimi ) BCADEABFG $.
Expand Down Expand Up @@ -587107,8 +587047,8 @@ the null class is disjoint (which it is, see ~ disjALTV0 ). (Contributed
EqvRel ,~ ( R i^i ( _I |` A ) ) ) $=
( cid cres cin disjALTVinidres detlem ) BCADEABFG $.

$( The cosets by the tail Cartesian product with the restricted identity
relation are in equivalence relation if and only if the tail Cartesian
$( The cosets by the range Cartesian product with the restricted identity
relation are in equivalence relation if and only if the range Cartesian
product with the restricted identity relation is disjoint. (Contributed
by Peter Mazsa, 31-Dec-2021.) $)
detxrnidres $p |- ( Disj ( R |X. ( _I |` A ) ) <->
Expand Down Expand Up @@ -587384,8 +587324,8 @@ implies disjointness (e.g. ~ eqvrelqseqdisj5 ), or converse function
wceq dfpart2 dferALTV2 3bitr4i ) BCADEZFSGSHAOISJZKTGTHAOIASLATMABNASPATQR
$.

$( Class ` A ` is a partition by a tail Cartesian product with the identity
class restricted to it if and only if the cosets by the tail Cartesian
$( Class ` A ` is a partition by a range Cartesian product with the identity
class restricted to it if and only if the cosets by the range Cartesian
product are in equivalence relation on it. (Contributed by Peter Mazsa,
31-Dec-2021.) $)
petxrnidres2 $p |- ( ( Disj ( R |X. ( _I |` A ) ) /\
Expand All @@ -587396,9 +587336,9 @@ implies disjointness (e.g. ~ eqvrelqseqdisj5 ), or converse function
,~ ( R |X. ( _I |` A ) ) ) = A ) ) $=
( cid cres cxrn disjALTVxrnidres petlemi ) ABCADEABFG $.

$( A class is a partition by a tail Cartesian product with the identity class
restricted to it if and only if the cosets by the tail Cartesian product
are in equivalence relation on it. Cf. ~ br1cossxrnidres ,
$( A class is a partition by a range Cartesian product with the identity
class restricted to it if and only if the cosets by the range Cartesian
product are in equivalence relation on it. Cf. ~ br1cossxrnidres ,
~ disjALTVxrnidres and ~ eqvrel1cossxrnidres . (Contributed by Peter
Mazsa, 31-Dec-2021.) $)
petxrnidres $p |- ( ( R |X. ( _I |` A ) ) Part A <->
Expand Down Expand Up @@ -587444,7 +587384,7 @@ implies disjointness (e.g. ~ eqvrelqseqdisj5 ), or converse function
( weqvrel cep ccnv cqs cres wdisjALTV cin eqvreldisj3 disjimin syl ) BDEFAB
GHZICNJIABKCNLM $.

$( Tail Cartesian product with converse epsilon relation restricted to the
$( Range Cartesian product with converse epsilon relation restricted to the
quotient set of an equivalence relation is disjoint. (Contributed by
Peter Mazsa, 30-May-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) $)
eqvreldisj5 $p |- ( EqvRel R -> Disj ( S |X. ( `' _E |` ( B /. R ) ) ) ) $=
Expand Down Expand Up @@ -587569,9 +587509,8 @@ is what we used to think of as the partition equivalence theorem (but cf.

$( Member Partition-Equivalence Theorem in its shortest possible form: it
shows that member partitions and comember equivalence relations are
literally the same. Cf. ~ pet , the general Partition-Equivalence
Theorem, with general ` R ` . (Contributed by Peter Mazsa,
31-Dec-2024.) $)
literally the same. Cf. ~ pet , the Partition-Equivalence Theorem, with
general ` R ` . (Contributed by Peter Mazsa, 31-Dec-2024.) $)
mpets $p |- MembParts = CoMembErs $=
( va cep ccnv cv cres cparts wbr ccoss cers cmembparts ccomembers wb mpets2
cab cvv elv abbii df-membparts df-comembers 3eqtr4i ) BCADZEZUAFGZANUBHUAIG
Expand Down Expand Up @@ -587643,10 +587582,10 @@ is what we used to think of as the partition equivalence theorem (but cf.

$( Partition-Equivalence Theorem with general ` R ` while preserving the
restricted converse epsilon relation of ~ mpet2 (as opposed to
~ petincnvepres ). A class is a partition by a tail Cartesian product
~ petincnvepres ). A class is a partition by a range Cartesian product
with general ` R ` and the restricted converse element class if and only
if the cosets by the tail Cartesian product are in an equivalence relation
on it. Cf. ~ br1cossxrncnvepres .
if the cosets by the range Cartesian product are in an equivalence
relation on it. Cf. ~ br1cossxrncnvepres .

This theorem (together with ~ pets and ~ pet2 ) is the main result of my
investigation into set theory. It is no more general than the
Expand Down
Loading