From 86809e0679f16ede755a6f082f50748952855573 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <30736367+wlammen@users.noreply.github.com>
Date: Thu, 27 Feb 2025 07:40:03 +0100
Subject: [PATCH] eqab -> eqabb (#4676)
* eqabw -> eqabbw
* eqab -> eqabb
* delete outdated OLD
* abbi -> abbib in nf.mm
* eqab -> eqabb in nf.mm
* update eqab reference in comment in nf.mm
* update mmset.raw.html
* shorten eqabr
* typo
* rm duplicated line
* eqabc -> eqabbc
* eqabbc -> eqabcb
---
changes-set.txt | 6 +-
discouraged | 9 +-
mmset.raw.html | 4 +-
nf.mm | 282 +++++++++++++------------
set.mm | 551 ++++++++++++++++++++++++------------------------
5 files changed, 422 insertions(+), 430 deletions(-)
diff --git a/changes-set.txt b/changes-set.txt
index 5b500283d3..3baa109f84 100644
--- a/changes-set.txt
+++ b/changes-set.txt
@@ -143,9 +143,9 @@ Date Old New Notes
15-Feb-25 abeq1i eqabci
15-Feb-25 abeq2i eqabi
15-Feb-25 abeq2d eqabd
-15-Feb-25 abeq2w eqabw
-15-Feb-25 abeq1 eqabc Commuted form of eqab
-15-Feb-25 abeq2 eqab Basic closed form
+15-Feb-25 abeq2w eqabbw
+15-Feb-25 abeq1 eqabbc Commuted form of eqabb
+15-Feb-25 abeq2 eqabb Basic closed form
14-Feb-25 --- --- Moved surreal negation theorems
from SF's mathbox to main set.mm
14-Feb-25 grpinvcld --- Moved from SN's mathbox to main set.mm
diff --git a/discouraged b/discouraged
index e1d6de3357..e865956a3b 100644
--- a/discouraged
+++ b/discouraged
@@ -10397,7 +10397,6 @@
"nfsb2" is used by "sb9".
"nfsb2" is used by "sbco3".
"nfsb2" is used by "wl-nfs1t".
-"nfsb4" is used by "nfsbOLD".
"nfsb4" is used by "sbco2".
"nfsb4t" is used by "nfsb4".
"nfsb4t" is used by "nfsbd".
@@ -16579,7 +16578,7 @@ New usage of "epweonALT" is discouraged (0 uses).
New usage of "eq0ALT" is discouraged (0 uses).
New usage of "eq0OLDOLD" is discouraged (0 uses).
New usage of "eq0rdvALT" is discouraged (0 uses).
-New usage of "eqabOLD" is discouraged (0 uses).
+New usage of "eqabbOLD" is discouraged (0 uses).
New usage of "eqeq12OLD" is discouraged (1 uses).
New usage of "eqeq12dOLD" is discouraged (1 uses).
New usage of "eqeq1dALT" is discouraged (0 uses).
@@ -17999,9 +17998,8 @@ New usage of "nfs1" is discouraged (2 uses).
New usage of "nfsabg" is discouraged (1 uses).
New usage of "nfsb" is discouraged (17 uses).
New usage of "nfsb2" is discouraged (4 uses).
-New usage of "nfsb4" is discouraged (2 uses).
+New usage of "nfsb4" is discouraged (1 uses).
New usage of "nfsb4t" is discouraged (2 uses).
-New usage of "nfsbOLD" is discouraged (0 uses).
New usage of "nfsbc" is discouraged (4 uses).
New usage of "nfsbcd" is discouraged (3 uses).
New usage of "nfsbd" is discouraged (3 uses).
@@ -20477,7 +20475,7 @@ Proof modification of "epweonALT" is discouraged (86 steps).
Proof modification of "eq0ALT" is discouraged (31 steps).
Proof modification of "eq0OLDOLD" is discouraged (6 steps).
Proof modification of "eq0rdvALT" is discouraged (25 steps).
-Proof modification of "eqabOLD" is discouraged (47 steps).
+Proof modification of "eqabbOLD" is discouraged (47 steps).
Proof modification of "eqeq12OLD" is discouraged (24 steps).
Proof modification of "eqeq12dOLD" is discouraged (22 steps).
Proof modification of "eqeq1dALT" is discouraged (62 steps).
@@ -21000,7 +20998,6 @@ Proof modification of "nfraldwOLD" is discouraged (41 steps).
Proof modification of "nfralwOLD" is discouraged (27 steps).
Proof modification of "nfreuwOLD" is discouraged (56 steps).
Proof modification of "nfrmowOLD" is discouraged (55 steps).
-Proof modification of "nfsbOLD" is discouraged (23 steps).
Proof modification of "nfsbvOLD" is discouraged (47 steps).
Proof modification of "nfunidALT" is discouraged (33 steps).
Proof modification of "nfunidALT2" is discouraged (49 steps).
diff --git a/mmset.raw.html b/mmset.raw.html
index 830327ecd1..4f4828aa54 100644
--- a/mmset.raw.html
+++ b/mmset.raw.html
@@ -2022,7 +2022,7 @@
may be the same) as long as they don't conflict with any distinct variable
requirements imposed on ` A ` and ` B ` . We then would
follow the procedure of the above example. The description of theorem
-~ eqab goes into more detail and gives some
+~ eqabb goes into more detail and gives some
actual database examples where this translation takes place.
@@ -2229,7 +2229,7 @@
Commutative law for union ~ uncom
A basic relationship between class and wff
-variables ~ eqab
+variables ~ eqabb
Two ways of saying "is a set" ~ isset
diff --git a/nf.mm b/nf.mm
index e61dc9f55e..44ab51744e 100644
--- a/nf.mm
+++ b/nf.mm
@@ -20257,7 +20257,7 @@ of variable (class variable) that can substituted with expressions such as
a setvar variable ` x ` for a class variable: all sets are classes by
~ cvjust (but not necessarily vice-versa). For a full description of how
classes are introduced and how to recover the primitive language, see the
- discussion in Quine (and under ~ eqab for a quick overview).
+ discussion in Quine (and under ~ eqabb for a quick overview).
Because class variables can be substituted with compound expressions and
setvar variables cannot, it is often useful to convert a theorem
@@ -20343,7 +20343,7 @@ of logic but rather presupposes the Axiom of Extensionality (see Theorem
definition. This also makes some proofs shorter and probably easier to
read, without the constant switching between two kinds of equality.
- See also comments under ~ df-clab , ~ df-clel , and ~ eqab .
+ See also comments under ~ df-clab , ~ df-clel , and ~ eqabb .
In the form of ~ dfcleq , this is called the "axiom of extensionality"
by [Levy] p. 338, who treats the theory of classes as an extralogical
@@ -21346,7 +21346,7 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
$( Equality of a class variable and a class abstraction (also called a
class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the
relationship between expressions with class abstractions and expressions
- with class variables. Note that ~ abbi and its relatives are among
+ with class variables. Note that ~ abbib and its relatives are among
those useful for converting theorems with class variables to equivalent
theorems with wff variables, by first substituting a class abstraction
for each class variable.
@@ -21367,7 +21367,7 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
equivalent formulation cplem2 in set.mm. For more information on class
variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13.
(Contributed by NM, 5-Aug-1993.) $)
- eqab $p |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) ) $=
+ eqabb $p |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) ) $=
( vy cab wceq cv wcel wb wal ax-17 hbab1 cleqh abid bibi2i albii bitri )
CABEZFBGZCHZSRHZIZBJTAIZBJBDCRDGCHBKABDLMUBUCBUAATABNOPQ $.
$}
@@ -21376,8 +21376,8 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
$d x A $.
$( Equality of a class variable and a class abstraction. (Contributed by
NM, 20-Aug-1993.) $)
- eqabc $p |- ( { x | ph } = A <-> A. x ( ph <-> x e. A ) ) $=
- ( cab wceq cv wcel wb wal eqab eqcom bicom albii 3bitr4i ) CABDZEBFCGZAH
+ eqabcb $p |- ( { x | ph } = A <-> A. x ( ph <-> x e. A ) ) $=
+ ( cab wceq cv wcel wb wal eqabb eqcom bicom albii 3bitr4i ) CABDZEBFCGZAH
ZBIOCEAPHZBIABCJOCKRQBAPLMN $.
$}
@@ -21409,10 +21409,11 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
$d ph y $. $d ps y $. $d x y $.
$( Equivalent wff's correspond to equal class abstractions. (Contributed
by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) $)
- abbi $p |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) $=
- ( vy cab wceq wcel wal dfcleq nfsab1 nfbi nfv wsb df-clab sbequ12r syl5bb
- cv wb bibi12d cbval bitr2i ) ACEZBCEZFDQZUBGZUDUCGZRZDHABRZCHDUBUCIUGUHDC
- UEUFCACDJBCDJKUHDLUDCQFZUEAUFBUEACDMUIAADCNADCOPUFBCDMUIBBDCNBDCOPSTUA $.
+ abbib $p |- ( { x | ph } = { x | ps } <-> A. x ( ph <-> ps ) ) $=
+ ( vy cab wceq cv wcel wal dfcleq nfsab1 nfbi nfv weq wsb df-clab sbequ12r
+ wb syl5bb bibi12d cbval bitri ) ACEZBCEZFDGZUCHZUEUDHZRZDIABRZCIDUCUDJUHU
+ IDCUFUGCACDKBCDKLUIDMDCNZUFAUGBUFACDOUJAADCPADCQSUGBCDOUJBBDCPBDCQSTUAUB
+ $.
$}
${
@@ -21421,7 +21422,7 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
$( Equality of a class variable and a class abstraction (inference rule).
(Contributed by NM, 5-Aug-1993.) $)
abbi2i $p |- A = { x | ph } $=
- ( cab wceq cv wcel wb eqab mpgbir ) CABEFBGCHAIBABCJDK $.
+ ( cab wceq cv wcel wb eqabb mpgbir ) CABEFBGCHAIBABCJDK $.
$}
${
@@ -21429,7 +21430,7 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
$( Equivalent wff's yield equal class abstractions (inference rule).
(Contributed by NM, 5-Aug-1993.) $)
abbii $p |- { x | ph } = { x | ps } $=
- ( wb cab wceq abbi mpgbi ) ABEACFBCFGCABCHDI $.
+ ( cab wceq wb abbib mpgbir ) ACEBCEFABGCABCHDI $.
$( Theorem abbii is the congruence law for class abstraction. $)
$( $j congruence 'abbii'; $)
@@ -21442,7 +21443,7 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
(Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro,
7-Oct-2016.) $)
abbid $p |- ( ph -> { x | ps } = { x | ch } ) $=
- ( wb wal cab wceq alrimi abbi sylib ) ABCGZDHBDICDIJANDEFKBCDLM $.
+ ( wb wal cab wceq alrimi abbib sylibr ) ABCGZDHBDICDIJANDEFKBCDLM $.
$}
${
@@ -21460,7 +21461,7 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
$( Deduction from a wff to a class abstraction. (Contributed by NM,
9-Jul-1994.) $)
abbi2dv $p |- ( ph -> A = { x | ps } ) $=
- ( cv wcel wb wal cab wceq alrimiv eqab sylibr ) ACFDGBHZCIDBCJKAOCELBCDM
+ ( cv wcel wb wal cab wceq alrimiv eqabb sylibr ) ACFDGBHZCIDBCJKAOCELBCDM
N $.
$}
@@ -21470,8 +21471,8 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
$( Deduction from a wff to a class abstraction. (Contributed by NM,
9-Jul-1994.) $)
abbi1dv $p |- ( ph -> { x | ps } = A ) $=
- ( cv wcel wb wal cab wceq alrimiv eqabc sylibr ) ABCFDGHZCIBCJDKAOCELBCDM
- N $.
+ ( cv wcel wb wal cab wceq alrimiv eqabcb sylibr ) ABCFDGHZCIBCJDKAOCELBCD
+ MN $.
$}
${
@@ -21521,7 +21522,7 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
17-Jan-2006.) $)
clabel $p |- ( { x | ph } e. A <->
E. y ( y e. A /\ A. x ( x e. y <-> ph ) ) ) $=
- ( cab wcel cv wceq wa wex wb wal df-clel eqab anbi2ci exbii bitri ) ABEZ
+ ( cab wcel cv wceq wa wex wb wal df-clel eqabb anbi2ci exbii bitri ) ABEZ
DFCGZRHZSDFZIZCJUABGSFAKBLZIZCJCRDMUBUDCTUCUAABSNOPQ $.
$}
@@ -21873,7 +21874,7 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
(Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro,
7-Oct-2016.) $)
sbabel $p |- ( [ y / x ] { z | ph } e. A <-> { z | [ y / x ] ph } e. A ) $=
- ( vv cv cab wceq wcel wa wex wsb wb wal sbf eqab sbbii 3bitr4i sbex sban
+ ( vv cv cab wceq wcel wa wex wsb wb wal sbf eqabb sbbii 3bitr4i sbex sban
nfv sbrbis sbalv nfcri anbi12i bitri exbii df-clel ) GHZADIZJZUKEKZLZGMZB
CNZUKABCNZDIZJZUNLZGMZULEKZBCNUSEKUQUOBCNZGMVBUOGBCUAVDVAGVDUMBCNZUNBCNZL
VAUMUNBCUBVEUTVFUNDHUKKZAOZDPZBCNVGUROZDPVEUTVHVJBCDVGVGABCVGBCVGBUCQUDUE
@@ -24070,7 +24071,7 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
$( An "identity" law for restricted class abstraction. (Contributed by NM,
9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) $)
rabid2 $p |- ( A = { x e. A | ph } <-> A. x e. A ph ) $=
- ( cv wcel wa cab wceq wi wal crab eqab pm4.71 albii bitr4i df-rab eqeq2i
+ ( cv wcel wa cab wceq wi wal crab eqabb pm4.71 albii bitr4i df-rab eqeq2i
wral wb df-ral 3bitr4i ) CBDCEZAFZBGZHZUBAIZBJZCABCKZHABCRUEUBUCSZBJUGUCB
CLUFUIBUBAMNOUHUDCABCPQABCTUA $.
$}
@@ -24079,9 +24080,9 @@ atomic formula (class version of ~ elsb2 ). (Contributed by Jim
Closed theorem form of ~ rabbidva . (Contributed by NM, 25-Nov-2013.) $)
rabbi $p |- ( A. x e. A ( ps <-> ch )
<-> { x e. A | ps } = { x e. A | ch } ) $=
- ( cv wcel wa wb wal wceq wral crab abbi wi df-ral pm5.32 albii bitri df-rab
- cab eqeq12i 3bitr4i ) CEDFZAGZUCBGZHZCIZUDCTZUECTZJABHZCDKZACDLZBCDLZJUDUEC
- MUKUCUJNZCIUGUJCDOUNUFCUCABPQRULUHUMUIACDSBCDSUAUB $.
+ ( cv wcel wa cab wceq wb wal crab wral abbib df-rab eqeq12i wi df-ral albii
+ pm5.32 bitri 3bitr4ri ) CEDFZAGZCHZUCBGZCHZIUDUFJZCKZACDLZBCDLZIABJZCDMZUDU
+ FCNUJUEUKUGACDOBCDOPUMUCULQZCKUIULCDRUNUHCUCABTSUAUB $.
$( Swap with a membership relation in a restricted class abstraction.
(Contributed by NM, 4-Jul-2005.) $)
@@ -26843,7 +26844,7 @@ equiconsistent to Z (ZF in which ax-sep in set.mm replaces ax-rep in
(Contributed by NM, 7-Aug-1994.) $)
ru $p |- { x | x e/ x } e/ _V $=
( vy cv wnel cab cvv wcel wn wceq wex wb wal pm5.19 df-nel eleq12d notbid
- eleq1 id syl5bb mtbir bibi12d spv mto eqab nex isset mpbir ) ACZUHDZAEZF
+ eleq1 id syl5bb mtbir bibi12d spv mto eqabb nex isset mpbir ) ACZUHDZAEZF
DUJFGZHUKBCZUJIZBJUMBUMUHULGZUIKZALZUPULULGZUQHZKZUQMUOUSABUHULIZUNUQUIUR
UHULULQUIUHUHGZHUTURUHUHNUTVAUQUTUHULUHULUTRZVBOPSUAUBUCUIAULUDTUEBUJUFTU
JFNUG $.
@@ -27662,7 +27663,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
NM, 5-Nov-2005.) $)
sbcabel $p |- ( A e. V -> ( [. A / x ]. { y | ph } e. B <->
{ y | [. A / x ]. ph } e. B ) ) $=
- ( vw wcel cvv cab wsbc wb cv wceq wa wex wal eqab bitrd elex sbcexg sbcg
+ ( vw wcel cvv cab wsbc wb cv wceq wa wex wal eqabb bitrd elex sbcexg sbcg
sbcang sbcbii sbcalg sbcbig bibi1d albidv syl6bbr anbi12d df-clel 3bitr4g
syl5bb nfcri sbcgf exbidv syl ) DFIDJIZACKZEIZBDLZABDLZCKZEIZMDFUAUSHNZUT
OZVFEIZPZHQZBDLZVFVDOZVHPZHQZVBVEUSVKVIBDLZHQVNVIHBDJUBUSVOVMHUSVOVGBDLZV
@@ -27874,9 +27875,9 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
$( Composition law for chained substitutions into a class. (Contributed by
NM, 10-Nov-2005.) $)
csbco $p |- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B $=
- ( vz cv csb wcel wsbc cab df-csb eqabi sbcbii sbcco bitri abbii 3eqtr4i
- ) EFZABFZDGZHZBCIZEJRDHZACIZEJBCTGACDGUBUDEUBUCASIZBCIUDUAUEBCUEETAESDKLM
- UCABCNOPBECTKAECDKQ $.
+ ( vz cv csb wcel wsbc cab df-csb eqabi sbcbii sbcco bitri abbii 3eqtr4i )
+ EFZABFZDGZHZBCIZEJRDHZACIZEJBCTGACDGUBUDEUBUCASIZBCIUDUAUEBCUEETAESDKLMUC
+ ABCNOPBECTKAECDKQ $.
$}
${
@@ -28283,11 +28284,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) $)
csbnestgf $p |- ( ( A e. V /\ A. y F/_ x C ) ->
[_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C ) $=
- ( vz wcel wnfc wal wa cv csb wsbc cab cvv wceq elex df-csb eqabi wb nfcr
- sbcbii wnf alimi sbcnestgf sylan2 syl5bb abbidv sylan 3eqtr4g ) CFHZAEIZB
- JZKGLZBDEMZHZACNZGOZUOEHZBACDMZNZGOZACUPMBVAEMULCPHZUNUSVCQCFRVDUNKZURVBG
- URUTBDNZACNZVEVBUQVFACVFGUPBGDESTUCUNVDUTAUDZBJVGVBUAUMVHBAGEUBUEUTABCDPU
- FUGUHUIUJAGCUPSBGVAESUK $.
+ ( vz wcel wnfc wal wa cv csb wsbc cab cvv wceq elex df-csb eqabi wnf nfcr
+ sbcbii wb alimi sbcnestgf sylan2 syl5bb abbidv sylan 3eqtr4g ) CFHZAEIZBJ
+ ZKGLZBDEMZHZACNZGOZUOEHZBACDMZNZGOZACUPMBVAEMULCPHZUNUSVCQCFRVDUNKZURVBGU
+ RUTBDNZACNZVEVBUQVFACVFGUPBGDESTUCUNVDUTAUAZBJVGVBUDUMVHBAGEUBUEUTABCDPUF
+ UGUHUIUJAGCUPSBGVAESUK $.
$d x ph $.
$( Nest the composition of two substitutions. (Contributed by NM,
@@ -32674,8 +32675,8 @@ fewer connectives (but probably less intuitive to understand).
$( Subclass relationship for power class. (Contributed by NM,
21-Jun-2009.) $)
pwss $p |- ( ~P A C_ B <-> A. x ( x C_ A -> x e. B ) ) $=
- ( cpw wss cv wcel wi wal dfss2 df-pw eqabi imbi1i albii bitri ) BDZCEAFZ
- PGZQCGZHZAIQBEZSHZAIAPCJTUBARUASUAAPABKLMNO $.
+ ( cpw wss cv wcel wi wal dfss2 df-pw eqabi imbi1i albii bitri ) BDZCEAFZP
+ GZQCGZHZAIQBEZSHZAIAPCJTUBARUASUAAPABKLMNO $.
$}
@@ -33128,9 +33129,9 @@ fewer connectives (but probably less intuitive to understand).
abstraction is a singleton. (Contributed by Mario Carneiro,
14-Nov-2016.) $)
euabsn2 $p |- ( E! x ph <-> E. y { x | ph } = { y } ) $=
- ( weu cv wceq wb wal wex cab csn df-eu wcel eqabc elsn bibi2i albii bitri
- exbii bitr4i ) ABDABEZCEZFZGZBHZCIABJUBKZFZCIABCLUGUECUGAUAUFMZGZBHUEABUF
- NUIUDBUHUCABUBOPQRST $.
+ ( weu cv wceq wb wal wex cab csn df-eu wcel eqabcb elsn albii bitri exbii
+ bibi2i bitr4i ) ABDABEZCEZFZGZBHZCIABJUBKZFZCIABCLUGUECUGAUAUFMZGZBHUEABU
+ FNUIUDBUHUCABUBOSPQRT $.
$( Another way to express existential uniqueness of a wff: its class
abstraction is a singleton. (Contributed by NM, 22-Feb-2004.) $)
@@ -33769,8 +33770,8 @@ fewer connectives (but probably less intuitive to understand).
$( The singleton of a class is a subset of its power class. (Contributed
by NM, 5-Aug-1993.) $)
snsspw $p |- { A } C_ ~P A $=
- ( vx csn cpw cv wceq wss wcel eqimss elsn df-pw eqabi 3imtr4i ssriv ) BA
- CZADZBEZAFQAGZQOHQPHQAIBAJRBPBAKLMN $.
+ ( vx csn cpw cv wceq wss wcel eqimss elsn df-pw eqabi 3imtr4i ssriv ) BAC
+ ZADZBEZAFQAGZQOHQPHQAIBAJRBPBAKLMN $.
$}
${
@@ -36315,10 +36316,10 @@ Kuratowski ordered pairs (continued)
$( Cardinal one is a set. (Contributed by SF, 12-Jan-2015.) $)
1cex $p |- 1c e. _V $=
( vy vx vw vz c1c cvv wcel wel weq wb wal wex ax-1c cv isset bitri bibi2i
- wceq albii exbii csn cab df-1c eqeq2i eqab dfcleq df-sn eqabi mpbir ) E
- FGZABHZCAHZCDIZJZCKZDLZJZAKZBLZBADCMUJBNZERZBLUSBEOVAURBVAUKANZDNZUAZRZDL
- ZJZAKZURVAUTVFAUBZRVHEVIUTADUCUDVFAUTUEPVGUQAVFUPUKVEUODVEULCNVDGZJZCKUOC
- VBVDUFVKUNCVJUMULUMCVDCVCUGUHQSPTQSPTPUI $.
+ wceq albii exbii csn cab df-1c eqeq2i eqabb dfcleq df-sn eqabi mpbir ) EF
+ GZABHZCAHZCDIZJZCKZDLZJZAKZBLZBADCMUJBNZERZBLUSBEOVAURBVAUKANZDNZUAZRZDLZ
+ JZAKZURVAUTVFAUBZRVHEVIUTADUCUDVFAUTUEPVGUQAVFUPUKVEUODVEULCNVDGZJZCKUOCV
+ BVDUFVKUNCVJUMULUMCVDCVCUGUHQSPTQSPTPUI $.
$}
$( Equality theorem for unit power class. (Contributed by SF,
@@ -37382,11 +37383,11 @@ Kuratowski ordered pairs (continued)
elp6 $p |- ( A e. V -> ( A e. P6 B <-> A. x << x , { A } >> e. B ) ) $=
( vy wcel cp6 cvv csn cxpk wss cv copk wal wceq sneq wi vex albii bitri
sneqd xpkeq2d sseq1d df-p6 elab2g xpkssvvk ssrelk ax-mp opkelxpk biantrur
- wb wa df-sn eqabi 3bitr2i imbi1i snex opkeq2 eleq1d ceqsalv syl6bb ) BDF
- BCGZFHBIZIZJZCKZALZVCMZCFZANZHELZIZIZJZCKVFEBVBDVKBOZVNVECVOVMVDHVOVLVCVK
- BPUAUBUCECUDUEVFVGVKMZVEFZVPCFZQZENZANZVJVEHHJKVFWAUKHVDUFAEVECUGUHVTVIAV
- TVKVCOZVRQZENVIVSWCEVQWBVRVQVGHFZVKVDFZULWEWBVGVKHVDARZERUIWDWEWFUJWBEVDE
- VCUMUNUOUPSVRVIEVCBUQWBVPVHCVKVCVGURUSUTTSTVA $.
+ wb wa df-sn eqabi 3bitr2i imbi1i snex opkeq2 eleq1d ceqsalv syl6bb ) BDFB
+ CGZFHBIZIZJZCKZALZVCMZCFZANZHELZIZIZJZCKVFEBVBDVKBOZVNVECVOVMVDHVOVLVCVKB
+ PUAUBUCECUDUEVFVGVKMZVEFZVPCFZQZENZANZVJVEHHJKVFWAUKHVDUFAEVECUGUHVTVIAVT
+ VKVCOZVRQZENVIVSWCEVQWBVRVQVGHFZVKVDFZULWEWBVGVKHVDARZERUIWDWEWFUJWBEVDEV
+ CUMUNUOUPSVRVIEVCBUQWBVPVHCVKVCVGURUSUTTSTVA $.
$}
${
@@ -38092,11 +38093,11 @@ Kuratowski ordered pairs (continued)
SF, 20-Jan-2015.) $)
unipw1 $p |- U. ~P1 A = A $=
( vx vy vz cpw1 cuni cv wcel wel wa wex csn wceq eluni elpw1 anbi1i ancom
- wrex weq 3bitri r19.41v 3bitr4i exbii risset ceqsexv eqabi equcom rexbii
- snex eleq2 df-sn rexcom4 3bitr2ri eqriv ) BAEZFZABGZUPHBCIZCGZUOHZJZCKUSD
- GZLZMZURJZDARZCKZUQAHZCUQUONVAVFCUTURJVDDARZURJVAVFUTVIURDUSAOPURUTQVDURD
- AUAUBUCVHDBSZDARVECKZDARVGDUQAUDVKVJDAVKUQVCHZBDSZVJURVLCVCVBUIUSVCUQUJUE
- VMBVCBVBUKUFBDUGTUHVEDCAULUMTUN $.
+ wrex weq 3bitri r19.41v exbii risset snex eleq2 df-sn eqabi equcom rexbii
+ 3bitr4i ceqsexv rexcom4 3bitr2ri eqriv ) BAEZFZABGZUPHBCIZCGZUOHZJZCKUSDG
+ ZLZMZURJZDARZCKZUQAHZCUQUONVAVFCUTURJVDDARZURJVAVFUTVIURDUSAOPURUTQVDURDA
+ UAUJUBVHDBSZDARVECKZDARVGDUQAUCVKVJDAVKUQVCHZBDSZVJURVLCVCVBUDUSVCUQUEUKV
+ MBVCBVBUFUGBDUHTUIVEDCAULUMTUN $.
$}
$( Biconditional existence for unit power class. (Contributed by SF,
@@ -38201,9 +38202,9 @@ Kuratowski ordered pairs (continued)
$( Alternate definition of existential uniqueness in terms of abstraction.
(Contributed by SF, 29-Jan-2015.) $)
dfeu2 $p |- ( E! x ph <-> { x | ph } e. 1c ) $=
- ( vy weq wb wal wex cab cv csn wceq weu c1c wcel abbi df-sn eqeq2i bitr4i
- exbii df-eu el1c 3bitr4i ) ABCDZEBFZCGABHZCIZJZKZCGABLUEMNUDUHCUDUEUCBHZK
- UHAUCBOUGUIUEBUFPQRSABCTCUEUAUB $.
+ ( vy weq wb wal wex cab cv csn wceq weu c1c wcel df-sn eqeq2i abbib exbii
+ bitr2i df-eu el1c 3bitr4i ) ABCDZEBFZCGABHZCIZJZKZCGABLUEMNUDUHCUHUEUCBHZ
+ KUDUGUIUEBUFOPAUCBQSRABCTCUEUAUB $.
$}
$( If there is a unique object satisfying a property ` ph ` , then the set of
@@ -38275,9 +38276,9 @@ Definite description binder (inverted iota)
$( Alternate definition for descriptions. Definition 8.18 in [Quine]
p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) $)
dfiota2 $p |- ( iota x ph ) = U. { y | A. x ( ph <-> x = y ) } $=
- ( cio cab cv csn wceq cuni wb wal df-iota df-sn eqeq2i abbi bitr4i unieqi
- abbii eqtri ) ABDABEZCFZGZHZCEZIABFUAHZJBKZCEZIABCLUDUGUCUFCUCTUEBEZHUFUB
- UHTBUAMNAUEBOPRQS $.
+ ( cio cab cv csn wceq cuni weq wal df-iota df-sn eqeq2i abbib bitri abbii
+ wb unieqi eqtri ) ABDABEZCFZGZHZCEZIABCJZRBKZCEZIABCLUEUHUDUGCUDUAUFBEZHU
+ GUCUIUABUBMNAUFBOPQST $.
$}
${
@@ -38363,16 +38364,17 @@ Definite description binder (inverted iota)
$( Equivalence theorem for descriptions. (Contributed by Andrew Salmon,
30-Jun-2011.) $)
iotabi $p |- ( A. x ( ph <-> ps ) -> ( iota x ph ) = ( iota x ps ) ) $=
- ( vz wb wal cab cv csn wceq cuni abbi biimpi eqeq1d abbidv unieqd df-iota
- cio 3eqtr4g ) ABECFZACGZDHIZJZDGZKBCGZUBJZDGZKACRBCRTUDUGTUCUFDTUAUEUBTUA
- UEJABCLMNOPACDQBCDQS $.
+ ( vz wb wal cab cv csn wceq cuni cio biimpri eqeq1d abbidv unieqd df-iota
+ abbib 3eqtr4g ) ABECFZACGZDHIZJZDGZKBCGZUBJZDGZKACLBCLTUDUGTUCUFDTUAUEUBU
+ AUEJTABCRMNOPACDQBCDQS $.
$( Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma
for the fundamental property of iota. (Contributed by Andrew Salmon,
11-Jul-2011.) $)
uniabio $p |- ( A. x ( ph <-> x = y ) -> U. { x | ph } = y ) $=
- ( cv wceq wb wal cab cuni csn abbi biimpi df-sn syl6eqr unieqd vex syl6eq
- unisn ) ABDCDZEZFBGZABHZISJZISUAUBUCUAUBTBHZUCUAUBUDEATBKLBSMNOSCPRQ $.
+ ( weq wb wal cab cuni cv csn abbib biimpri df-sn syl6eqr unieqd vex unisn
+ wceq syl6eq ) ABCDZEBFZABGZHCIZJZHUCUAUBUDUAUBTBGZUDUBUERUAATBKLBUCMNOUCC
+ PQS $.
$( Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property
of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) $)
@@ -38406,11 +38408,11 @@ Definite description binder (inverted iota)
isn't exactly one ` x ` that satisfies ` ph ` . (Contributed by Andrew
Salmon, 11-Jul-2011.) $)
iotanul $p |- ( -. E! x ph -> ( iota x ph ) = (/) ) $=
- ( vz weu cv wceq wb wal wex cio c0 df-eu wn cuni dfiota2 alnex ax-1 eqidd
- cab impbid1 con2bid alimi abbi dfnul2 syl6eqr sylbir unieqd syl6eq syl5eq
- sylib uni0 sylnbi ) ABDABECEZFGBHZCIZABJZKFABCLUOMZUPUNCSZNZKABCOUQUSKNKU
- QURKUQUNMZCHZURKFUNCPVAURUMUMFZMZCSZKVAUNVCGZCHURVDFUTVECUTVBUNUTVBUTUTVB
- QUTUMRTUAUBUNVCCUCUJCUDUEUFUGUKUHUIUL $.
+ ( vz weu weq wb wal wex cio c0 wceq df-eu wn cab cuni dfiota2 alnex eqidd
+ ax-1 cv impbid1 con2bid sylibr dfnul2 syl6eqr sylbir unieqd syl6eq syl5eq
+ alimi abbib uni0 sylnbi ) ABDABCEFBGZCHZABIZJKABCLUOMZUPUNCNZOZJABCPUQUSJ
+ OJUQURJUQUNMZCGZURJKUNCQVAURCCEZMZCNZJVAUNVCFZCGURVDKUTVECUTVBUNUTVBUTUTV
+ BSUTCTRUAUBUJUNVCCUKUCCUDUEUFUGULUHUIUM $.
$( The ` iota ` class is a subset of the union of all elements satisfying
` ph ` . (Contributed by Mario Carneiro, 24-Dec-2016.) $)
@@ -39754,7 +39756,7 @@ Definite description binder (inverted iota)
wn df-rex 3bitr4i opkeq1 eleq1d ceqsexv elpw131c 19.41v excom wb elpw161c
wel elsymdif otkelins3k vex elssetk otkelins2k elpw181c ndisjrelk elcompl
bitri notbii df-ne con2bii elpw1111c orbi12i elun bibi12i wal dfcleq alex
- wo anbi12i rexcom df-addc eqeq2i eqab opkelimagek dfaddc2 addcex addceq1
+ wo anbi12i rexcom df-addc eqeq2i eqabb opkelimagek dfaddc2 addcex addceq1
eqeq2d rexbii opkelxpk mpbiran2 elsnc anbi2i syl6bb pm5.32i 2exbii bitr3i
eldif ancom abbi2i eqtr4i vvex xpkex ssetkex ins3kex ins2kex pw1ex imakex
inex complex symdifex 1cex unex addcexlem imagekex nncex difex eqeltri )
@@ -40076,7 +40078,7 @@ Definite description binder (inverted iota)
cins2k csik cins3k csymdif c1c cimak wss ccompl cpw opkex elimak elpw121c
anbi1i 19.41v bitr4i exbii df-rex excom 3bitr4i opkeq1 ceqsexv otkelins2k
eleq1d elsymdif vex elssetk bitri otkelins3k opksnelsik opkelssetkg mp2an
- wrex bibi12i notbii elcompl cab wal df-pw eqeq2i eqab alex ) AGZBHZIUAZI
+ wrex bibi12i notbii elcompl cab wal df-pw eqeq2i eqabb alex ) AGZBHZIUAZI
UBZUCZUDZUEJJZUFZKZLEMZBKZWKAUGZNZLZEOZLZWCWIUHKBAUIZPZWJWPWJFMZWCHZWGKZF
WHVLZWTWKGZGZGZPZXBQZFOZEOZWPFWGWHWCWBBUJZUKWTWHKZXBQZFOXHEOZFOXCXJXMXNFX
MXGEOZXBQXNXLXOXBEWTULUMXGXBEUNUOUPXBFWHUQXHEFURUSXIWOEXIXFWCHZWGKZXPWDKZ
@@ -40989,7 +40991,7 @@ Definite description binder (inverted iota)
wral elin wel wal opkex elimak elpw121c anbi1i 19.41v bitr4i df-rex excom
wb opkeq1 ceqsexv elsymdif otkelins3k elssetk bitri otkelins2k opksnelsik
eleq1d elpw141c ndisjrelk notbii elcompl con2bii elpw171c orbi12i bibi12i
- df-ne elun dfcleq alex anbi12i rexcom df-addc eqeq2i eqab opkelxpk elsnc
+ df-ne elun dfcleq alex anbi12i rexcom df-addc eqeq2i eqabb opkelxpk elsnc
weq elpw11c opkelcnvk opkelimagek dfaddc2 addcex addceq1 eqeq2d opkelidkg
mpbiran2 eldif mp2an equcom 1cex eqeq2 eqeq1 notbid anbi12d annim ssetkex
rexbii ins3kex ins2kex inex pw1ex imakex complex sikex unex symdifex vvex
@@ -41210,7 +41212,7 @@ Definite description binder (inverted iota)
cab cpw1 cxpk cin ccompl cins3k cins2k cv cun csymdif csik cdif cuni wceq
cimak wrex wral snex opkeq1 eleq1d ceqsexv elin vex elssetk eldif elcompl
wi elimak el1c anbi1i 19.41v bitr4i df-rex excom opkelxpk mpbiran2 elequ2
- snelpw1 elab anbi12i eluni xchbinx wb wal eqab opkex elpw121c otkelins3k
+ snelpw1 elab anbi12i eluni xchbinx wb wal eqabb opkex elpw121c otkelins3k
df-clel opksnelsik elsymdif bitri otkelins2k alex dfcleq wo elsnc orbi12i
sneqb elun bibi12i 3bitr4ri notbii annim dfral2 abbi2i ssetkex setswithex
weq pw1ex vvex xpkex inex 1cex imakex complex ins3kex unex symdifex sikex
@@ -41460,7 +41462,7 @@ Ins3_k SI_k ( ( ~P 1c X._k _V ) \
cin wsfin opkelxpk wrex opkex elimak elpw131c anbi1i 19.41v bitr4i df-rex
excom opkeq1 eleq1d ceqsexv elin elpw121c otkelins3k opksnelsik eqpw1relk
w3a vex otkelins2k elssetk bitri anbi12i df-clel wel elsymdif opkelssetkg
- wss wb wal wn mp2an bibi12i notbii elcompl alex df-pw eqeq2i eqab df-3an
+ wss wb wal wn mp2an bibi12i notbii elcompl alex df-pw eqeq2i eqabb df-3an
cab df-sfin ) ABIZJJUAZKZWSUBUCUDUALUEZLUFZUGZUHZUBUIUIZUIZUJUKZUFZUEZLUG
ZUNZXFUJZUEZXEXFUJZULZUFZUEZXKUNZXFUJZUGZUNZXGUJZKZMZAJKZBJKZEUMZUIZAKZYH
UCZBKZMZENZVNZWSWTYCUNKABUOYEYFYGMZYNMYOXAYPYDYNABJJCDUPYDFUMZWSIZYBKZFXG
@@ -41689,7 +41691,7 @@ Ins3_k SI_k ( ( ~P 1c X._k _V ) \
wral wel eleq1d ceqsexv elin opksnelsik elssetk opkelxpk mpbiran2 snelpw1
eldif otkelins2k opkelcnvk eqtfinrelk opkex elimak elpw121c anbi1i 19.41v
bitr4i df-rex excom wb elsymdif otkelins3k anbi12i bibi12i notbii elcompl
- elpw eqab df-clel elpw11c tfinex clel3 annim dfral2 abbi2i ssetkex sikex
+ elpw eqabb df-clel elpw11c tfinex clel3 annim dfral2 abbi2i ssetkex sikex
wal alex nncex pwex pw1ex vvex xpkex tfinrelkex ins2kex ins3kex inex 1cex
cnvkex imakex symdifex complex difex uni1ex eqeltrri ) HUAZUBUCZUDZUEUFZU
AZUGIZIZYMUFHUHZHUIUJUBUEUFYHUHZUKUCUEUFHUJZYPULUKUDZUDZUDZJUMUAUJYOUNYSJ
@@ -42743,10 +42745,10 @@ Ins3_k SI_k ( ( ~P 1c X._k _V ) \
phi011lem1 $p |- ( ( Phi A u. { 0c } ) = ( Phi B u. { 0c } ) ->
Phi A C_ Phi B ) $=
( vz cphi c0c csn wceq cv wcel wn ssun1 sseli eleq2 syl5ib 0cnelphi eleq1
- cun wi mtbiri wo con2i a1i elun df-sn eqabi orbi2i bitri biimpi ord ee22
- orcomd ssrdv ) ADZEFZQZBDZUNQZGZCUMUPURCHZUMIZUSUQIZUSEGZJZUSUPIZUTUSUOIU
- RVAUMUOUSUMUNKLUOUQUSMNUTVCRURVBUTVBUTEUMIAOUSEUMPSUAUBVAVBVDVAVDVBVAVDVB
- TZVAVDUSUNIZTVEUSUPUNUCVFVBVDVBCUNCEUDUEUFUGUHUKUIUJUL $.
+ cun wi mtbiri wo con2i a1i elun df-sn eqabi orbi2i biimpi orcomd ord ee22
+ bitri ssrdv ) ADZEFZQZBDZUNQZGZCUMUPURCHZUMIZUSUQIZUSEGZJZUSUPIZUTUSUOIUR
+ VAUMUOUSUMUNKLUOUQUSMNUTVCRURVBUTVBUTEUMIAOUSEUMPSUAUBVAVBVDVAVDVBVAVDVBT
+ ZVAVDUSUNIZTVEUSUPUNUCVFVBVDVBCUNCEUDUEUFUKUGUHUIUJUL $.
$}
$( ` ( Phi A u. { 0c } ) ` is one-to-one. Theorem X.2.4 of [Rosser] p. 282.
@@ -42961,10 +42963,10 @@ Ins3_k SI_k ( ( ~P 1c X._k _V ) \
phidisjnn $p |- ( ( A i^i Nn ) = (/) -> Phi A = A ) $=
( vx vy cnnc cin c0 wceq cv wcel c1c cplc cif wrex wb wal cphi wa syl6bbr
weq wn wral disj biimpi r19.21bi iffalse syl eqeq2d equcom risset alrimiv
- rexbidva cab df-phi eqeq1i eqabc bitri sylibr ) ADEFGZBHZCHZDIZUTJKZUTLZG
- ZCAMZUSAIZNZBOZAPZAGZURVGBURVECBSZCAMVFURVDVKCAURUTAIQZVDBCSVKVLVCUTUSVLV
- ATZVCUTGURVMCAURVMCAUACADUBUCUDVAVBUTUEUFUGCBUHRUKCUSAUIRUJVJVEBULZAGVHVI
- VNACBAUMUNVEBAUOUPUQ $.
+ rexbidva cab df-phi eqeq1i eqabcb bitri sylibr ) ADEFGZBHZCHZDIZUTJKZUTLZ
+ GZCAMZUSAIZNZBOZAPZAGZURVGBURVECBSZCAMVFURVDVKCAURUTAIQZVDBCSVKVLVCUTUSVL
+ VATZVCUTGURVMCAURVMCAUACADUBUCUDVAVBUTUEUFUGCBUHRUKCUSAUIRUJVJVEBULZAGVHV
+ IVNACBAUMUNVEBAUOUPUQ $.
$}
${
@@ -46413,7 +46415,7 @@ We use their notation ("onto" under the arrow). For alternate
dmopab3 $p |- ( A. x e. A E. y ph <->
dom { <. x , y >. | ( x e. A /\ ph ) } = A ) $=
( wex wral cv wcel wi wal wa wb copab cdm wceq df-ral pm4.71 albii dmopab
- cab 19.42v abbii eqtri eqeq1i eqcom eqab 3bitr2ri 3bitri ) ACEZBDFBGDHZU
+ cab 19.42v abbii eqtri eqeq1i eqcom eqabb 3bitr2ri 3bitri ) ACEZBDFBGDHZU
IIZBJUJUJUIKZLZBJZUJAKZBCMNZDOZUIBDPUKUMBUJUIQRUQULBTZDODUROUNUPURDUPUOCE
ZBTURUOBCSUSULBUJACUAUBUCUDDURUEULBDUFUGUH $.
$}
@@ -46449,11 +46451,11 @@ We use their notation ("onto" under the arrow). For alternate
$( An empty domain implies an empty range. (Contributed by set.mm
contributors, 21-May-1998.) $)
dm0rn0 $p |- ( dom A = (/) <-> ran A = (/) ) $=
- ( vx vy cv wbr wex cab c0 wceq wcel wb wal alnex noel albii eqabc 3bitr4i
- wn nbn eqeq1i cdm crn excom xchbinx bitr4i 3bitr3i dfdm2 dfrn2 ) BDZCDZAE
- ZCFZBGZHIZUKBFZCGZHIZAUAZHIAUBZHIULUIHJZKZBLZUOUJHJZKZCLZUNUQULRZBLZUORZC
- LZVBVEVGUOCFZRVIVGULBFVJULBMUKBCUCUDUOCMUEVFVABUTULUINSOVHVDCVCUOUJNSOUFU
- LBHPUOCHPQURUMHBCAUGTUSUPHBCAUHTQ $.
+ ( vx vy cv wbr wex cab c0 wceq wcel wb wal wn alnex noel nbn albii eqabcb
+ 3bitr4i eqeq1i cdm crn excom xchbinx bitr4i 3bitr3i dfdm2 dfrn2 ) BDZCDZA
+ EZCFZBGZHIZUKBFZCGZHIZAUAZHIAUBZHIULUIHJZKZBLZUOUJHJZKZCLZUNUQULMZBLZUOMZ
+ CLZVBVEVGUOCFZMVIVGULBFVJULBNUKBCUCUDUOCNUEVFVABUTULUIOPQVHVDCVCUOUJOPQUF
+ ULBHRUOCHRSURUMHBCAUGTUSUPHBCAUHTS $.
$( A class is empty iff its domain is empty. (Contributed by set.mm
contributors, 15-Sep-2004.) (Revised by Scott Fenton, 17-Apr-2021.) $)
@@ -50336,11 +50338,11 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
E. x e. B ( F ` x ) = C ) ) $=
( vy wfn wss wa cima wcel cv cfv wceq wrex cvv anim2i eleq1 wb wi rexbidv
elex fvex mpbii rexlimivw eqeq2 bibi12d imbi2d wfun cdm fnfun adantr fndm
- cab sseq2d biimpar dfimafn syl2anc eqabd vtoclg impcom pm5.21nd ) EBGZCB
- HZIZDECJZKZALZEMZDNZACOZVEDPKZIVGVLVEDVFUBQVKVLVEVJVLACVJVIPKVLVHEUCVIDPR
- UDUEQVLVEVGVKSZVEFLZVFKZVIVNNZACOZSZTVEVMTFDPVNDNZVRVMVEVSVOVGVQVKVNDVFRV
- SVPVJACVNDVIUFUAUGUHVEVQFVFVEEUIZCEUJZHZVFVQFUNNVCVTVDBEUKULVCWBVDVCWABCB
- EUMUOUPAFCEUQURUSUTVAVB $.
+ cab sseq2d biimpar dfimafn syl2anc eqabd vtoclg impcom pm5.21nd ) EBGZCBH
+ ZIZDECJZKZALZEMZDNZACOZVEDPKZIVGVLVEDVFUBQVKVLVEVJVLACVJVIPKVLVHEUCVIDPRU
+ DUEQVLVEVGVKSZVEFLZVFKZVIVNNZACOZSZTVEVMTFDPVNDNZVRVMVEVSVOVGVQVKVNDVFRVS
+ VPVJACVNDVIUFUAUGUHVEVQFVFVEEUIZCEUJZHZVFVQFUNNVCVTVDBEUKULVCWBVDVCWABCBE
+ UMUOUPAFCEUQURUSUTVAVB $.
$}
$( Membership in the preimage of a singleton, under a function. (Contributed
@@ -50889,11 +50891,11 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
A. y e. B E. x e. A y = ( F ` x ) ) ) $=
( wfo wf crn wceq wa cv cfv wrex wral dffo2 cab wb wcel wal wi wfn fnrnfv
ffn eqeq1d simpr ffvelrn adantr eqeltrd exp31 rexlimdv biantrurd syl6rbbr
- syl dfbi2 albidv eqabc df-ral 3bitr4g bitrd pm5.32i bitri ) CDEFCDEGZEHZD
- IZJVBBKZAKZELZIZACMZBDNZJCDEOVBVDVJVBVDVIBPZDIZVJVBECUAZVDVLQCDEUCVMVCVKD
- ABCEUBUDUMVBVIVEDRZQZBSVNVITZBSVLVJVBVOVPBVBVPVIVNTZVPJVOVBVQVPVBVHVNACVB
- VFCRZVHVNVBVRJZVHJVEVGDVSVHUEVSVGDRVHCDVFEUFUGUHUIUJUKVIVNUNULUOVIBDUPVIB
- DUQURUSUTVA $.
+ syl dfbi2 albidv eqabcb df-ral 3bitr4g bitrd pm5.32i bitri ) CDEFCDEGZEHZ
+ DIZJVBBKZAKZELZIZACMZBDNZJCDEOVBVDVJVBVDVIBPZDIZVJVBECUAZVDVLQCDEUCVMVCVK
+ DABCEUBUDUMVBVIVEDRZQZBSVNVITZBSVLVJVBVOVPBVBVPVIVNTZVPJVOVBVQVPVBVHVNACV
+ BVFCRZVHVNVBVRJZVHJVEVGDVSVHUEVSVGDRVHCDVFEUFUGUHUIUJUKVIVNUNULUOVIBDUPVI
+ BDUQURUSUTVA $.
$( Alternate definition of an onto mapping. (Contributed by set.mm
contributors, 20-Mar-2007.) $)
@@ -54206,14 +54208,14 @@ result of an operator (deduction version). (Contributed by Paul
` A ` . (Contributed by Mario Carneiro, 13-Feb-2015.) $)
fvmptss $p |- ( A. x e. A B C_ C -> ( F ` D ) C_ C ) $=
( vy wss wcel cfv cv wi wceq fveq2 sseq1d imbi2d nfcv wa c0 dmmptss sseli
- wral cdm nfra1 cmpt nfmpt1 nfcxfr nffv nfss nfim cvv dmmpt reqabi fvmpt2
- eqimss syl sylbi ndmfv 0ss a1i eqsstrd pm2.61i rsp impcom syl5ss vtoclgaf
- wn ex vtoclga sylan2 adantl pm2.61dan ) CDIZABUCZEFUDZJZEFKZDIZVQVOEBJZVS
- VPBEABCFGUAUBVTVOVSVOHLZFKZDIZMZVOVSMHEBWAENZWCVSVOWEWBVRDWAEFOPQVOALZFKZ
- DIZMWDAWABAWARZVOWCAVNABUEAWBDAWAFAFABCUFGABCUGUHWIUIADRUJUKWFWANZWHWCVOW
- JWGWBDWFWAFOPQWFBJZVOWHWKVOSWGCDWFVPJZWGCIZWLWKCULJZSZWMWNAVPBABCFGUMUNWO
- WGCNWMABCULFGUOWGCUPUQURWLVHZWGTCWFFUSTCIWPCUTVAVBVCVOWKVNVNABVDVEVFVIVGV
- JVEVKVOVQVHZSZVRTDWQVRTNVOEFUSVLTDIWRDUTVAVBVM $.
+ wral cdm nfra1 cmpt nfmpt1 nfcxfr nffv nfss nfim cvv reqabi fvmpt2 eqimss
+ dmmpt syl sylbi wn ndmfv 0ss a1i eqsstrd pm2.61i impcom syl5ss ex vtoclga
+ rsp vtoclgaf sylan2 adantl pm2.61dan ) CDIZABUCZEFUDZJZEFKZDIZVQVOEBJZVSV
+ PBEABCFGUAUBVTVOVSVOHLZFKZDIZMZVOVSMHEBWAENZWCVSVOWEWBVRDWAEFOPQVOALZFKZD
+ IZMWDAWABAWARZVOWCAVNABUEAWBDAWAFAFABCUFGABCUGUHWIUIADRUJUKWFWANZWHWCVOWJ
+ WGWBDWFWAFOPQWFBJZVOWHWKVOSWGCDWFVPJZWGCIZWLWKCULJZSZWMWNAVPBABCFGUPUMWOW
+ GCNWMABCULFGUNWGCUOUQURWLUSZWGTCWFFUTTCIWPCVAVBVCVDVOWKVNVNABVIVEVFVGVJVH
+ VEVKVOVQUSZSZVRTDWQVRTNVOEFUTVLTDIWRDVAVBVCVM $.
$}
@@ -55972,16 +55974,16 @@ result of an operator (deduction version). (Contributed by Paul
9-Mar-2015.) $)
fvfullfunlem3 $p |- ( A e. dom ( ( _I o. F ) \ ( ~ _I o. F ) ) ->
( ( ( _I o. F ) \ ( ~ _I o. F ) ) ` A ) = ( F ` A ) ) $=
- ( vx vy vz cid ccom wcel cfv wss wceq cv wbr wal weu fvfullfunlem1 eqabi
- wa brres cvv ccompl cdif cdm cres wfun weq wi dffun2 anbi2i bitri adantrl
- tz6.12-1 adantl eqtr3d adantlr syl2anb gen2 cxp cin fvfullfunlem2 crn ssv
- mpgbir ssdmrn xpss2 ax-mp sstri ssini df-res sseqtr4i funssfv mp3an12
- fvres ) AFBGFUABGUBZUCZHZABVOUDZIZAVNIZABIVQUEZVNVQJVPVRVSKVTCLZDLZVQMZWA
- ELZVQMZRDEUFZUGZENDNCCDEVQUHWGDEWCWAWBBMZWAWDBMZEOZRZWIWHDOZRZWFWEWCWHWAV
- OHZRWKWAWBBVOSWNWJWHWJCVOCEBPQUIUJWEWIWNRWMWAWDBVOSWNWLWIWLCVOCDBPQUIUJWH
- WMWFWJWHWMRWABIZWBWDWHWLWOWBKWIDWAWBBULUKWMWOWDKWHDWAWDBULUMUNUOUPUQVCVNB
- VOTURZUSVQVNBWPBUTVNVOVNVAZURZWPVNVDWQTJWRWPJWQVBWQTVOVEVFVGVHBVOVIVJAVQV
- NVKVLAVOBVMUN $.
+ ( vx vy vz cid ccom wcel cfv wss wceq cv wbr wa brres fvfullfunlem1 eqabi
+ wal weu cvv ccompl cdif cdm cres wfun weq wi dffun2 anbi2i bitri tz6.12-1
+ adantrl adantl eqtr3d adantlr syl2anb mpgbir cxp cin fvfullfunlem2 ssdmrn
+ gen2 crn xpss2 ax-mp sstri ssini df-res sseqtr4i funssfv mp3an12 fvres
+ ssv ) AFBGFUABGUBZUCZHZABVOUDZIZAVNIZABIVQUEZVNVQJVPVRVSKVTCLZDLZVQMZWAEL
+ ZVQMZNDEUFZUGZERDRCCDEVQUHWGDEWCWAWBBMZWAWDBMZESZNZWIWHDSZNZWFWEWCWHWAVOH
+ ZNWKWAWBBVOOWNWJWHWJCVOCEBPQUIUJWEWIWNNWMWAWDBVOOWNWLWIWLCVOCDBPQUIUJWHWM
+ WFWJWHWMNWABIZWBWDWHWLWOWBKWIDWAWBBUKULWMWOWDKWHDWAWDBUKUMUNUOUPVBUQVNBVO
+ TURZUSVQVNBWPBUTVNVOVNVCZURZWPVNVAWQTJWRWPJWQVMWQTVOVDVEVFVGBVOVHVIAVQVNV
+ JVKAVOBVLUN $.
$}
${
@@ -55992,13 +55994,13 @@ result of an operator (deduction version). (Contributed by Paul
( vx vy cvv wcel cfv wceq cv fveq2 cid ccom ccompl c0 wfn wa mp3an12 mpan
0ex eqtr4d cfullfun eqeq12d cdm csn cxp cun df-fullfun fveq1i cin incompl
cdif wfun fnfullfunlem2 funfn fnconstg ax-mp fvun1 fvfullfunlem3 eqtrd wn
- mpbi vex elcompl sylbir wbr fvfullfunlem1 eqabi tz6.12-2 sylnbi fvconst2
- fvun2 weu pm2.61i eqtri vtoclg fvprc ) AEFZABUAZGZABGZHZCIZVRGZWBBGZHWACA
- EWBAHWCVSWDVTWBAVRJWBABJUBWCWBKBLKMBLUKZWEUCZMZNUDUEZUFZGZWDWBVRWIBUGUHWB
- WFFZWJWDHWKWJWBWEGZWDWFWGUINHZWKWJWLHZWFUJZWEWFOZWHWGOZWMWKPWNWEULWPBUMWE
- UNVAZNEFWQSWGNEUOUPZWFWGWEWHWBUQQRWBBURUSWKUTZWJWBWHGZWDWTWBWGFZWJXAHZWBW
- FCVBVCZWMXBXCWOWPWQWMXBPXCWRWSWFWGWEWHWBVKQRVDWTWDNXAWKWBDIBVEDVLZWDNHXEC
- WFCDBVFVGDWBBVHVIWTXBXANHXDWGNWBSVJVDTTVMVNVOVQUTVSNVTAVRVPABVPTVM $.
+ mpbi vex elcompl fvun2 sylbir wbr weu fvfullfunlem1 eqabi tz6.12-2 sylnbi
+ fvconst2 pm2.61i eqtri vtoclg fvprc ) AEFZABUAZGZABGZHZCIZVRGZWBBGZHWACAE
+ WBAHWCVSWDVTWBAVRJWBABJUBWCWBKBLKMBLUKZWEUCZMZNUDUEZUFZGZWDWBVRWIBUGUHWBW
+ FFZWJWDHWKWJWBWEGZWDWFWGUINHZWKWJWLHZWFUJZWEWFOZWHWGOZWMWKPWNWEULWPBUMWEU
+ NVAZNEFWQSWGNEUOUPZWFWGWEWHWBUQQRWBBURUSWKUTZWJWBWHGZWDWTWBWGFZWJXAHZWBWF
+ CVBVCZWMXBXCWOWPWQWMXBPXCWRWSWFWGWEWHWBVDQRVEWTWDNXAWKWBDIBVFDVGZWDNHXECW
+ FCDBVHVIDWBBVJVKWTXBXANHXDWGNWBSVLVETTVMVNVOVQUTVSNVTAVRVPABVPTVM $.
$}
$( Binary relationship of the full function operation. (Contributed by SF,
@@ -57812,12 +57814,12 @@ the first case of his notation (simple exponentiation) and subscript it
pmvalg $p |- ( ( A e. C /\ B e. D ) ->
( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } ) $=
( vx vy wcel cvv cpm cv cxp cpw crab wceq elex wa cab pweqd biidd co wfun
- wss df-rab ancom df-pw eqabi anbi2i bitri abbii eqtri syl5eqel rabeqbidv
- pmex ancoms xpeq2 xpeq1 df-pm ovmpt2g mpd3an3 syl2an ) ACHAIHZBIHZABJUAEK
- ZUBZEBALZMZNZOZBDHACPBDPVBVCVHIHVIVBVCQVHVEVDVFUCZQZERZIVHVDVGHZVEQZERVLV
- EEVGUDVNVKEVNVEVMQVKVMVEUEVMVJVEVJEVGEVFUFUGUHUIUJUKVCVBVLIHBAIIEUNUOULFG
- ABIIVEEGKZFKZLZMZNVHJVEEVOALZMZNIVPAOZVEVEEVRVTWAVQVSVPAVOUPSWAVETUMVOBOZ
- VEVEEVTVGWBVSVFVOBAUQSWBVETUMFGEURUSUTVA $.
+ wss df-rab ancom df-pw eqabi anbi2i bitri abbii eqtri pmex syl5eqel xpeq2
+ ancoms rabeqbidv xpeq1 df-pm ovmpt2g mpd3an3 syl2an ) ACHAIHZBIHZABJUAEKZ
+ UBZEBALZMZNZOZBDHACPBDPVBVCVHIHVIVBVCQVHVEVDVFUCZQZERZIVHVDVGHZVEQZERVLVE
+ EVGUDVNVKEVNVEVMQVKVMVEUEVMVJVEVJEVGEVFUFUGUHUIUJUKVCVBVLIHBAIIEULUOUMFGA
+ BIIVEEGKZFKZLZMZNVHJVEEVOALZMZNIVPAOZVEVEEVRVTWAVQVSVPAVOUNSWAVETUPVOBOZV
+ EVEEVTVGWBVSVFVOBAUQSWBVETUPFGEURUSUTVA $.
$}
${
@@ -58716,15 +58718,15 @@ the first case of his notation (simple exponentiation) and subscript it
enpw1pw $p |- ~P1 ~P A ~~ ~P ~P1 A $=
( vy vx vz cpw cpw1 cpw1fn wf1o wbr c1c wss ax-mp wceq cv wrex wa wex vex
wcel cres cen cima wf1 pw1fnf1o f1of1 pw1ss1c f1ores mp2an wb df-ima elpw
- cab sspw1 df-rex df-pw eqabi anbi1i exbii bitr2i 3bitri csn elpw1 bitr4i
- r19.41v rexcom4 snex breq1 ceqsexv bitri rexbii bitr3i abbi2i eqtr4i mpbi
- brpw1fn f1oeq3 pw1fnex pwex pw1ex resex f1oen ) AFZGZAGZFZHWDUAZIZWDWFUBJ
- WDHWDUCZWGIZWHKKFZHUDZWDKLWJKWKHIWLUEKWKHUFMWCUGKWKWDHUHUIWIWFNWJWHUJWICO
- ZDOZHJZCWDPZDUMWFDCHWDUKWPDWFWNWFTZWNEOZGNZEWCPZWPWQWNWELWRALZWSQZERZWTWN
- WEDSZULEWNAXDUNWTWRWCTZWSQZERXCWSEWCUOXFXBEXEXAWSXAEWCEAUPUQURUSUTVAWPWMW
- DTZWOQZCRWMWRVBZNZWOQZEWCPZCRZWTWOCWDUOXHXLCXHXJEWCPZWOQXLXGXNWOEWMWCVCUR
- XJWOEWCVEVDUSXMXKCRZEWCPWTXKECWCVFXOWSEWCXOXIWNHJZWSWOXPCXIWRVGWMXIWNHVHV
- IWRWNESVPVJVKVLVAVDVMVNWIWFWDWGVQMVOWDWFWGHWDVRWCABVSVTWAWBM $.
+ cab sspw1 df-rex df-pw eqabi anbi1i exbii bitr2i 3bitri csn elpw1 r19.41v
+ bitr4i rexcom4 snex breq1 ceqsexv brpw1fn bitri rexbii bitr3i abbi2i mpbi
+ eqtr4i f1oeq3 pw1fnex pwex pw1ex resex f1oen ) AFZGZAGZFZHWDUAZIZWDWFUBJW
+ DHWDUCZWGIZWHKKFZHUDZWDKLWJKWKHIWLUEKWKHUFMWCUGKWKWDHUHUIWIWFNWJWHUJWICOZ
+ DOZHJZCWDPZDUMWFDCHWDUKWPDWFWNWFTZWNEOZGNZEWCPZWPWQWNWELWRALZWSQZERZWTWNW
+ EDSZULEWNAXDUNWTWRWCTZWSQZERXCWSEWCUOXFXBEXEXAWSXAEWCEAUPUQURUSUTVAWPWMWD
+ TZWOQZCRWMWRVBZNZWOQZEWCPZCRZWTWOCWDUOXHXLCXHXJEWCPZWOQXLXGXNWOEWMWCVCURX
+ JWOEWCVDVEUSXMXKCRZEWCPWTXKECWCVFXOWSEWCXOXIWNHJZWSWOXPCXIWRVGWMXIWNHVHVI
+ WRWNESVJVKVLVMVAVEVNVPWIWFWDWGVQMVOWDWFWGHWDVRWCABVSVTWAWBM $.
$}
${
@@ -59805,7 +59807,7 @@ the first case of his notation (simple exponentiation) and subscript it
wf wb wn snex opex elcompl elsymdif opelssetsn otelins2 otsnelsi3 wfn wss
df-br brfns bitr3i opelco brimage dfrn5 eqeq2i bitr4i brsset rnex ceqsexv
exbii sseq1 oteltxp bibi12i xchbinx exnal 3bitrri con1bii oqelins4 mapval
- df-f eqab ovex breq2 df-3an abbi2i cnvex imaexg mpan xpexg syl2an cnvexg
+ df-f eqabb ovex breq2 df-3an abbi2i cnvex imaexg mpan xpexg syl2an cnvexg
pw1fnex ins3exg syl ssetex ins3ex fnsex 2ndex coex ins2ex 1cex mpan2 3syl
imageex txpex si3ex symdifex imaex complex ins4ex enex inexg syl5eqelr
inex ) CDJZBEJZKZFUAZUBZCJZGUAZUBZBJZAUAZUUNUUQUEUCZLMZUDZGNZFNZAUFOUGZCU
diff --git a/set.mm b/set.mm
index 99b266539a..991f7799ff 100644
--- a/set.mm
+++ b/set.mm
@@ -22276,12 +22276,6 @@ that proposition with a distinct variable (inference associated with
(New usage is discouraged.) $)
nfsb $p |- F/ z [ y / x ] ph $=
( wsb wnf wtru nftru a1i nfsbd mptru ) ABCFDGHABCDBIADGHEJKL $.
-
- $( Obsolete version of ~ nfsb as of 25-Feb-2024. (Contributed by Mario
- Carneiro, 11-Aug-2016.) (New usage is discouraged.)
- (Proof modification is discouraged.) $)
- nfsbOLD $p |- F/ z [ y / x ] ph $=
- ( weq wal wsb wnf axc16nf nfsb4 pm2.61i ) DCFDGABCHZDIMDCDJABCDEKL $.
$}
${
@@ -24761,7 +24755,7 @@ yield an eliminable and weakly (that is, object-level) conservative
theory axioms. He calls the construction ` { y | ph } ` a "class term".
For a full description of how classes are introduced and how to recover
the primitive language, see the books of Quine and Levy (and the comment
- of ~ eqab for a quick overview). For a general discussion of the theory
+ of ~ eqabb for a quick overview). For a general discussion of the theory
of classes, see ~ mmset.html#class . (Contributed by NM, 26-May-1993.)
(Revised by BJ, 19-Aug-2023.) $)
df-clab $a |- ( x e. { y | ph } <-> [ x / y ] ph ) $.
@@ -25198,7 +25192,7 @@ variables at the beginning of this section (not visible on the webpages).
it does not have the usual form of a definition. If we required a
definition to have the usual form, we would call ~ df-cleq an axiom.
- See also comments under ~ df-clab , ~ df-clel , and ~ eqab .
+ See also comments under ~ df-clab , ~ df-clel , and ~ eqabb .
In the form of ~ dfcleq , this is called the "axiom of extensionality"
by [Levy] p. 338, who treats the theory of classes as an extralogical
@@ -25997,13 +25991,13 @@ the definition of class equality ( ~ df-cleq ). Its forward implication
${
$d x y $. $d y A $. $d ph y $. $d ps x $.
- eqabw.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
- $( Version of ~ eqab using implicit substitution, which requires fewer
+ eqabbw.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
+ $( Version of ~ eqabb using implicit substitution, which requires fewer
axioms. (Contributed by GG and AV, 18-Sep-2024.) $)
- eqabw $p |- ( A = { x | ph } <-> A. y ( y e. A <-> ps ) ) $=
+ eqabbw $p |- ( A = { x | ph } <-> A. y ( y e. A <-> ps ) ) $=
( cab wceq cv wcel wb wal dfcleq wsb df-clab sbievw bitri bibi2i albii )
EACGZHDIZEJZUATJZKZDLUBBKZDLDETMUDUEDUCBUBUCACDNBADCOABCDFPQRSQ $.
- $( $j usage 'eqabw' avoids 'df-clel' 'ax-8' 'ax-10' 'ax-11' 'ax-12'; $)
+ $( $j usage 'eqabbw' avoids 'df-clel' 'ax-8' 'ax-10' 'ax-11' 'ax-12'; $)
$}
@@ -26031,7 +26025,7 @@ the definition of class equality ( ~ df-cleq ). Its forward implication
it does not have the usual form of a definition. If we required a
definition to have the usual form, we would call ~ df-clel an axiom.
- See also comments under ~ df-clab , ~ df-cleq , and ~ eqab .
+ See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb .
Alternate characterizations of ` A e. B ` when either ` A ` or ` B ` is
a set are given by ~ clel2g , ~ clel3g , and ~ clel4g .
@@ -26666,11 +26660,10 @@ generally appear in a single form (either definitional, but more often
${
$d x A y $. $d ph y $.
- $( One direction of ~ eqab is provable from fewer axioms. (Contributed by
+ $( One direction of ~ eqabb is provable from fewer axioms. (Contributed by
Wolf Lammen, 13-Feb-2025.) $)
eqabr $p |- ( A. x ( x e. A <-> ph ) -> A = { x | ph } ) $=
- ( cv wcel wb wal cab wceq abbi abid1 eqeq1i sylibr ) BDCEZAFBGNBHZABHZICP
- INABJCOPBCKLM $.
+ ( cv wcel wb wal cab abid1 abbi eqtrid ) BDCEZAFBGCLBHABHBCILABJK $.
$( $j usage 'eqabr' avoids 'ax-10' 'ax-11' 'ax-12'; $)
$( Equality of a class variable and a class abstraction (also called a
@@ -26697,17 +26690,17 @@ generally appear in a single form (either definitional, but more often
equivalent formulation ~ cplem2 . For more information on class
variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13.
- Usage of ~ eqabw is preferred since it requires fewer axioms.
+ Usage of ~ eqabbw is preferred since it requires fewer axioms.
(Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen,
12-Feb-2025.) $)
- eqab $p |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) ) $=
+ eqabb $p |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) ) $=
( cab wceq cv wcel wb wal abid1 eqeq1i abbib bitri ) CABDZEBFCGZBDZNEOAHB
ICPNBCJKOABLM $.
- $( Obsolete version of ~ eqab as of 12-Feb-2025. (Contributed by NM,
+ $( Obsolete version of ~ eqabb as of 12-Feb-2025. (Contributed by NM,
26-May-1993.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
- eqabOLD $p |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) ) $=
+ eqabbOLD $p |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) ) $=
( vy cab wceq cv wcel wb wal ax-5 hbab1 cleqh abid bibi2i albii bitri ) C
ABEZFBGZCHZSRHZIZBJTAIZBJBDCRDGCHBKABDLMUBUCBUAATABNOPQ $.
$}
@@ -26715,16 +26708,16 @@ generally appear in a single form (either definitional, but more often
${
$d x A $.
$( Equality of a class variable and a class abstraction. Commuted form of
- ~ eqab . (Contributed by NM, 20-Aug-1993.) $)
- eqabc $p |- ( { x | ph } = A <-> A. x ( ph <-> x e. A ) ) $=
- ( cab wceq cv wcel wb wal eqab eqcom bicom albii 3bitr4i ) CABDZEBFCGZAHZ
- BIOCEAPHZBIABCJOCKRQBAPLMN $.
+ ~ eqabb . (Contributed by NM, 20-Aug-1993.) $)
+ eqabcb $p |- ( { x | ph } = A <-> A. x ( ph <-> x e. A ) ) $=
+ ( cab wceq cv wcel wb wal eqabb eqcom bicom albii 3bitr4i ) CABDZEBFCGZAH
+ ZBIOCEAPHZBIABCJOCKRQBAPLMN $.
$}
${
eqabd.1 $e |- ( ph -> A = { x | ps } ) $.
$( Equality of a class variable and a class abstraction (deduction form of
- ~ eqab ). (Contributed by NM, 16-Nov-1995.) $)
+ ~ eqabb ). (Contributed by NM, 16-Nov-1995.) $)
eqabd $p |- ( ph -> ( x e. A <-> ps ) ) $=
( cv wcel cab eleq2d abid bitrdi ) ACFZDGLBCHZGBADMLEIBCJK $.
$}
@@ -26777,8 +26770,8 @@ generally appear in a single form (either definitional, but more often
17-Jan-2006.) $)
clabel $p |- ( { x | ph } e. A <->
E. y ( y e. A /\ A. x ( x e. y <-> ph ) ) ) $=
- ( cab wcel cv wceq wa wex wb wal dfclel eqab anbi2ci exbii bitri ) ABEZDF
- CGZRHZSDFZIZCJUABGSFAKBLZIZCJCRDMUBUDCTUCUAABSNOPQ $.
+ ( cab wcel cv wceq wa wex wb wal dfclel eqabb anbi2ci exbii bitri ) ABEZD
+ FCGZRHZSDFZIZCJUABGSFAKBLZIZCJCRDMUBUDCTUCUAABSNOPQ $.
$}
${
@@ -31940,9 +31933,9 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is
9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
rabid2OLD $p |- ( A = { x e. A | ph } <-> A. x e. A ph ) $=
- ( cv wcel wa cab wceq wi wal crab wral wb eqab pm4.71 albii bitr4i df-rab
- eqeq2i df-ral 3bitr4i ) CBDCEZAFZBGZHZUBAIZBJZCABCKZHABCLUEUBUCMZBJUGUCBC
- NUFUIBUBAOPQUHUDCABCRSABCTUA $.
+ ( cv wcel wa cab wceq wi wal crab eqabb pm4.71 albii bitr4i df-rab eqeq2i
+ wral wb df-ral 3bitr4i ) CBDCEZAFZBGZHZUBAIZBJZCABCKZHABCRUEUBUCSZBJUGUCB
+ CLUFUIBUBAMNOUHUDCABCPQABCTUA $.
$}
${
@@ -34394,7 +34387,7 @@ general is seen either by substitution (when the variable ` V ` has no
20-Apr-2022.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
rabeqcOLD $p |- { x e. A | ph } = A $=
- ( crab cv wcel wa cab df-rab wceq wb eqabc pm4.71i bicomi mpgbir eqtri )
+ ( crab cv wcel wa cab df-rab wceq wb eqabcb pm4.71i bicomi mpgbir eqtri )
ABCEBFCGZAHZBIZCABCJTCKSRLBSBCMRSRADNOPQ $.
$}
@@ -35591,9 +35584,9 @@ too large (beyond the size of those used in standard mathematics), the
(Proof modification is discouraged.) $)
ru $p |- { x | x e/ x } e/ _V $=
( vy cv wnel cab cvv wcel wceq wex wel wb wn pm5.19 eleq1w df-nel eleq12d
- wal id notbid mtbir bitrid bibi12d spvv mto eqab nex isset nelir ) ACZUID
- ZAEZFUKFGBCZUKHZBIUMBUMABJZUJKZAQZUPBBJZUQLZKZUQMUOUSABUIULHZUNUQUJURABUL
- NUJAAJZLUTURUIUIOUTVAUQUTUIULUIULUTRZVBPSUAUBUCUDUJAULUETUFBUKUGTUH $.
+ wal id notbid mtbir bitrid bibi12d spvv mto eqabb nex isset nelir ) ACZUI
+ DZAEZFUKFGBCZUKHZBIUMBUMABJZUJKZAQZUPBBJZUQLZKZUQMUOUSABUIULHZUNUQUJURABU
+ LNUJAAJZLUTURUIUIOUTVAUQUTUIULUIULUTRZVBPSUAUBUCUDUJAULUETUFBUKUGTUH $.
$( $j usage 'ru' avoids 'ax-13' 'ax-reg'; $)
$}
@@ -36639,13 +36632,13 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
NM, 5-Nov-2005.) $)
sbcabel $p |- ( A e. V -> ( [. A / x ]. { y | ph } e. B <->
{ y | [. A / x ]. ph } e. B ) ) $=
- ( vw wcel cvv cab wsbc wb cv wceq wa wex wal bitrid eqab elex sbcan sbcal
- sbcex2 sbcbig sbcg bibi1d bitrd albidv sbcbii 3bitr4g nfcri sbcgf anbi12d
- exbidv dfclel syl ) DFIDJIZACKZEIZBDLZABDLZCKZEIZMDFUAURHNZUSOZVEEIZPZHQZ
- BDLZVEVCOZVGPZHQZVAVDVJVHBDLZHQURVMVHHBDUDURVNVLHVNVFBDLZVGBDLZPURVLVFVGB
- DUBURVOVKVPVGURCNVEIZAMZCRZBDLZVQVBMZCRZVOVKVTVRBDLZCRURWBVRCBDUCURWCWACU
- RWCVQBDLZVBMWAVQABDJUEURWDVQVBVQBDJUFUGUHUISVFVSBDACVETUJVBCVETUKVGBDJBHE
- GULUMUNSUOSUTVIBDHUSEUPUJHVCEUPUKUQ $.
+ ( vw wcel cvv cab wsbc wb cv wceq wa wex wal bitrid eqabb elex sbcan sbcg
+ sbcex2 sbcal sbcbig bibi1d bitrd albidv sbcbii 3bitr4g nfcri sbcgf exbidv
+ anbi12d dfclel syl ) DFIDJIZACKZEIZBDLZABDLZCKZEIZMDFUAURHNZUSOZVEEIZPZHQ
+ ZBDLZVEVCOZVGPZHQZVAVDVJVHBDLZHQURVMVHHBDUDURVNVLHVNVFBDLZVGBDLZPURVLVFVG
+ BDUBURVOVKVPVGURCNVEIZAMZCRZBDLZVQVBMZCRZVOVKVTVRBDLZCRURWBVRCBDUEURWCWAC
+ URWCVQBDLZVBMWAVQABDJUFURWDVQVBVQBDJUCUGUHUISVFVSBDACVETUJVBCVETUKVGBDJBH
+ EGULUMUOSUNSUTVIBDHUSEUPUJHVCEUPUKUQ $.
$}
${
@@ -37724,9 +37717,9 @@ technically classes despite morally (and provably) being sets, like ` 1 `
8-Jan-2002.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
dfss2OLD $p |- ( A C_ B <-> A. x ( x e. A -> x e. B ) ) $=
- ( wss cv wcel wa wb wal cin wceq cab dfss df-in eqeq2i eqab 3bitri pm4.71
- wi albii bitr4i ) BCDZAEZBFZUDUCCFZGZHZAIZUDUESZAIUBBBCJZKBUFALZKUHBCMUJU
- KBABCNOUFABPQUIUGAUDUERTUA $.
+ ( wss cv wcel wa wb wal wi cin wceq dfss df-in eqeq2i eqabb 3bitri pm4.71
+ cab albii bitr4i ) BCDZAEZBFZUDUCCFZGZHZAIZUDUEJZAIUBBBCKZLBUFASZLUHBCMUJ
+ UKBABCNOUFABPQUIUGAUDUERTUA $.
$( Alternate definition of subclass relationship. (Contributed by NM,
14-Oct-1999.) $)
@@ -41648,10 +41641,10 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets,
17-Feb-2004.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
disjOLD $p |- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B ) $=
- ( cin c0 wceq cv wcel wn wi wal wral wa cab df-in eqeq1i eqabc imnan noel
- wb nbn bitr2i albii 3bitri df-ral bitr4i ) BCDZEFZAGZBHZUICHZIZJZAKZULABL
- UHUJUKMZANZEFUOUIEHZTZAKUNUGUPEABCOPUOAEQURUMAUMUOIURUJUKRUQUOUISUAUBUCUD
- ULABUEUF $.
+ ( cin c0 wceq cv wcel wn wi wal wral wa wb df-in eqeq1i eqabcb imnan noel
+ cab nbn bitr2i albii 3bitri df-ral bitr4i ) BCDZEFZAGZBHZUICHZIZJZAKZULAB
+ LUHUJUKMZATZEFUOUIEHZNZAKUNUGUPEABCOPUOAEQURUMAUMUOIURUJUKRUQUOUISUAUBUCU
+ DULABUEUF $.
$( Two ways of saying that two classes are disjoint. (Contributed by Jeff
Madsen, 19-Jun-2011.) $)
@@ -49861,10 +49854,10 @@ under a function is also a set (see the variant ~ funimaex ). Although
$( A version of Replacement using class abstractions. (Contributed by NM,
26-Nov-1995.) $)
zfrep4 $p |- { y | E. x ( ph /\ ps ) } e. _V $=
- ( cv cab wcel wa wex cvv abid anbi1i exbii abbii wceq wb wal eqab issetri
- nfab1 wi sylbi zfrepclf mpbir eqeltrri ) CHACIZJZBKZCLZDIZABKZCLZDIMULUOD
- UKUNCUJABACNZOPQEUMEHZUMRZELDHZUQJULSDTZELBCDEUIACUCFUJABUSUQRUDDTELUPGUE
- UFURUTEULDUQUAPUGUBUH $.
+ ( cv cab wcel wa wex cvv abid anbi1i exbii abbii wceq wb wal nfab1 sylbi
+ wi zfrepclf eqabb mpbir issetri eqeltrri ) CHACIZJZBKZCLZDIZABKZCLZDIMULU
+ ODUKUNCUJABACNZOPQEUMEHZUMRZELDHZUQJULSDTZELBCDEUIACUAFUJABUSUQRUCDTELUPG
+ UBUDURUTEULDUQUEPUFUGUH $.
$}
@@ -50745,8 +50738,8 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with
~ vpwex . (Revised by BJ, 10-Aug-2022.) $)
vpwex $p |- ~P x e. _V $=
( vw vy vz cv cpw wss cab cvv df-pw wceq wex wel wal axpow2 bm1.3ii sseq1
- wb eqabw exbii mpbir issetri eqeltri ) AEZFBEZUDGZBHZIBUDJCUGCEZUGKZCLDCM
- DEZUDGZRDNZCLUKCDACDOPUIULCUFUKBDUHUEUJUDQSTUAUBUC $.
+ wb eqabbw exbii mpbir issetri eqeltri ) AEZFBEZUDGZBHZIBUDJCUGCEZUGKZCLDC
+ MDEZUDGZRDNZCLUKCDACDOPUIULCUFUKBDUHUEUJUDQSTUAUBUC $.
$( $j usage 'vpwex' avoids 'ax-10' 'ax-11' 'ax-12'; $)
$}
@@ -56479,9 +56472,9 @@ ordered pairs as classes (in set.mm, the Kuratowski encoding). A more
dmopab3 $p |- ( A. x e. A E. y ph <->
dom { <. x , y >. | ( x e. A /\ ph ) } = A ) $=
( wex wral cv wcel wi wal wa wb copab cdm wceq df-ral pm4.71 albii dmopab
- cab 19.42v abbii eqtri eqeq1i eqcom eqab 3bitr2ri 3bitri ) ACEZBDFBGDHZUI
- IZBJUJUJUIKZLZBJZUJAKZBCMNZDOZUIBDPUKUMBUJUIQRUQULBTZDODUROUNUPURDUPUOCEZ
- BTURUOBCSUSULBUJACUAUBUCUDDURUEULBDUFUGUH $.
+ cab 19.42v abbii eqtri eqeq1i eqcom eqabb 3bitr2ri 3bitri ) ACEZBDFBGDHZU
+ IIZBJUJUJUIKZLZBJZUJAKZBCMNZDOZUIBDPUKUMBUJUIQRUQULBTZDODUROUNUPURDUPUOCE
+ ZBTURUOBCSUSULBUJACUAUBUCUDDURUEULBDUFUGUH $.
$}
${
@@ -56523,11 +56516,11 @@ ordered pairs as classes (in set.mm, the Kuratowski encoding). A more
$( An empty domain is equivalent to an empty range. (Contributed by NM,
21-May-1998.) $)
dm0rn0 $p |- ( dom A = (/) <-> ran A = (/) ) $=
- ( vx vy cv wbr wex cab c0 wceq wcel wb wal alnex noel albii eqabc 3bitr4i
- wn nbn eqeq1i cdm crn excom xchbinx bitr4i 3bitr3i df-dm dfrn2 ) BDZCDZAE
- ZCFZBGZHIZUKBFZCGZHIZAUAZHIAUBZHIULUIHJZKZBLZUOUJHJZKZCLZUNUQULRZBLZUORZC
- LZVBVEVGUOCFZRVIVGULBFVJULBMUKBCUCUDUOCMUEVFVABUTULUINSOVHVDCVCUOUJNSOUFU
- LBHPUOCHPQURUMHBCAUGTUSUPHBCAUHTQ $.
+ ( vx vy cv wbr wex cab c0 wceq wcel wb wal wn alnex noel nbn albii eqabcb
+ 3bitr4i eqeq1i cdm crn excom xchbinx bitr4i 3bitr3i df-dm dfrn2 ) BDZCDZA
+ EZCFZBGZHIZUKBFZCGZHIZAUAZHIAUBZHIULUIHJZKZBLZUOUJHJZKZCLZUNUQULMZBLZUOMZ
+ CLZVBVEVGUOCFZMVIVGULBFVJULBNUKBCUCUDUOCNUEVFVABUTULUIOPQVHVDCVCUOUJOPQUF
+ ULBHRUOCHRSURUMHBCAUGTUSUPHBCAUHTS $.
$}
$( The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
@@ -62984,11 +62977,11 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
(New usage is discouraged.) $)
funimaexgOLD $p |- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V ) $=
( vw vx vy vz wcel wfun cima cvv cv wceq imaeq2 eleq1d wal wex wel bitri
- wi imbi2d wrel cop dffun5 wa wb nfv axrep4 isset dfima3 eqeq2i eqab exbii
- cab sylibr simplbiim vtoclg impcom ) BCHAIZABJZKHZUSADLZJZKHZTUSVATDBCVBB
- MZVDVAUSVEVCUTKVBBANOUAUSAUBELFLZUCAHZVFGLZMTFPGQEPZVDEFGAUDVIFGREDRVGUEE
- QZUFFPZGQZVDVGEFGDVGGUGUHVDVHVCMZGQVLGVCUIVMVKGVMVHVJFUNZMVKVCVNVHEFAVBUJ
- UKVJFVHULSUMSUOUPUQUR $.
+ wi imbi2d cop dffun5 wa wb nfv axrep4 isset cab dfima3 eqeq2i eqabb exbii
+ wrel sylibr simplbiim vtoclg impcom ) BCHAIZABJZKHZUSADLZJZKHZTUSVATDBCVB
+ BMZVDVAUSVEVCUTKVBBANOUAUSAUNELFLZUBAHZVFGLZMTFPGQEPZVDEFGAUCVIFGREDRVGUD
+ EQZUEFPZGQZVDVGEFGDVGGUFUGVDVHVCMZGQVLGVCUHVMVKGVMVHVJFUIZMVKVCVNVHEFAVBU
+ JUKVJFVHULSUMSUOUPUQUR $.
$}
${
@@ -67318,10 +67311,10 @@ in the range of the function (the implication "to the right" is always
A. y e. B E. x e. A y = ( F ` x ) ) ) $=
( wfo wf crn wceq wa cv cfv wrex wral dffo2 cab wb wcel wal wi wfn fnrnfv
ffn eqeq1d syl dfbi2 ffvelcdm adantr eqeltrd rexlimdva2 biantrurd bitr4id
- simpr albidv eqabc df-ral 3bitr4g bitrd pm5.32i bitri ) CDEFCDEGZEHZDIZJV
- ABKZAKZELZIZACMZBDNZJCDEOVAVCVIVAVCVHBPZDIZVIVAECUAZVCVKQCDEUCVLVBVJDABCE
- UBUDUEVAVHVDDRZQZBSVMVHTZBSVKVIVAVNVOBVAVNVHVMTZVOJVOVHVMUFVAVPVOVAVGVMAC
- VAVECRJZVGJVDVFDVQVGUMVQVFDRVGCDVEEUGUHUIUJUKULUNVHBDUOVHBDUPUQURUSUT $.
+ simpr albidv eqabcb df-ral 3bitr4g bitrd pm5.32i bitri ) CDEFCDEGZEHZDIZJ
+ VABKZAKZELZIZACMZBDNZJCDEOVAVCVIVAVCVHBPZDIZVIVAECUAZVCVKQCDEUCVLVBVJDABC
+ EUBUDUEVAVHVDDRZQZBSVMVHTZBSVKVIVAVNVOBVAVNVHVMTZVOJVOVHVMUFVAVPVOVAVGVMA
+ CVAVECRJZVGJVDVFDVQVGUMVQVFDRVGCDVEEUGUHUIUJUKULUNVHBDUOVHBDUPUQURUSUT $.
$( Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.) $)
@@ -99339,17 +99332,17 @@ all reals (greatest real number) for which all positive reals are greater.
dfsup2 $p |- sup ( B , A , R ) =
U. ( A \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) ) $=
( vx vy vz cv wbr wn wral wrex wi wa cdif cvv wcel vex elima bitri eqtri
- csup crab cuni ccnv cima cun df-sup cab cin dfrab3 wb eqabc eldif mpbiran
- wceq dfrex2 orbi12i elun ianor 3bitr4i con2bii brcnv notbii ralbii impexp
- imbi1i rexbii imbi2i con34b bitr3i ralbii2 anbi12i 3bitr2ri mpgbir ineq2i
- wo invdif unieqi ) BACUADGZEGZCHZIZEBJZVTVSCHZVTFGZCHZFBKZLZEAJZMZDAUBZUC
- ACUDZBUEZCAWMNZUEZUFZNZUCDEFBACUGWKWQWKAWJDUHZUIZWQWJDAUJWSAOWPNZUIWQWRWT
- AWRWTUOWJVSWTPZUKDWJDWTULXAVSWPPZIZVTVSWLHZIZEBJZWDIZEWNJZMZWJXAVSOPXCDQZ
- VSOWPUMUNXBXIVSWMPZVSWOPZVPXFIZXHIZVPXBXIIXKXMXLXNXKXDEBKXMEVSWLBXJRXDEBU
- PSXLWDEWNKXNEVSCWNXJRWDEWNUPSUQVSWMWOURXFXHUSUTVAXFWCXHWIXEWBEBXDWAVTVSCE
- QZXJVBVCVDXGWHEWNAVTAPZVTWMPZIZMZXGLXPXRXGLZLVTWNPZXGLXPWHLXPXRXGVEYAXSXG
- VTAWMUMVFWHXTXPWHWDXQLXTXQWGWDXQWEVTWLHZFBKWGFVTWLBXORYBWFFBWEVTCFQXOVBVG
- SVHWDXQVIVJVHUTVKVLVMVNVOAWPVQTTVRT $.
+ csup crab cuni ccnv cima cun df-sup cab cin dfrab3 wceq wb eqabcb mpbiran
+ eldif wo dfrex2 orbi12i ianor 3bitr4i con2bii notbii ralbii impexp imbi1i
+ rexbii imbi2i con34b bitr3i ralbii2 anbi12i 3bitr2ri mpgbir ineq2i invdif
+ elun brcnv unieqi ) BACUADGZEGZCHZIZEBJZVTVSCHZVTFGZCHZFBKZLZEAJZMZDAUBZU
+ CACUDZBUEZCAWMNZUEZUFZNZUCDEFBACUGWKWQWKAWJDUHZUIZWQWJDAUJWSAOWPNZUIWQWRW
+ TAWRWTUKWJVSWTPZULDWJDWTUMXAVSWPPZIZVTVSWLHZIZEBJZWDIZEWNJZMZWJXAVSOPXCDQ
+ ZVSOWPUOUNXBXIVSWMPZVSWOPZUPXFIZXHIZUPXBXIIXKXMXLXNXKXDEBKXMEVSWLBXJRXDEB
+ UQSXLWDEWNKXNEVSCWNXJRWDEWNUQSURVSWMWOVPXFXHUSUTVAXFWCXHWIXEWBEBXDWAVTVSC
+ EQZXJVQVBVCXGWHEWNAVTAPZVTWMPZIZMZXGLXPXRXGLZLVTWNPZXGLXPWHLXPXRXGVDYAXSX
+ GVTAWMUOVEWHXTXPWHWDXQLXTXQWGWDXQWEVTWLHZFBKWGFVTWLBXORYBWFFBWEVTCFQXOVQV
+ FSVGWDXQVHVIVGUTVJVKVLVMVNAWPVOTTVRT $.
$}
${
@@ -105497,13 +105490,13 @@ of the previous layer (and the union of previous layers when the
rankf $p |- rank : U. ( R1 " On ) --> On $=
( vx vy vz cr1 con0 cima cuni crnk wf wfn cv cfv wcel wceq eqtri mpbir2an
cdm cvv mpan sylbi wral wfun csuc crab cint df-rank copab cmpt mptv dmeqi
- funmpt2 wex dmopab wb eqabc wrex rankwflemb intexrab isset 3bitrri mpgbir
- cab df-fn c0 wne rabn0 bitr4i intex vex fvmpt2 wss ssrab2 oninton eqeltrd
- rgen ffnfv ) DEFGZEHIHVQJZAKZHLZEMZAVQUAVRHUBHQZVQNARVSBKUCDLMZBEUDZUEZHA
- BUFZUKWBCKWENZACUGZQZVQHWHHARWEUHWHWFACWEUIOUJWIWGCULZAVBZVQWGACUMWKVQNWJ
- VSVQMZUNAWJAVQUOWLWCBEUPZWERMZWJBVSUQZWCBEURCWEUSUTVAOOHVQVCPWAAVQWLWDVDV
- EZWAWLWMWPWOWCBEVFVGWPVTWEEWPWNVTWENZWDVHVSRMWNWQAVIARWERHWFVJSTWDEVKWPWE
- EMWCBEVLWDVMSVNTVOAVQEHVPP $.
+ funmpt2 wex cab dmopab wb eqabcb rankwflemb intexrab isset 3bitrri mpgbir
+ wrex df-fn c0 wne rabn0 bitr4i vex fvmpt2 wss ssrab2 oninton eqeltrd rgen
+ intex ffnfv ) DEFGZEHIHVQJZAKZHLZEMZAVQUAVRHUBHQZVQNARVSBKUCDLMZBEUDZUEZH
+ ABUFZUKWBCKWENZACUGZQZVQHWHHARWEUHWHWFACWEUIOUJWIWGCULZAUMZVQWGACUNWKVQNW
+ JVSVQMZUOAWJAVQUPWLWCBEVBZWERMZWJBVSUQZWCBEURCWEUSUTVAOOHVQVCPWAAVQWLWDVD
+ VEZWAWLWMWPWOWCBEVFVGWPVTWEEWPWNVTWENZWDVOVSRMWNWQAVHARWERHWFVISTWDEVJWPW
+ EEMWCBEVKWDVLSVMTVNAVQEHVPP $.
$}
$( The rank of a set is an ordinal number. Proposition 9.15(1) of
@@ -532264,17 +532257,17 @@ have become an indirect lemma of the theorem in question (i.e. a lemma
E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) ) $=
( vu vv wal weq wex cfn cvv wel wa cv wcel cop nfv nfel2 nfan wi wb copab
wceq wfun wmo funopab nfa1 mof albii bitr2i cima vex eleq2w2 mpbiri imafi
- sylan2 elexd cab nfopab nfex nfab issetf eqab exbii opabidw anbi2i bibi2i
- 3bitrri dfima3 nfopab2 nfopab1 elequ1 opeq1 eleq1d anbi12d cbvexv1 anbi2d
- opeq2 exbidv bitrid cbvabw eqtri eleq1i bitr4i sylibr sylanb expcom ) ACH
- ZDCIUADHCJZEHZKLUDZDCMZEBMZWINZEJZUBZDHZCJZWKWIEDUCZUEZWLWSXAWIDUFZEHWKWI
- EDUGXBWJEWIDCACUHZUIUJUKXAWLNZWTBOZULZLPZWSXDXFKWLXAXEKPZXFKPWLXHXELPBUMB
- KLUNUOWTXEUPUQURWSWNEOZDOZQZWTPZNZEJZDUSZLPZXGXPCOZXOUDZCJWMXNUBZDHZCJWSC
- XOXNCDXMCEWNXLCWNCRCXKWTWIEDCXCUTSTVAVBVCXRXTCXNDXQVDVEXTWRCXSWQDXNWPWMXM
- WOEXLWIWNWIEDVFVGVEVHUJVEVIXFXOLXFFBMZFOZGOZQZWTPZNZFJZGUSXOFGWTXEVJYGXNG
- DYFDFYAYEDYADRDYDWTWIEDVKSTVAXNGRYGWNXIYCQZWTPZNZEJGDIZXNYFYJFEYAYEEYAERE
- YDWTWIEDVLSTYJFRFEIZYAWNYEYIFEBVMYLYDYHWTYBXIYCVNVOVPVQYKYJXMEYKYIXLWNYKY
- HXKWTYCXJXIVSVOVRVTWAWBWCWDWEWFWGWH $.
+ sylan2 elexd nfopab nfex issetf eqabb exbii opabidw anbi2i bibi2i 3bitrri
+ cab nfab dfima3 nfopab2 nfopab1 elequ1 opeq1 eleq1d anbi12d cbvexv1 opeq2
+ anbi2d exbidv bitrid cbvabw eqtri eleq1i bitr4i sylibr sylanb expcom ) AC
+ HZDCIUADHCJZEHZKLUDZDCMZEBMZWINZEJZUBZDHZCJZWKWIEDUCZUEZWLWSXAWIDUFZEHWKW
+ IEDUGXBWJEWIDCACUHZUIUJUKXAWLNZWTBOZULZLPZWSXDXFKWLXAXEKPZXFKPWLXHXELPBUM
+ BKLUNUOWTXEUPUQURWSWNEOZDOZQZWTPZNZEJZDVHZLPZXGXPCOZXOUDZCJWMXNUBZDHZCJWS
+ CXOXNCDXMCEWNXLCWNCRCXKWTWIEDCXCUSSTUTVIVAXRXTCXNDXQVBVCXTWRCXSWQDXNWPWMX
+ MWOEXLWIWNWIEDVDVEVCVFUJVCVGXFXOLXFFBMZFOZGOZQZWTPZNZFJZGVHXOFGWTXEVJYGXN
+ GDYFDFYAYEDYADRDYDWTWIEDVKSTUTXNGRYGWNXIYCQZWTPZNZEJGDIZXNYFYJFEYAYEEYAER
+ EYDWTWIEDVLSTYJFRFEIZYAWNYEYIFEBVMYLYDYHWTYBXIYCVNVOVPVQYKYJXMEYKYIXLWNYK
+ YHXKWTYCXJXIVRVOVSVTWAWBWCWDWEWFWGWH $.
$( $j usage 'fineqvrep' avoids 'ax-pow' 'ax-rep' 'ax-inf' 'ax-inf2'; $)
$}
@@ -532285,11 +532278,11 @@ have become an indirect lemma of the theorem in question (i.e. a lemma
fineqvpow $p |- ( Fin = _V ->
E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) ) $=
( vv cfn cvv wceq cv wss wel wi wal wex wb cab wcel syl exbii sylib df-pw
- cpw eleq2w2 pwfi bitr3di mpbii elexd eqeltrrid elisset sseq1 eqabw biimpr
- vex alimi eximi dfss2 imbi1i albii ) FGHZCIZAIZJZCBKZLZCMZBNZDCKDAKLDMZVC
- LZCMZBNUSVCVBOZCMZBNZVFUSBIZEIZVAJZEPZHZBNZVLUSVPGQVRUSVPVAUBZGEVAUAUSVSF
- USVAGQZVSFQZAUMUSVAFQVTWAAFGUCVAUDUEUFUGUHBVPGUIRVQVKBVOVBECVMVNUTVAUJUKS
- TVKVEBVJVDCVCVBULUNUORVEVIBVDVHCVBVGVCDUTVAUPUQURST $.
+ cpw vex eleq2w2 bitr3di mpbii elexd eqeltrrid elisset sseq1 eqabbw biimpr
+ pwfi alimi eximi dfss2 imbi1i albii ) FGHZCIZAIZJZCBKZLZCMZBNZDCKDAKLDMZV
+ CLZCMZBNUSVCVBOZCMZBNZVFUSBIZEIZVAJZEPZHZBNZVLUSVPGQVRUSVPVAUBZGEVAUAUSVS
+ FUSVAGQZVSFQZAUCUSVAFQVTWAAFGUDVAUMUEUFUGUHBVPGUIRVQVKBVOVBECVMVNUTVAUJUK
+ STVKVEBVJVDCVCVBULUNUORVEVIBVDVHCVBVGVCDUTVAUPUQURST $.
$( $j usage 'fineqvpow' avoids 'ax-pow' 'ax-rep' 'ax-inf' 'ax-inf2'; $)
$}
@@ -539542,16 +539535,16 @@ codes is an increasing chain (with respect to inclusion). (Contributed
fmla0xp $p |- ( Fmla ` (/) ) = ( { (/) } X. ( _om X. _om ) ) $=
( vx vi vj vy vz c0 cv wceq com wrex cxp wcel wb cop wa eqeq2d wex adantr
elxpi adantl cfmla cfv cgoe co cvv crab cab csn fmla0 rabab goel 2rexbiia
- eqabc 0ex snid opelxpi opelxpd eleq1 syl5ibrcom rexlimivv elsni opeq1d wi
- a1i simprr simpl opeq2 eqtrd jca ex 2eximdv syl6ibr syl5com sylbid impcom
- r2ex exlimivv syl impbii bitri mpgbir 3eqtri ) FUAUBAGZBGZCGZUCUDZHZCIJBI
- JZAUEUFWHAUGZFUHZIIKZKZABCUIWHAUJWIWLHWHWCWLLZMAWHAWLUMWHWCFWDWENZNZHZCIJ
- BIJZWMWGWPBCIIWDILWEILOZWFWOWCWDWEUKPULWQWMWPWMBCIIWRWMWPWOWLLWRFWNWJWKFW
- JLWRFUNUOVDWDWEIIUPUQWCWOWLURUSUTWMWCDGZEGZNZHZWSWJLZWTWKLZOZOZEQDQWQDEWC
- WJWKSXFWQDEXEXBWQXEXBWCFWTNZHZWQXCXBXHMXDXCXAXGWCXCWSFWTWSFVAVBPRXDXHWQVC
- XCXDWTWNHZWROZCQBQZXHWQBCWTIISXHXKWRWPOZCQBQWQXHXJXLBCXHXJXLXHXJOZWRWPXHX
- IWRVEXMWCXGWOXHXJVFXJXGWOHZXHXIXNWRWTWNFVGRTVHVIVJVKWPBCIIVPVLVMTVNVOVQVR
- VSVTWAWB $.
+ eqabcb 0ex a1i opelxpi opelxpd eleq1 syl5ibrcom rexlimivv elsni opeq1d wi
+ snid simprr simpl opeq2 jca ex 2eximdv r2ex syl6ibr syl5com sylbid impcom
+ eqtrd exlimivv syl impbii bitri mpgbir 3eqtri ) FUAUBAGZBGZCGZUCUDZHZCIJB
+ IJZAUEUFWHAUGZFUHZIIKZKZABCUIWHAUJWIWLHWHWCWLLZMAWHAWLUMWHWCFWDWENZNZHZCI
+ JBIJZWMWGWPBCIIWDILWEILOZWFWOWCWDWEUKPULWQWMWPWMBCIIWRWMWPWOWLLWRFWNWJWKF
+ WJLWRFUNVDUOWDWEIIUPUQWCWOWLURUSUTWMWCDGZEGZNZHZWSWJLZWTWKLZOZOZEQDQWQDEW
+ CWJWKSXFWQDEXEXBWQXEXBWCFWTNZHZWQXCXBXHMXDXCXAXGWCXCWSFWTWSFVAVBPRXDXHWQV
+ CXCXDWTWNHZWROZCQBQZXHWQBCWTIISXHXKWRWPOZCQBQWQXHXJXLBCXHXJXLXHXJOZWRWPXH
+ XIWRVEXMWCXGWOXHXJVFXJXGWOHZXHXIXNWRWTWNFVGRTVPVHVIVJWPBCIIVKVLVMTVNVOVQV
+ RVSVTWAWB $.
$}
${
@@ -546660,15 +546653,15 @@ Set induction (or epsilon induction)
( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) ) $=
( vy vx cv wa wcel cvv csset ctrans cid cep cdif wceq wbr wex vex anbi12i
wn bitri wo anbi1i con0 wpss wtr wi wal cab cxp cin cun crn dfon2 wb elrn
- eqabc wss brin brsset brxp mpbiran2 eltrans ioran brun ideq epel xchnxbir
- orbi12i brdif dfpss2 an32 anass 3bitr4i exbii exanali eldif bitr4i mpgbir
- con2bii mpbiran eqtri ) UAACZBCZUBZVTUCZDZVTWAEZUDAUEZBUFZFGHFUGZUHZIJUIZ
- KZUJZKZBAUKWGWMLWFWAWMEZULBWFBWMUNWFWAWLEZQZWNWOWFWOVTWAWKMZANZWFQZAWAWKB
- OZUMWRWDWEQZDZANWSWQXBAVTWAWIMZVTWAWJMZQZDVTWAUOZWCDZVTWALZQZXADZDZWQXBXC
- XGXEXJXCVTWAGMZVTWAWHMZDXGVTWAGWHUPXLXFXMWCVTWAWTUQXMVTHEZWCXMXNWAFEZWTVT
- WAHFURUSVTAOUTRPRXHWESZXJXDXHWEVAXDVTWAIMZVTWAJMZSXPVTWAIJVBXQXHXRWEVTWAW
- TVCBVTVDVFRVEPVTWAWIWJVGXBXGXIDZXADXKWDXSXAWDXFXIDZWCDXSWBXTWCVTWAVHTXFXI
- WCVIRTXGXIXAVJRVKVLWDWEAVMRRVQWNXOWPWTWAFWLVNVRVOVPVS $.
+ eqabcb wss brin brsset brxp mpbiran2 eltrans ioran brun ideq epel orbi12i
+ brdif dfpss2 an32 anass 3bitr4i exbii exanali con2bii eldif bitr4i mpgbir
+ xchnxbir mpbiran eqtri ) UAACZBCZUBZVTUCZDZVTWAEZUDAUEZBUFZFGHFUGZUHZIJUI
+ ZKZUJZKZBAUKWGWMLWFWAWMEZULBWFBWMUNWFWAWLEZQZWNWOWFWOVTWAWKMZANZWFQZAWAWK
+ BOZUMWRWDWEQZDZANWSWQXBAVTWAWIMZVTWAWJMZQZDVTWAUOZWCDZVTWALZQZXADZDZWQXBX
+ CXGXEXJXCVTWAGMZVTWAWHMZDXGVTWAGWHUPXLXFXMWCVTWAWTUQXMVTHEZWCXMXNWAFEZWTV
+ TWAHFURUSVTAOUTRPRXHWESZXJXDXHWEVAXDVTWAIMZVTWAJMZSXPVTWAIJVBXQXHXRWEVTWA
+ WTVCBVTVDVERVQPVTWAWIWJVFXBXGXIDZXADXKWDXSXAWDXFXIDZWCDXSWBXTWCVTWAVGTXFX
+ IWCVHRTXGXIXAVIRVJVKWDWEAVLRRVMWNXOWPWTWAFWLVNVRVOVPVS $.
$}
$( Another quantifier-free definition of ` On ` . (Contributed by Scott
@@ -547024,15 +547017,15 @@ Set induction (or epsilon induction)
Fenton, 19-Feb-2013.) $)
dfiota3 $p |- ( iota x ph ) = U. U. ( { { x | ph } } i^i Singletons ) $=
( vy vz vw cab cv csn wceq cuni csingles cin wex wcel ceqsexv bitri exbii
- wa weq eqtri cio df-iota wb eqabc wel exdistr vex sneq eqeq2d vsnex eqeq1
- eleq2 anbi12d eqcom velsn equcom bitrdi an13 bitr3i excom eluniab 3bitr4i
- anbi12ci mpgbir df-sn dfsingles2 ineq12i inab 19.42v bicomi unieqi eqtr4i
- abbii ) ABUAABFZCGZHZIZCFZJVNHZKLZJZJABCUBVRWAVRDGZVNIZWBEGZHZIZRZEMZDFZJ
- ZWAVRWJIVQVOWJNZUCCVQCWJUDCDUEZWGRZEMDMZWLWHRDMVQWKWLWGDEUFVQWMDMZEMZWNVQ
- ECSZVNWEIZRZEMWPWRVQEVOCUGWQWEVPVNWDVOUHUIOWSWOEWSWFWCWLRZRZDMWOWTWSDWEEU
- JWFWTWEVNIZVOWENZRWSWFWCXBWLXCWBWEVNUKWBWEVOULUMXBWRXCWQWEVNUNXCCESWQCWDU
- OCEUPPVCUQOXAWMDWFWCWLURQUSQUSWMEDUTPWHDVOVAVBVDVTWIVTWCDFZWFEMZDFZLZWIVS
- XDKXFDVNVEDEVFVGXGWCXERZDFWIWCXEDVHXHWHDWHXHWCWFEVIVJVMTTVKVLVKT $.
+ wa weq eqtri cio df-iota wb eqabcb wel exdistr vex sneq vsnex eqeq1 eleq2
+ eqeq2d anbi12d eqcom velsn equcom bitrdi an13 bitr3i excom eluniab mpgbir
+ anbi12ci 3bitr4i df-sn dfsingles2 ineq12i inab 19.42v bicomi abbii unieqi
+ eqtr4i ) ABUAABFZCGZHZIZCFZJVNHZKLZJZJABCUBVRWAVRDGZVNIZWBEGZHZIZRZEMZDFZ
+ JZWAVRWJIVQVOWJNZUCCVQCWJUDCDUEZWGRZEMDMZWLWHRDMVQWKWLWGDEUFVQWMDMZEMZWNV
+ QECSZVNWEIZRZEMWPWRVQEVOCUGWQWEVPVNWDVOUHULOWSWOEWSWFWCWLRZRZDMWOWTWSDWEE
+ UIWFWTWEVNIZVOWENZRWSWFWCXBWLXCWBWEVNUJWBWEVOUKUMXBWRXCWQWEVNUNXCCESWQCWD
+ UOCEUPPVCUQOXAWMDWFWCWLURQUSQUSWMEDUTPWHDVOVAVDVBVTWIVTWCDFZWFEMZDFZLZWIV
+ SXDKXFDVNVEDEVFVGXGWCXERZDFWIWCXEDVHXHWHDWHXHWCWFEVIVJVKTTVLVMVLT $.
$}
${
@@ -560682,8 +560675,8 @@ FOL part ( ~ bj-ru0 ) and then two versions ( ~ bj-ru1 and ~ bj-ru ).
$( A version of Russell's paradox ~ ru (see also ~ bj-ru ). (Contributed
by BJ, 12-Oct-2019.) (Proof modification is discouraged.) $)
bj-ru1 $p |- -. E. y y = { x | -. x e. x } $=
- ( cv wel wn cab wceq wb wal bj-ru0 eqab mtbir nex ) BCZAADEZAFGZBPABDOHAI
- ABJOANKLM $.
+ ( cv wel wn cab wceq wb wal bj-ru0 eqabb mtbir nex ) BCZAADEZAFGZBPABDOHA
+ IABJOANKLM $.
$}
${
@@ -561452,7 +561445,7 @@ sethood hypotheses (compare ~ opth ). (Contributed by BJ, 6-Oct-2018.) $)
${
$d A x $. $d V x $.
- $( Relative form of ~ eqab . (Contributed by BJ, 27-Dec-2023.) $)
+ $( Relative form of ~ eqabb . (Contributed by BJ, 27-Dec-2023.) $)
bj-reabeq $p |- ( ( V i^i A ) = { x e. V | ph } <->
A. x e. V ( x e. A <-> ph ) ) $=
( cin crab wceq cv wcel wb wral dfrab3 eqeq2i nfcv nfab1 bj-rcleqf bibi2i
@@ -561530,8 +561523,8 @@ equivalent to the existence of binary unions and of nullary unions (the
(Contributed by BJ, 18-Jan-2025.)
(Proof modification is discouraged.) $)
bj-abex $p |- ( { x | ph } e. _V <-> E. y A. x ( x e. y <-> ph ) ) $=
- ( cab cvv wcel cv wceq wex wel wb wal isset eqab exbii bitri ) ABDZEFCGZQ
- HZCIBCJAKBLZCICQMSTCABRNOP $.
+ ( cab cvv wcel cv wceq wex wel wb wal isset eqabb exbii bitri ) ABDZEFCGZ
+ QHZCIBCJAKBLZCICQMSTCABRNOP $.
$}
${
@@ -659030,73 +659023,73 @@ fixed reference functional determined by this vector (corresponding to
nfv 3ad2ant1 lttri4d simp3 sseli simprd simpl3 breq1 breq1d imbi12d breq2
cdm breq2d rspc2v mpd cle sylib 3expa 3adantl2 ltned necomd neeq1d simpl2
lttrd 3jaodan neneqd wrex ralnex nnel fvelrnb bitrd con1bid elnelne1 ltso
- wor fzfid ssrab2 ssfi rabeq0 ralbii cab wal eqab spi biimpi eqfnfv bicomd
- mpbi biimpd sylan2b necon3d nnssre 3jca fiinfcl eleq1d elrab3 ssrd lttri2
- w3o simp2 3ad2ant2 ltnled infrefilb 3expia con3d elrabf notbii ianor imor
- eqeltrd sylibr eqcomd jaodan ) AGJUCZGKUCZSUDZUWBUWASUDZUEZJUFZKUFZUGZAUW
- AUWBUGZUWEAGDUHZJUCZUWJKUCZUGZDUIHUJUKZULZTZUWIAGUWOUMSUNZUWOGUWQUOZARUPZ
- AUMSUUBZUWOURTZUWOUQUGZUWOUMUSZUTUWQUWOTUWTAUUAUPAUXAUXBUXCAUWNURTUWOUWNU
- SZUXAAUIHUUCUXDAUWMDUWNUUDUPZUWNUWOUUEVAZAJKUGZUXBQAUXGUXBAUWOUQJKAUWOUQU
- OZJKUOZUXHAUWKUWLUOZDUWNVBZUXIUXHUWMVCZDUWNVBUXKUWMDUWNUUFUXLUXJDUWNUWKUW
- LVDUUGVEAUXKUXIAUXKVFZUXKUXIUXMUXIUXKUXMJUWNVGZKUWNVGZUXIUXKVHAUXNUXKAUWN
- UIIUJUKZJAUWNUXPJVIZBUHZCUHZSUDZUXRJUCZUXSJUCZSUDZVJZCUWNVBBUWNVBZAUWNUXP
- FUHZVIZUXTUXRUYFUCZUXSUYFUCZSUDZVJZCUWNVBBUWNVBZVFZUXQUYEVFFEJUYFJUOZUYGU
- XQUYLUYEUWNUXPUYFJVKUYNUYKUYDBCUWNUWNUYNUYJUYCUXTUYNUYHUYAUYIUYBSUXRUYFJV
- NUXSUYFJVNVLVMVOVPAUYMFEUYFETZUYMAUYOUYMUYOUYMVHZFEUYMFUUHUOUYPFUUINUYMFE
- UUJUUOUUKUULVQVRZOVSZVTZWAZWDAUXOUXKAUWNUXPKAUWNUXPKVIZUXTUXRKUCZUXSKUCZS
- UDZVJZCUWNVBBUWNVBZAKETZVUAVUFVFZPAVUHVUGAUYMVUHFEKUYFKUOZUYGVUAUYLVUFUWN
- UXPUYFKVKVUIUYKVUEBCUWNUWNVUIUYJVUDUXTVUIUYHVUBUYIVUCSUXRUYFKVNUXSUYFKVNV
- LVMVOVPUYQPVSZWDWBVTZWAZWDDUWNJKUUMVAUUNUUPWCUUQWEUURWFWBAUWOUWNUMUXEAUWN
- WGUMUWNWGUSAHWHUPWGUMUSAUUSUPWIZWIZUUTUMUWOSUVAVAZUVQAGUWNTZUWPUWIVHAVUPU
- WQUWNTAUWOUWNUWQUXEVUOWJAGUWQUWNUWSUVBWKZUWMUWIDGUWNUWJGUOUWKUWAUWLUWBUWJ
- GJWLUWJGKWLWMUVCWNWOZAUWAUMTZUWBUMTZUWIUWEVHAUXPUMUWAAUAUXPUMAUAXHUAUXPWP
- UAUMWPAUAUHZUXPTZVVAUMTZAVVBVFVVAWGTZVVCVVBVVDAVVAIWQVQVVAWRWNWEUVDZAUWNU
- XPGJUYSVUQWSWJZAUXPUMUWBVVEAUWNUXPGKVUKVUQWSWJZUWAUWBUVEVAWOAUWCUWHUWDAUW
- CVFZUWAUWFTZUWAUWGWTZUWHVVHJXAZGJXSZTZVVIAVVKUWCAUWNUXPJUYSXBWDAVVMUWCAGU
- WNVVLVUQAUWNUXPJUYSXCXDWDGJXEVAVVHUBUHZKUCZUWAUOZVCZUBUWNVBZVVJVVHVVQUBUW
- NVVHVVNUWNTZVFVVOUWAAUWCVVSVVOUWAUGZAUWCVVSUTZVVNGSUDZVVNGUOZGVVNSUDZUVFZ
- VVTVWAVVNGVWAVVNVVSAVVNWGTZUWCVVNHWQZXFXGAUWCGUMTZVVSAUWNUMGVUMVUQWJZXIXJ
- VWAVWBVVTVWCVWDVWAVWBVFZVVOUWAVWAVVOUMTZVWBVWAVVOUXPTZVWKVWAUWNUXPVVNKAUW
- CVUAVVSVUKXIAUWCVVSXKZWSVWLVVOWGTVWKUXPWGVVOIWHZXLVVOWRWNWNZWDVWJVVOUWASU
- DVVNJUCZUWASUDZVWAVWBVWQVWJUYEVWBVWQVJZVWAUYEVWBAUWCUYEVVSAUXQUYEUYRXMZXI
- WDVWJVVSVUPUYEVWRVJAUWCVVSVWBXNVWAVUPVWBAUWCVUPVVSVUQXIZWDUYDVWRVVNUXSSUD
- ZVWPUYBSUDZVJBCVVNGUWNUWNUXRVVNUOZUXTVXAUYCVXBUXRVVNUXSSXOZVXCUYAVWPUYBSU
- XRVVNJWLXPXQUXSGUOZVXAVWBVXBVWQUXSGVVNSXRZVXEUYBUWAVWPSUXSGJWLXTXQYAVAYBW
- CVWJVVOVWPUWASVWJVWPVVOAVVSVWBVWPVVOUOZUWCAVVSVWBVXGAVVSVWBUTZVVSVXGAVVSV
- WBUVGVXHVVSVFVWPVVOUGZVCZVXGVXHVVSVXJVXHVVSVCVXJUEZVVSVXJVJVXHVVNUWOTZVCZ
- VXKVXHGVVNYCUDZVCZVXMVXHVWBVXOAVVSVWBXKVXHVVNGVXHVVNVVSAVWFVWBVWGUVHXGAVV
- SVWHVWBVWIXIUVIWOVXHVXLVXNVXHVXLVXNVXHVXLVFZVXNUWQVVNYCUDZVXHVXLVXQVXHUXC
- UXAVXLVXQVJAVVSUXCVWBVUNXIAVVSUXAVWBUXFXIUXCUXAVXLVXQVVNUWOUVJUVKVAWFVXPG
- UWQVVNYCUWRVXPRUPXPWKWEUVLYBVXMVVSVXIVFZVCVXKVXLVXRUWMVXIDVVNUWNDVVNWPDUW
- NWPVXIDXHUWJVVNUOUWKVWPUWLVVOUWJVVNJWLUWJVVNKWLWMUVMUVNVVSVXIUVOVEYDVVSVX
- JUVPUVRWFVWPVVOVDYDWBYEZYFUVSXPWKYGVWAVWCVFZVVTUWBUWAUGZVXTUWAUWBVWAUWIVW
- CAUWCUWIVVSVURXIWDYHVWCVVTVYAVHVWAVWCVVOUWBUWAVVNGKWLYIVQWKVWAVWDVFZUWAVV
- OVYBUWAVVOVWAVUSVWDAUWCVUSVVSVVFXIWDZVYBUWAUWBVVOVYCVWAVUTVWDAUWCVUTVVSVV
- GXIWDVWAVWKVWDVWOWDAUWCVVSVWDYJVWAVWDUWBVVOSUDZVYBVUFVWDVYDVJZVWAVUFVWDAU
- WCVUFVVSAVUAVUFVUJXMZXIWDVYBVUPVVSVUFVYEVJVWAVUPVWDVWTWDVWAVVSVWDVWMWDVUE
- VYEGUXSSUDZUWBVUCSUDZVJBCGVVNUWNUWNUXRGUOZUXTVYGVUDVYHUXRGUXSSXOZVYIVUBUW
- BVUCSUXRGKWLXPXQUXSVVNUOZVYGVWDVYHVYDUXSVVNGSXRZVYKVUCVVOUWBSUXSVVNKWLXTX
- QYAVAYBWCYKYGYHYLWBYEYMVRAVVRVVJVHUWCAVVRVVPUBUWNYNZVCZVVJVVRVYNVHAVVPUBU
- WNYOUPAVVJVYMAVVJVCZUWAUWGTZVYMVYOVYPVHAUWAUWGYPUPAUXOVYPVYMVHVULUBUWNUWA
- KYQWNYRYSYRWDWOUWAUWFUWGYTVAAUWDVFZUWBUWGTZUWBUWFWTZUWHVYQKXAZGKXSZTZVYRA
- VYTUWDAUWNUXPKVUKXBWDAWUBUWDAGUWNWUAVUQAUWNUXPKVUKXCXDWDGKXEVAVYQVWPUWBUO
- ZVCZUBUWNVBZVYSVYQWUDUBUWNVYQVVSVFVWPUWBAUWDVVSVWPUWBUGZAUWDVVSUTZVWEWUFW
- UGVVNGWUGVVNVVSAVWFUWDVWGXFXGAUWDVWHVVSVWIXIXJWUGVWBWUFVWCVWDWUGVWBVFZVWP
- UWBWUGVWPUMTZVWBWUGVWPWUGVWPUXPTVWPWGTWUGUWNUXPVVNJAUWDUXQVVSUYSXIAUWDVVS
- XKZWSUXPWGVWPVWNXLWNXGZWDWUHVWPUWBSUDVVOUWBSUDZWUGVWBWULWUHVUFVWBWULVJZWU
- GVUFVWBAUWDVUFVVSVYFXIWDWUHVVSVUPVUFWUMVJAUWDVVSVWBXNWUGVUPVWBAUWDVUPVVSV
- UQXIZWDVUEWUMVXAVVOVUCSUDZVJBCVVNGUWNUWNVXCUXTVXAVUDWUOVXDVXCVUBVVOVUCSUX
- RVVNKWLXPXQVXEVXAVWBWUOWULVXFVXEVUCUWBVVOSUXSGKWLXTXQYAVAYBWCWUHVWPVVOUWB
- SAVVSVWBVXGUWDVXSYFXPWKYGWUGVWCVFZWUFUWIWUPUWBUWAWUPUWBUWAWUGVUTVWCAUWDVU
- TVVSVVGXIZWDAUWDVVSVWCYJYGYHVWCWUFUWIVHWUGVWCVWPUWAUWBVVNGJWLYIVQWKWUGVWD
- VFZUWBVWPWURUWBVWPWUGVUTVWDWUQWDZWURUWBUWAVWPWUSWUGVUSVWDAUWDVUSVVSVVFXIW
- DWUGWUIVWDWUKWDAUWDVVSVWDYJWUGVWDUWAVWPSUDZWURUYEVWDWUTVJZWUGUYEVWDAUWDUY
- EVVSVWSXIWDWURVUPVVSUYEWVAVJWUGVUPVWDWUNWDWUGVVSVWDWUJWDUYDWVAVYGUWAUYBSU
- DZVJBCGVVNUWNUWNVYIUXTVYGUYCWVBVYJVYIUYAUWAUYBSUXRGJWLXPXQVYKVYGVWDWVBWUT
- VYLVYKUYBVWPUWASUXSVVNJWLXTXQYAVAYBWCYKYGYHYLWBYEYMVRAWUEVYSVHUWDAWUEWUCU
- BUWNYNZVCZVYSWUEWVDVHAWUCUBUWNYOUPAVYSWVCAVYSVCZUWBUWFTZWVCWVEWVFVHAUWBUW
- FYPUPAUXNWVFWVCVHUYTUBUWNUWBJYQWNYRYSYRWDWOVYRVYSVFUWGUWFUWBUWGUWFYTYHVAU
- VTWB $.
+ wor fzfid ssrab2 ssfi rabeq0 ralbii cab wal mpbi spi biimpi eqfnfv bicomd
+ biimpd sylan2b necon3d nnssre 3jca fiinfcl eqeltrd eleq1d elrab3 ssrd w3o
+ eqabb lttri2 simp2 ltnled infrefilb 3expia con3d elrabf notbii ianor imor
+ 3ad2ant2 sylibr eqcomd jaodan ) AGJUCZGKUCZSUDZUWBUWASUDZUEZJUFZKUFZUGZAU
+ WAUWBUGZUWEAGDUHZJUCZUWJKUCZUGZDUIHUJUKZULZTZUWIAGUWOUMSUNZUWOGUWQUOZARUP
+ ZAUMSUUBZUWOURTZUWOUQUGZUWOUMUSZUTUWQUWOTUWTAUUAUPAUXAUXBUXCAUWNURTUWOUWN
+ USZUXAAUIHUUCUXDAUWMDUWNUUDUPZUWNUWOUUEVAZAJKUGZUXBQAUXGUXBAUWOUQJKAUWOUQ
+ UOZJKUOZUXHAUWKUWLUOZDUWNVBZUXIUXHUWMVCZDUWNVBUXKUWMDUWNUUFUXLUXJDUWNUWKU
+ WLVDUUGVEAUXKUXIAUXKVFZUXKUXIUXMUXIUXKUXMJUWNVGZKUWNVGZUXIUXKVHAUXNUXKAUW
+ NUIIUJUKZJAUWNUXPJVIZBUHZCUHZSUDZUXRJUCZUXSJUCZSUDZVJZCUWNVBBUWNVBZAUWNUX
+ PFUHZVIZUXTUXRUYFUCZUXSUYFUCZSUDZVJZCUWNVBBUWNVBZVFZUXQUYEVFFEJUYFJUOZUYG
+ UXQUYLUYEUWNUXPUYFJVKUYNUYKUYDBCUWNUWNUYNUYJUYCUXTUYNUYHUYAUYIUYBSUXRUYFJ
+ VNUXSUYFJVNVLVMVOVPAUYMFEUYFETZUYMAUYOUYMUYOUYMVHZFEUYMFUUHUOUYPFUUINUYMF
+ EUVFUUJUUKUULVQVRZOVSZVTZWAZWDAUXOUXKAUWNUXPKAUWNUXPKVIZUXTUXRKUCZUXSKUCZ
+ SUDZVJZCUWNVBBUWNVBZAKETZVUAVUFVFZPAVUHVUGAUYMVUHFEKUYFKUOZUYGVUAUYLVUFUW
+ NUXPUYFKVKVUIUYKVUEBCUWNUWNVUIUYJVUDUXTVUIUYHVUBUYIVUCSUXRUYFKVNUXSUYFKVN
+ VLVMVOVPUYQPVSZWDWBVTZWAZWDDUWNJKUUMVAUUNUUOWCUUPWEUUQWFWBAUWOUWNUMUXEAUW
+ NWGUMUWNWGUSAHWHUPWGUMUSAUURUPWIZWIZUUSUMUWOSUUTVAZUVAAGUWNTZUWPUWIVHAVUP
+ UWQUWNTAUWOUWNUWQUXEVUOWJAGUWQUWNUWSUVBWKZUWMUWIDGUWNUWJGUOUWKUWAUWLUWBUW
+ JGJWLUWJGKWLWMUVCWNWOZAUWAUMTZUWBUMTZUWIUWEVHAUXPUMUWAAUAUXPUMAUAXHUAUXPW
+ PUAUMWPAUAUHZUXPTZVVAUMTZAVVBVFVVAWGTZVVCVVBVVDAVVAIWQVQVVAWRWNWEUVDZAUWN
+ UXPGJUYSVUQWSWJZAUXPUMUWBVVEAUWNUXPGKVUKVUQWSWJZUWAUWBUVGVAWOAUWCUWHUWDAU
+ WCVFZUWAUWFTZUWAUWGWTZUWHVVHJXAZGJXSZTZVVIAVVKUWCAUWNUXPJUYSXBWDAVVMUWCAG
+ UWNVVLVUQAUWNUXPJUYSXCXDWDGJXEVAVVHUBUHZKUCZUWAUOZVCZUBUWNVBZVVJVVHVVQUBU
+ WNVVHVVNUWNTZVFVVOUWAAUWCVVSVVOUWAUGZAUWCVVSUTZVVNGSUDZVVNGUOZGVVNSUDZUVE
+ ZVVTVWAVVNGVWAVVNVVSAVVNWGTZUWCVVNHWQZXFXGAUWCGUMTZVVSAUWNUMGVUMVUQWJZXIX
+ JVWAVWBVVTVWCVWDVWAVWBVFZVVOUWAVWAVVOUMTZVWBVWAVVOUXPTZVWKVWAUWNUXPVVNKAU
+ WCVUAVVSVUKXIAUWCVVSXKZWSVWLVVOWGTVWKUXPWGVVOIWHZXLVVOWRWNWNZWDVWJVVOUWAS
+ UDVVNJUCZUWASUDZVWAVWBVWQVWJUYEVWBVWQVJZVWAUYEVWBAUWCUYEVVSAUXQUYEUYRXMZX
+ IWDVWJVVSVUPUYEVWRVJAUWCVVSVWBXNVWAVUPVWBAUWCVUPVVSVUQXIZWDUYDVWRVVNUXSSU
+ DZVWPUYBSUDZVJBCVVNGUWNUWNUXRVVNUOZUXTVXAUYCVXBUXRVVNUXSSXOZVXCUYAVWPUYBS
+ UXRVVNJWLXPXQUXSGUOZVXAVWBVXBVWQUXSGVVNSXRZVXEUYBUWAVWPSUXSGJWLXTXQYAVAYB
+ WCVWJVVOVWPUWASVWJVWPVVOAVVSVWBVWPVVOUOZUWCAVVSVWBVXGAVVSVWBUTZVVSVXGAVVS
+ VWBUVHVXHVVSVFVWPVVOUGZVCZVXGVXHVVSVXJVXHVVSVCVXJUEZVVSVXJVJVXHVVNUWOTZVC
+ ZVXKVXHGVVNYCUDZVCZVXMVXHVWBVXOAVVSVWBXKVXHVVNGVXHVVNVVSAVWFVWBVWGUVQXGAV
+ VSVWHVWBVWIXIUVIWOVXHVXLVXNVXHVXLVXNVXHVXLVFZVXNUWQVVNYCUDZVXHVXLVXQVXHUX
+ CUXAVXLVXQVJAVVSUXCVWBVUNXIAVVSUXAVWBUXFXIUXCUXAVXLVXQVVNUWOUVJUVKVAWFVXP
+ GUWQVVNYCUWRVXPRUPXPWKWEUVLYBVXMVVSVXIVFZVCVXKVXLVXRUWMVXIDVVNUWNDVVNWPDU
+ WNWPVXIDXHUWJVVNUOUWKVWPUWLVVOUWJVVNJWLUWJVVNKWLWMUVMUVNVVSVXIUVOVEYDVVSV
+ XJUVPUVRWFVWPVVOVDYDWBYEZYFUVSXPWKYGVWAVWCVFZVVTUWBUWAUGZVXTUWAUWBVWAUWIV
+ WCAUWCUWIVVSVURXIWDYHVWCVVTVYAVHVWAVWCVVOUWBUWAVVNGKWLYIVQWKVWAVWDVFZUWAV
+ VOVYBUWAVVOVWAVUSVWDAUWCVUSVVSVVFXIWDZVYBUWAUWBVVOVYCVWAVUTVWDAUWCVUTVVSV
+ VGXIWDVWAVWKVWDVWOWDAUWCVVSVWDYJVWAVWDUWBVVOSUDZVYBVUFVWDVYDVJZVWAVUFVWDA
+ UWCVUFVVSAVUAVUFVUJXMZXIWDVYBVUPVVSVUFVYEVJVWAVUPVWDVWTWDVWAVVSVWDVWMWDVU
+ EVYEGUXSSUDZUWBVUCSUDZVJBCGVVNUWNUWNUXRGUOZUXTVYGVUDVYHUXRGUXSSXOZVYIVUBU
+ WBVUCSUXRGKWLXPXQUXSVVNUOZVYGVWDVYHVYDUXSVVNGSXRZVYKVUCVVOUWBSUXSVVNKWLXT
+ XQYAVAYBWCYKYGYHYLWBYEYMVRAVVRVVJVHUWCAVVRVVPUBUWNYNZVCZVVJVVRVYNVHAVVPUB
+ UWNYOUPAVVJVYMAVVJVCZUWAUWGTZVYMVYOVYPVHAUWAUWGYPUPAUXOVYPVYMVHVULUBUWNUW
+ AKYQWNYRYSYRWDWOUWAUWFUWGYTVAAUWDVFZUWBUWGTZUWBUWFWTZUWHVYQKXAZGKXSZTZVYR
+ AVYTUWDAUWNUXPKVUKXBWDAWUBUWDAGUWNWUAVUQAUWNUXPKVUKXCXDWDGKXEVAVYQVWPUWBU
+ OZVCZUBUWNVBZVYSVYQWUDUBUWNVYQVVSVFVWPUWBAUWDVVSVWPUWBUGZAUWDVVSUTZVWEWUF
+ WUGVVNGWUGVVNVVSAVWFUWDVWGXFXGAUWDVWHVVSVWIXIXJWUGVWBWUFVWCVWDWUGVWBVFZVW
+ PUWBWUGVWPUMTZVWBWUGVWPWUGVWPUXPTVWPWGTWUGUWNUXPVVNJAUWDUXQVVSUYSXIAUWDVV
+ SXKZWSUXPWGVWPVWNXLWNXGZWDWUHVWPUWBSUDVVOUWBSUDZWUGVWBWULWUHVUFVWBWULVJZW
+ UGVUFVWBAUWDVUFVVSVYFXIWDWUHVVSVUPVUFWUMVJAUWDVVSVWBXNWUGVUPVWBAUWDVUPVVS
+ VUQXIZWDVUEWUMVXAVVOVUCSUDZVJBCVVNGUWNUWNVXCUXTVXAVUDWUOVXDVXCVUBVVOVUCSU
+ XRVVNKWLXPXQVXEVXAVWBWUOWULVXFVXEVUCUWBVVOSUXSGKWLXTXQYAVAYBWCWUHVWPVVOUW
+ BSAVVSVWBVXGUWDVXSYFXPWKYGWUGVWCVFZWUFUWIWUPUWBUWAWUPUWBUWAWUGVUTVWCAUWDV
+ UTVVSVVGXIZWDAUWDVVSVWCYJYGYHVWCWUFUWIVHWUGVWCVWPUWAUWBVVNGJWLYIVQWKWUGVW
+ DVFZUWBVWPWURUWBVWPWUGVUTVWDWUQWDZWURUWBUWAVWPWUSWUGVUSVWDAUWDVUSVVSVVFXI
+ WDWUGWUIVWDWUKWDAUWDVVSVWDYJWUGVWDUWAVWPSUDZWURUYEVWDWUTVJZWUGUYEVWDAUWDU
+ YEVVSVWSXIWDWURVUPVVSUYEWVAVJWUGVUPVWDWUNWDWUGVVSVWDWUJWDUYDWVAVYGUWAUYBS
+ UDZVJBCGVVNUWNUWNVYIUXTVYGUYCWVBVYJVYIUYAUWAUYBSUXRGJWLXPXQVYKVYGVWDWVBWU
+ TVYLVYKUYBVWPUWASUXSVVNJWLXTXQYAVAYBWCYKYGYHYLWBYEYMVRAWUEVYSVHUWDAWUEWUC
+ UBUWNYNZVCZVYSWUEWVDVHAWUCUBUWNYOUPAVYSWVCAVYSVCZUWBUWFTZWVCWVEWVFVHAUWBU
+ WFYPUPAUXNWVFWVCVHUYTUBUWNUWBJYQWNYRYSYRWDWOVYRVYSVFUWGUWFUWBUWGUWFYTYHVA
+ UVTWB $.
$}
${
@@ -659116,53 +659109,53 @@ fixed reference functional determined by this vector (corresponding to
sticksstones2 $p |- ( ph -> F : A -1-1-> B ) $=
( cfv wceq wcel clt vi vj vb vs vr wf cv wi wral wa wf1 crn chash cfz cpw
c1 co crab fveqeq2 cfn fzfid wbr eleq1w feq1 fveq1 breq12d imbi2d ralbidv
- wb anbi12d bibi12d cab wal eqab mpbi chvarvv biimpi adantl simpld sselpwd
- spi frnd wfn ffnd hashfn syl cn0 adantr hashfz1 eqtrd eqcomd w3a wo cr cn
+ wb anbi12d bibi12d cab wal eqabb spi chvarvv biimpi adantl simpld sselpwd
+ mpbi frnd wfn hashfn syl cn0 adantr hashfz1 eqtrd eqcomd w3a wne wo cr cn
elfznn 3ad2ant3 nnred lttri2 syl2anc 3adant3 simp3 ffvelcdmd simprd simpr
- wne breq1 fveq2 breq1d imbi12d breq2d rspc2v mpd ffvelcdmda necomd jaodan
- breq2 imp ltned ex sylbid necon4d ralrimiva 3expa jca dff13 sylibr elrabd
- hashf1rn eleq2i a1i mpbird fmptd cinf 3ad2ant1 simpl2 simpl3 rneqd fvmptd
- 2ralbidv neeq12d cbvrabv infeq1i sticksstones1 cmpt 3adant2 3netr4d ) AEF
- HUFZUAUGZHQZUBUGZHQZRUUIUUKRUHZUBEUIZUAEUIZUJEFHUKAUUHUUOADEDUGZULZFHAUUP
- ESZUJZUUQFSZUUQKUGZUMQIRZKUPJUNUQZUOZURZSZUUSUVBUUQUMQZIRKUUQUVDUVAUUQIUM
- USUUSUUQUVCUTUUSUPJVAUUSUPIUNUQZUVCUUPUUSUVHUVCUUPUFZBUGZCUGZTVBZUVJUUPQZ
- UVKUUPQZTVBZUHZCUVHUIZBUVHUIZUURUVIUVRUJZAUURUVSGUGZESZUVHUVCUVTUFZUVLUVJ
- UVTQZUVKUVTQZTVBZUHZCUVHUIZBUVHUIZUJZVIZUURUVSVIGDUVTUUPRZUWAUURUWIUVSGDE
- VCUWKUWBUVIUWHUVRUVHUVCUVTUUPVDUWKUWGUVQBUVHUWKUWFUVPCUVHUWKUWEUVOUVLUWKU
- WCUVMUWDUVNTUVJUVTUUPVEUVKUVTUUPVEVFVGVHVHVJVKUWJGEUWIGVLRUWJGVMOUWIGEVNV
- OWAZVPVQVRZVSZWBVTUUSIUVGUUSIUUPUMQZUVGUUSUWOIUUSUWOUVHUMQZIUUSUUPUVHWCUW
- OUWPRUUSUVHUVCUUPUWNWDUVHUUPWEWFUUSIWGSZUWPIRAUWQUURMWHIWIWFWJWKUUSUVHUTS
- UVHUVCUUPUKZUWOUVGRUUSUPIVAUUSUVIUVAUUPQZUCUGZUUPQZRUVAUWTRUHZUCUVHUIZKUV
- HUIZUJUWRUUSUVIUXDUWNUUSUXCKUVHAUURUVAUVHSZUXCAUURUXEWLZUXBUCUVHUXFUWTUVH
- SZUJZUVAUWTUWSUXAUXHUVAUWTXFZUVAUWTTVBZUWTUVATVBZWMZUWSUXAXFZUXHUVAWNSZUW
- TWNSZUXIUXLVIUXFUXNUXGUXFUVAUXEAUVAWOSUURUVAIWPWQWRWHUXGUXOUXFUXGUWTUWTIW
- PWRVRUVAUWTWSWTUXHUXLUXMUXHUXJUXMUXKUXHUXJUJZUWSUXAUXPUWSUXPUWSUVCSZUWSWO
- SUXHUXQUXJUXFUXQUXGUXFUVHUVCUVAUUPAUURUVIUXEUWNXAZAUURUXEXBZXCWHWHUWSJWPW
- FWRUXHUXJUWSUXATVBZUXHUVRUXJUXTUHZUXFUVRUXGAUURUVRUXEUUSUVIUVRUWMXDXAWHZU
- XHUXEUXGUVRUYAUHUXFUXEUXGUXSWHZUXFUXGXEZUVPUYAUVAUVKTVBZUWSUVNTVBZUHBCUVA
- UWTUVHUVHUVJUVARZUVLUYEUVOUYFUVJUVAUVKTXGUYGUVMUWSUVNTUVJUVAUUPXHXIXJUVKU
- WTRZUYEUXJUYFUXTUVKUWTUVATXQUYHUVNUXAUWSTUVKUWTUUPXHXKXJXLWTXMXRXSUXHUXKU
- JZUXAUWSUYIUXAUWSUXHUXAWNSUXKUXHUXAUXHUXAUVCSUXAWOSUXFUVHUVCUWTUUPUXRXNUX
- AJWPWFWRWHUXHUXKUXAUWSTVBZUXHUVRUXKUYJUHZUYBUXHUXGUXEUVRUYKUHUYDUYCUVPUYK
- UWTUVKTVBZUXAUVNTVBZUHBCUWTUVAUVHUVHUVJUWTRZUVLUYLUVOUYMUVJUWTUVKTXGUYNUV
- MUXAUVNTUVJUWTUUPXHXIXJUVKUVARZUYLUXKUYMUYJUVKUVAUWTTXQUYOUVNUWSUXATUVKUV
- AUUPXHXKXJXLWTXMXRXSXOXPXTYAYBYCYDYCYEKUCUVHUVCUUPYFYGUVHUVCUUPUTYIWTWJWK
- YHUUTUVFVIUUSFUVEUUQNYJYKYLPYMAUUNUAEAUUIESZUJZUUMUBEAUYPUUKESZUUMAUYPUYR
- WLZUUIUUKUUJUULUYSUUIUUKXFZUUJUULXFUYSUYTUJZUUIULZUUKULZUUJUULVUABCUDEGUE
- UGZUUIQZVUDUUKQZXFZUEUVHURZWNTYNIJUUIUUKUYSJWGSZUYTAUYPVUIUYRLYOWHUYSUWQU
- YTAUYPUWQUYRMYOWHOAUYPUYRUYTYPZAUYPUYRUYTYQZUYSUYTXEWNVUHUDUGZUUIQZVULUUK
- QZXFZUDUVHURTVUGVUOUEUDUVHVUDVULRVUEVUMVUFVUNVUDVULUUIXHVUDVULUUKXHUUAUUB
- UUCUUDVUADUUIUUQVUBEHUVDHDEUUQUUERVUAPYKZVUAUUPUUIRZUJUUPUUIVUAVUQXEYRVUJ
- VUAVUBUVCUTVUAUPJVAVUAUVHUVCUUIUYSUVHUVCUUIUFZUYTAUYPVURUYRUYQVURUVLUVJUU
- IQZUVKUUIQZTVBZUHZCUVHUIBUVHUIZUYPVURVVCUJZAUYPVVDUWJUYPVVDVIGUAUVTUUIRZU
- WAUYPUWIVVDGUAEVCVVEUWBVURUWHVVCUVHUVCUVTUUIVDVVEUWFVVBBCUVHUVHVVEUWEVVAU
- VLVVEUWCVUSUWDVUTTUVJUVTUUIVEUVKUVTUUIVEVFVGYTVJVKUWLVPVQVRVSXAWHWBVTYSVU
- ADUUKUUQVUCEHUVDVUPVUAUUPUUKRZUJUUPUUKVUAVVFXEYRVUKUYSVUCUVDSUYTUYSVUCUVC
- UTAUYPUVCUTSUYRAUPJVAYOUYSUVHUVCUUKAUYRUVHUVCUUKUFZUYPAUYRUJVVGUVLUVJUUKQ
- ZUVKUUKQZTVBZUHZCUVHUIBUVHUIZUYRVVGVVLUJZAUYRVVMUWJUYRVVMVIGUBUVTUUKRZUWA
- UYRUWIVVMGUBEVCVVNUWBVVGUWHVVLUVHUVCUVTUUKVDVVNUWFVVKBCUVHUVHVVNUWEVVJUVL
- VVNUWCVVHUWDVVITUVJUVTUUKVEUVKUVTUUKVEVFVGYTVJVKUWLVPVQVRVSUUFWBVTWHYSUUG
- XTYBYDYCYCYEUAUBEFHYFYG $.
+ ffnd breq1 fveq2 breq1d imbi12d breq2 breq2d rspc2v mpd ffvelcdmda necomd
+ imp ltned jaodan sylbid necon4d ralrimiva 3expa jca dff13 sylibr hashf1rn
+ elrabd eleq2i a1i mpbird fmptd cinf 3ad2ant1 simpl2 simpl3 rneqd 2ralbidv
+ ex fvmptd neeq12d cbvrabv infeq1i sticksstones1 cmpt 3adant2 3netr4d ) AE
+ FHUFZUAUGZHQZUBUGZHQZRUUIUUKRUHZUBEUIZUAEUIZUJEFHUKAUUHUUOADEDUGZULZFHAUU
+ PESZUJZUUQFSZUUQKUGZUMQIRZKUPJUNUQZUOZURZSZUUSUVBUUQUMQZIRKUUQUVDUVAUUQIU
+ MUSUUSUUQUVCUTUUSUPJVAUUSUPIUNUQZUVCUUPUUSUVHUVCUUPUFZBUGZCUGZTVBZUVJUUPQ
+ ZUVKUUPQZTVBZUHZCUVHUIZBUVHUIZUURUVIUVRUJZAUURUVSGUGZESZUVHUVCUVTUFZUVLUV
+ JUVTQZUVKUVTQZTVBZUHZCUVHUIZBUVHUIZUJZVIZUURUVSVIGDUVTUUPRZUWAUURUWIUVSGD
+ EVCUWKUWBUVIUWHUVRUVHUVCUVTUUPVDUWKUWGUVQBUVHUWKUWFUVPCUVHUWKUWEUVOUVLUWK
+ UWCUVMUWDUVNTUVJUVTUUPVEUVKUVTUUPVEVFVGVHVHVJVKUWJGEUWIGVLRUWJGVMOUWIGEVN
+ WAVOZVPVQVRZVSZWBVTUUSIUVGUUSIUUPUMQZUVGUUSUWOIUUSUWOUVHUMQZIUUSUUPUVHWCU
+ WOUWPRUUSUVHUVCUUPUWNXFUVHUUPWDWEUUSIWFSZUWPIRAUWQUURMWGIWHWEWIWJUUSUVHUT
+ SUVHUVCUUPUKZUWOUVGRUUSUPIVAUUSUVIUVAUUPQZUCUGZUUPQZRUVAUWTRUHZUCUVHUIZKU
+ VHUIZUJUWRUUSUVIUXDUWNUUSUXCKUVHAUURUVAUVHSZUXCAUURUXEWKZUXBUCUVHUXFUWTUV
+ HSZUJZUVAUWTUWSUXAUXHUVAUWTWLZUVAUWTTVBZUWTUVATVBZWMZUWSUXAWLZUXHUVAWNSZU
+ WTWNSZUXIUXLVIUXFUXNUXGUXFUVAUXEAUVAWOSUURUVAIWPWQWRWGUXGUXOUXFUXGUWTUWTI
+ WPWRVRUVAUWTWSWTUXHUXLUXMUXHUXJUXMUXKUXHUXJUJZUWSUXAUXPUWSUXPUWSUVCSZUWSW
+ OSUXHUXQUXJUXFUXQUXGUXFUVHUVCUVAUUPAUURUVIUXEUWNXAZAUURUXEXBZXCWGWGUWSJWP
+ WEWRUXHUXJUWSUXATVBZUXHUVRUXJUXTUHZUXFUVRUXGAUURUVRUXEUUSUVIUVRUWMXDXAWGZ
+ UXHUXEUXGUVRUYAUHUXFUXEUXGUXSWGZUXFUXGXEZUVPUYAUVAUVKTVBZUWSUVNTVBZUHBCUV
+ AUWTUVHUVHUVJUVARZUVLUYEUVOUYFUVJUVAUVKTXGUYGUVMUWSUVNTUVJUVAUUPXHXIXJUVK
+ UWTRZUYEUXJUYFUXTUVKUWTUVATXKUYHUVNUXAUWSTUVKUWTUUPXHXLXJXMWTXNXQXRUXHUXK
+ UJZUXAUWSUYIUXAUWSUXHUXAWNSUXKUXHUXAUXHUXAUVCSUXAWOSUXFUVHUVCUWTUUPUXRXOU
+ XAJWPWEWRWGUXHUXKUXAUWSTVBZUXHUVRUXKUYJUHZUYBUXHUXGUXEUVRUYKUHUYDUYCUVPUY
+ KUWTUVKTVBZUXAUVNTVBZUHBCUWTUVAUVHUVHUVJUWTRZUVLUYLUVOUYMUVJUWTUVKTXGUYNU
+ VMUXAUVNTUVJUWTUUPXHXIXJUVKUVARZUYLUXKUYMUYJUVKUVAUWTTXKUYOUVNUWSUXATUVKU
+ VAUUPXHXLXJXMWTXNXQXRXPXSYSXTYAYBYCYBYDKUCUVHUVCUUPYEYFUVHUVCUUPUTYGWTWIW
+ JYHUUTUVFVIUUSFUVEUUQNYIYJYKPYLAUUNUAEAUUIESZUJZUUMUBEAUYPUUKESZUUMAUYPUY
+ RWKZUUIUUKUUJUULUYSUUIUUKWLZUUJUULWLUYSUYTUJZUUIULZUUKULZUUJUULVUABCUDEGU
+ EUGZUUIQZVUDUUKQZWLZUEUVHURZWNTYMIJUUIUUKUYSJWFSZUYTAUYPVUIUYRLYNWGUYSUWQ
+ UYTAUYPUWQUYRMYNWGOAUYPUYRUYTYOZAUYPUYRUYTYPZUYSUYTXEWNVUHUDUGZUUIQZVULUU
+ KQZWLZUDUVHURTVUGVUOUEUDUVHVUDVULRVUEVUMVUFVUNVUDVULUUIXHVUDVULUUKXHUUAUU
+ BUUCUUDVUADUUIUUQVUBEHUVDHDEUUQUUERVUAPYJZVUAUUPUUIRZUJUUPUUIVUAVUQXEYQVU
+ JVUAVUBUVCUTVUAUPJVAVUAUVHUVCUUIUYSUVHUVCUUIUFZUYTAUYPVURUYRUYQVURUVLUVJU
+ UIQZUVKUUIQZTVBZUHZCUVHUIBUVHUIZUYPVURVVCUJZAUYPVVDUWJUYPVVDVIGUAUVTUUIRZ
+ UWAUYPUWIVVDGUAEVCVVEUWBVURUWHVVCUVHUVCUVTUUIVDVVEUWFVVBBCUVHUVHVVEUWEVVA
+ UVLVVEUWCVUSUWDVUTTUVJUVTUUIVEUVKUVTUUIVEVFVGYRVJVKUWLVPVQVRVSXAWGWBVTYTV
+ UADUUKUUQVUCEHUVDVUPVUAUUPUUKRZUJUUPUUKVUAVVFXEYQVUKUYSVUCUVDSUYTUYSVUCUV
+ CUTAUYPUVCUTSUYRAUPJVAYNUYSUVHUVCUUKAUYRUVHUVCUUKUFZUYPAUYRUJVVGUVLUVJUUK
+ QZUVKUUKQZTVBZUHZCUVHUIBUVHUIZUYRVVGVVLUJZAUYRVVMUWJUYRVVMVIGUBUVTUUKRZUW
+ AUYRUWIVVMGUBEVCVVNUWBVVGUWHVVLUVHUVCUVTUUKVDVVNUWFVVKBCUVHUVHVVNUWEVVJUV
+ LVVNUWCVVHUWDVVITUVJUVTUUKVEUVKUVTUUKVEVFVGYRVJVKUWLVPVQVRVSUUFWBVTWGYTUU
+ GYSYAYCYBYBYDUAUBEFHYEYF $.
$}
${
@@ -681132,19 +681125,19 @@ is in the span of P(i)(X), so there is an R-linear combination of
( vx vy vz con0 wss wel wrex wral wn wb wex cep wceq wcel cv elequ1 bitri
wa wal cxp cin cdm cuni elirrv pm5.501 mp1i notbid rexbidv bibi12d bitr4d
weq biimpd spimevw wi ssel adantr imp ssel2 ontri1 ralbidva ralnex bitrdi
- syl2anc unissb simpr elssuni ad2antlr eqssd cab dfuni2 eqeq1i eqabc bicom
- sylan2br albii 3bitri sylib notnotb bibi1i alnex ex sylbird con4d impbid2
- nbbn dminxp epel rexbii ralbii exnal bicomi exbii bitr3i xchnxbir 3bitr4g
- wbr uniel ) AEFZBCGZCAHZBAIZDBGZJZDCGZCAHZKZDLZBAIZMAAUAUBUCANZAUDZAOZJWS
- XAXHBAWSBPZAOZSZXAXHXAXGDBDBULZXAXGXPXABBGZJZXAKZXGXRXAXSKXPBUEXRXAUFUGXP
- XDXRXFXAXPXCXQDBBQUHXPXEWTCADBCQUIUJUKUMUNXOXAXHXOXAJZCPZXMFZCAIZXHJZXOYC
- WTJZCAIXTXOYBYECAXOYAAOZSYAEOZXMEOZYBYEKXOYFYGWSYFYGUOXNAEYAUPUQURXOYHYFA
- EXMUSUQYAXMUTVDVAWTCAVBVCXOYCYDXOYCSZXCXFKZDTZYDYIXKXMNZYKYCXOXKXMFZYLCAX
- MVEXOYMSXKXMXOYMVFXNXMXKFWSYMXMAVGVHVIVOYLXFDVJZXMNXFXCKZDTYKXKYNXMDCAVKV
- LXFDXMVMYOYJDXFXCVNVPVQVRYKXGJZDTYDYJYPDYJXDJZXFKYPXCYQXFXCVSVTXDXFWFRVPX
- GDWARVRWBWCWDWEVAXJXMYAMWQZCAHZBAIXBBCAAMWGYSXABAYRWTCACXMWHWIWJRYKBAHZXI
- XLYTJYKJZBAIXIYKBAVBUUAXHBAUUAYJJZDLXHYJDWKUUBXGDXGUUBXCXFWFWLWMWNWJWNBCD
- AAWRWOWP $.
+ syl2anc unissb simpr elssuni ad2antlr eqssd sylan2br dfuni2 eqeq1i eqabcb
+ cab bicom albii 3bitri sylib notnotb bibi1i nbbn alnex ex sylbird impbid2
+ con4d wbr dminxp rexbii ralbii exnal bicomi exbii bitr3i xchnxbir 3bitr4g
+ epel uniel ) AEFZBCGZCAHZBAIZDBGZJZDCGZCAHZKZDLZBAIZMAAUAUBUCANZAUDZAOZJW
+ SXAXHBAWSBPZAOZSZXAXHXAXGDBDBULZXAXGXPXABBGZJZXAKZXGXRXAXSKXPBUEXRXAUFUGX
+ PXDXRXFXAXPXCXQDBBQUHXPXEWTCADBCQUIUJUKUMUNXOXAXHXOXAJZCPZXMFZCAIZXHJZXOY
+ CWTJZCAIXTXOYBYECAXOYAAOZSYAEOZXMEOZYBYEKXOYFYGWSYFYGUOXNAEYAUPUQURXOYHYF
+ AEXMUSUQYAXMUTVDVAWTCAVBVCXOYCYDXOYCSZXCXFKZDTZYDYIXKXMNZYKYCXOXKXMFZYLCA
+ XMVEXOYMSXKXMXOYMVFXNXMXKFWSYMXMAVGVHVIVJYLXFDVNZXMNXFXCKZDTYKXKYNXMDCAVK
+ VLXFDXMVMYOYJDXFXCVOVPVQVRYKXGJZDTYDYJYPDYJXDJZXFKYPXCYQXFXCVSVTXDXFWARVP
+ XGDWBRVRWCWDWFWEVAXJXMYAMWGZCAHZBAIXBBCAAMWHYSXABAYRWTCACXMWQWIWJRYKBAHZX
+ IXLYTJYKJZBAIXIYKBAVBUUAXHBAUUAYJJZDLXHYJDWKUUBXGDXGUUBXCXFWAWLWMWNWJWNBC
+ DAAWRWOWP $.
$}
$( Unordered past here $)
@@ -696134,14 +696127,14 @@ base set if and only if the neighborhoods (convergents) of every point
scottabf $p |- Scott { x | ph }
= { x | ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) } $=
( vz vw cab cv crnk cfv wss wcel wa wi wal wceq wb eleq1w cscott df-scott
- wral crab df-rab eqabc nfsab1 nfab1 nfv nfan vex abid bitr3id wsb df-clab
- nfralw sbiev bitr2i bitrid adantl fveq2d sseq12d imbi12d cbvaldvaw df-ral
- simpl simpr bitr4di anbi12d elabf bicomi mpgbir 3eqtri ) ACIZUAGJZKLZHJZK
- LZMZHVNUCZGVNUDVOVNNZVTOZGIZABCJZKLZDJZKLZMZPZDQZOZCIZGHVNUBVTGVNUEWCWLRW
- BVOWLNZSGWBGWLUFWMWBWKWBCVOWAVTCACGUGVSCHVNACUHVSCUIUPUJGUKWDVORZAWAWJVTA
- WDVNNWNWAACULCGVNTUMWNWJVQVNNZVSPZHQVTWNWIWPDHWNWFVQRZOZBWOWHVSWQBWOSWNBW
- FVNNZWQWOWSACDUNBADCUOABCDEFUQURDHVNTUSUTWRWEVPWGVRWRWDVOKWNWQVFVAWRWFVQK
- WNWQVGVAVBVCVDVSHVNVEVHVIVJVKVLVM $.
+ wral crab df-rab eqabcb nfsab1 nfab1 nfv nfralw nfan vex abid bitr3id wsb
+ df-clab sbiev bitr2i bitrid adantl simpl fveq2d sseq12d imbi12d cbvaldvaw
+ simpr df-ral bitr4di anbi12d elabf bicomi mpgbir 3eqtri ) ACIZUAGJZKLZHJZ
+ KLZMZHVNUCZGVNUDVOVNNZVTOZGIZABCJZKLZDJZKLZMZPZDQZOZCIZGHVNUBVTGVNUEWCWLR
+ WBVOWLNZSGWBGWLUFWMWBWKWBCVOWAVTCACGUGVSCHVNACUHVSCUIUJUKGULWDVORZAWAWJVT
+ AWDVNNWNWAACUMCGVNTUNWNWJVQVNNZVSPZHQVTWNWIWPDHWNWFVQRZOZBWOWHVSWQBWOSWNB
+ WFVNNZWQWOWSACDUOBADCUPABCDEFUQURDHVNTUSUTWRWEVPWGVRWRWDVOKWNWQVAVBWRWFVQ
+ KWNWQVFVBVCVDVEVSHVNVGVHVIVJVKVLVM $.
$}
${
@@ -711375,13 +711368,13 @@ not even needed (it can be any class). (Contributed by Glauco
( F ` x ) ) ) $=
( vw wfo wceq wa cv cfv wrex cab wb nfcv nfv wcel wal wi wf crn dffo2 wfn
wral ffn fnrnfv nffv nfeq2 fveq2 eqeq2d cbvrexw abbii eqtrdi eqeq1d dfbi2
- syl simpr ffvelcdm adantr eqeltrd rexlimd3 biantrurd bitr4id albidv eqabc
- nff df-ral 3bitr4g bitrd pm5.32i bitri ) CDEHCDEUAZEUBZDIZJVMBKZAKZELZIZA
- CMZBDUEZJCDEUCVMVOWAVMVOVTBNZDIZWAVMECUDZVOWCOCDEUFWDVNWBDWDVNVPGKZELZIZG
- CMZBNWBGBCEUGWHVTBWGVSGACAVPWFAWEEFAWEPUHUIVSGQWEVQIWFVRVPWEVQEUJUKULUMUN
- UOUQVMVTVPDRZOZBSWIVTTZBSWCWAVMWJWKBVMWJVTWITZWKJWKVTWIUPVMWLWKVMVSWIACAC
- DEFACPADPVGWIAQVMVQCRJZVSJVPVRDWMVSURWMVRDRVSCDVQEUSUTVAVBVCVDVEVTBDVFVTB
- DVHVIVJVKVL $.
+ syl simpr ffvelcdm adantr eqeltrd rexlimd3 biantrurd albidv eqabcb df-ral
+ nff bitr4id 3bitr4g bitrd pm5.32i bitri ) CDEHCDEUAZEUBZDIZJVMBKZAKZELZIZ
+ ACMZBDUEZJCDEUCVMVOWAVMVOVTBNZDIZWAVMECUDZVOWCOCDEUFWDVNWBDWDVNVPGKZELZIZ
+ GCMZBNWBGBCEUGWHVTBWGVSGACAVPWFAWEEFAWEPUHUIVSGQWEVQIWFVRVPWEVQEUJUKULUMU
+ NUOUQVMVTVPDRZOZBSWIVTTZBSWCWAVMWJWKBVMWJVTWITZWKJWKVTWIUPVMWLWKVMVSWIACA
+ CDEFACPADPVGWIAQVMVQCRJZVSJVPVRDWMVSURWMVRDRVSCDVQEUSUTVAVBVCVHVDVTBDVEVT
+ BDVFVIVJVKVL $.
$}
${