diff --git a/discouraged b/discouraged
index e5f69ec296..41c6092513 100755
--- a/discouraged
+++ b/discouraged
@@ -13673,6 +13673,7 @@ New usage of "ax6fromc10" is discouraged (1 uses).
New usage of "ax6vsep" is discouraged (0 uses).
New usage of "ax7v" is discouraged (2 uses).
New usage of "ax8v" is discouraged (2 uses).
+New usage of "ax9ALT" is discouraged (0 uses).
New usage of "ax9v" is discouraged (2 uses).
New usage of "axac2" is discouraged (0 uses).
New usage of "axacnd" is discouraged (2 uses).
@@ -13808,6 +13809,7 @@ New usage of "bj-0" is discouraged (1 uses).
New usage of "bj-1" is discouraged (0 uses).
New usage of "bj-ax12v3ALT" is discouraged (0 uses).
New usage of "bj-ax6e" is discouraged (0 uses).
+New usage of "bj-ax9" is discouraged (0 uses).
New usage of "bj-axc4" is discouraged (0 uses).
New usage of "bj-axd2d" is discouraged (0 uses).
New usage of "bj-axdd2" is discouraged (0 uses).
@@ -18286,6 +18288,7 @@ Proof modification of "ax6e2ndeqALT" is discouraged (342 steps).
Proof modification of "ax6e2ndeqVD" is discouraged (340 steps).
Proof modification of "ax6fromc10" is discouraged (24 steps).
Proof modification of "ax6vsep" is discouraged (73 steps).
+Proof modification of "ax9ALT" is discouraged (68 steps).
Proof modification of "axac" is discouraged (55 steps).
Proof modification of "axac2" is discouraged (108 steps).
Proof modification of "axac3" is discouraged (74 steps).
@@ -18370,9 +18373,7 @@ Proof modification of "bj-ax12v3ALT" is discouraged (44 steps).
Proof modification of "bj-ax6e" is discouraged (43 steps).
Proof modification of "bj-ax6elem1" is discouraged (27 steps).
Proof modification of "bj-ax6elem2" is discouraged (23 steps).
-Proof modification of "bj-ax8" is discouraged (55 steps).
-Proof modification of "bj-ax9" is discouraged (35 steps).
-Proof modification of "bj-ax9-2" is discouraged (74 steps).
+Proof modification of "bj-ax9" is discouraged (29 steps).
Proof modification of "bj-axc10" is discouraged (30 steps).
Proof modification of "bj-axc10v" is discouraged (37 steps).
Proof modification of "bj-axc11nv" is discouraged (5 steps).
@@ -18385,7 +18386,6 @@ Proof modification of "bj-axc4" is discouraged (15 steps).
Proof modification of "bj-axd2d" is discouraged (16 steps).
Proof modification of "bj-axdd2" is discouraged (28 steps).
Proof modification of "bj-axext3" is discouraged (57 steps).
-Proof modification of "bj-axext4" is discouraged (21 steps).
Proof modification of "bj-axrep1" is discouraged (190 steps).
Proof modification of "bj-axrep2" is discouraged (181 steps).
Proof modification of "bj-axrep3" is discouraged (122 steps).
@@ -18435,9 +18435,7 @@ Proof modification of "bj-ceqsalv" is discouraged (10 steps).
Proof modification of "bj-chvarv" is discouraged (18 steps).
Proof modification of "bj-chvarvv" is discouraged (11 steps).
Proof modification of "bj-clabel" is discouraged (43 steps).
-Proof modification of "bj-cleljustab" is discouraged (93 steps).
Proof modification of "bj-cleljusti" is discouraged (20 steps).
-Proof modification of "bj-cleqhyp" is discouraged (21 steps).
Proof modification of "bj-cmnssmnd" is discouraged (36 steps).
Proof modification of "bj-cmnssmndel" is discouraged (5 steps).
Proof modification of "bj-consensusALT" is discouraged (30 steps).
@@ -18445,12 +18443,8 @@ Proof modification of "bj-csbprc" is discouraged (47 steps).
Proof modification of "bj-currypeirce" is discouraged (51 steps).
Proof modification of "bj-denotes" is discouraged (76 steps).
Proof modification of "bj-denotesv" is discouraged (15 steps).
-Proof modification of "bj-df-clel" is discouraged (4 steps).
-Proof modification of "bj-df-cleq" is discouraged (4 steps).
Proof modification of "bj-df-nul" is discouraged (11 steps).
Proof modification of "bj-df-v" is discouraged (29 steps).
-Proof modification of "bj-dfclel" is discouraged (27 steps).
-Proof modification of "bj-dfcleq" is discouraged (27 steps).
Proof modification of "bj-dfnnf2" is discouraged (34 steps).
Proof modification of "bj-disjsn01" is discouraged (18 steps).
Proof modification of "bj-dral1v" is discouraged (36 steps).
@@ -18684,7 +18678,6 @@ Proof modification of "decmul1OLD" is discouraged (119 steps).
Proof modification of "dedtOLD" is discouraged (19 steps).
Proof modification of "demoivreALT" is discouraged (1087 steps).
Proof modification of "dfbi1ALT" is discouraged (100 steps).
-Proof modification of "dfcleq" is discouraged (10 steps).
Proof modification of "dfeu" is discouraged (35 steps).
Proof modification of "dfeuOLD" is discouraged (33 steps).
Proof modification of "dfiun2gOLD" is discouraged (134 steps).
diff --git a/set.mm b/set.mm
index df08b1ea9d..10f4e43d03 100644
--- a/set.mm
+++ b/set.mm
@@ -1609,10 +1609,9 @@ giving a shorter proof but depending on more axioms (namely, ~ ax-1 and
~ ax-2 ). (Contributed by NM, 29-Dec-1992.) $)
con4i $p |- ( ps -> ph ) $=
( wn wi con4 ax-mp ) ADBDEBAECABFG $.
+ $( $j usage 'con4i' avoids 'ax-1' 'ax-2'; $)
$}
- $( $j usage 'con4i' avoids 'ax-1' 'ax-2'; $)
-
${
con4d.1 $e |- ( ph -> ( -. ps -> -. ch ) ) $.
$( Deduction associated with ~ con4 . (Contributed by NM, 26-Mar-1995.) $)
@@ -1645,10 +1644,9 @@ giving a shorter proof but depending on more axioms (namely, ~ ax-1 and
and ~ pm2.24i . (Contributed by NM, 27-Feb-2008.) $)
pm2.24ii $p |- ps $=
( pm2.21i ax-mp ) ABCABDEF $.
+ $( $j usage 'pm2.24ii' avoids 'ax-2'; $)
$}
- $( $j usage 'pm2.24ii' avoids 'ax-2'; $)
-
${
pm2.21d.1 $e |- ( ph -> -. ps ) $.
$( A contradiction implies anything. Deduction associated with ~ pm2.21 .
@@ -1736,20 +1734,17 @@ In classical logic (our logic) this is always true. In intuitionistic
(Revised by Steven Nguyen, 27-Dec-2022.) $)
notnotri $p |- ph $=
( wn pm2.21i mt4 ) ACZCZABFGCBDE $.
-
$( $j usage 'notnotri' avoids 'ax-2'; $)
- $( Alternate proof of ~ notnotri . Inference associated with ~ notnotr .
-
- Remark: the proof via ~ notnotr and ~ ax-mp also has three essential
- steps, but has a total number of steps equal to 8, instead of the
- present 7, because it has to construct the formula ` ph ` twice and the
- formula ` -. -. ph ` once, whereas the present proof has to construct
- the formula ` ph ` twice and the formula ` -. ph ` once, and therefore
- makes only one use of ~ wn instead of two. This can be checked by
- running the Metamath command "MM> SHOW PROOF notnotri / NORMAL".
- (Contributed by NM, 27-Feb-2008.) (Proof shortened by Wolf Lammen,
- 15-Jul-2021.) (Proof modification is discouraged.)
+ $( Alternate proof of ~ notnotri . The proof via ~ notnotr and ~ ax-mp
+ also has three essential steps, but has a total number of steps equal to
+ 8, instead of the present 7, because it has to construct the formula
+ ` ph ` twice and the formula ` -. -. ph ` once, whereas the present
+ proof has to construct the formula ` ph ` twice and the formula
+ ` -. ph ` once, and therefore makes only one use of ~ wn instead of two.
+ This can be checked by running the Metamath command "MM> SHOW PROOF
+ notnotri / NORMAL". (Contributed by NM, 27-Feb-2008.) (Proof shortened
+ by Wolf Lammen, 15-Jul-2021.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
notnotriALT $p |- ph $=
( wn pm2.21i pm2.18i ) AACABDE $.
@@ -12544,7 +12539,6 @@ simplest antecedents (i.e., in the corresponding ordering of binary trees
minimp $p |- ( ph ->
( ( ps -> ch ) -> ( ( ( th -> ps ) -> ( ch -> ta ) ) -> ( ps -> ta ) ) ) ) $=
( wi jarr a2d com12 a1i ) BCFZDBFCEFZFZBEFZFFAMKNMBCEDBLGHIJ $.
-
$( $j usage 'minimp' avoids 'ax-3'; $)
$( Derivation of Syll-Simp ( ~ jarr ) from ~ ax-mp and ~ minimp .
@@ -12593,6 +12587,7 @@ simplest antecedents (i.e., in the corresponding ordering of binary trees
( wi minimp-ax2 minimp-ax1 ax-mp mp2 ) AABCZCZAACZHCCIJCZIHCAABDAHACCKAHEAH
ADFIJHDG $.
+
$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Implicational Calculus
@@ -12621,7 +12616,6 @@ simplest antecedents (i.e., in the corresponding ordering of binary trees
$)
-
$( The shortest single axiom for implicational calculus, due to Lukasiewicz.
It is now known to be the _unique_ shortest axiom. The axiom is proved
here starting from { ~ ax-1 , ~ ax-2 and ~ peirce }. (Contributed by
@@ -17418,6 +17412,14 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the
elequ2 $p |- ( x = y -> ( z e. x <-> z e. y ) ) $=
( weq wel ax9 wi equcoms impbid ) ABDCAEZCBEZABCFKJGBABACFHI $.
+ ${
+ $d x z $. $d y z $.
+ $( A form of ~ elequ2 with a universal quantifier. Its converse is the
+ axiom of extensionality ~ ax-ext . (Contributed by BJ, 3-Oct-2019.) $)
+ elequ2g $p |- ( x = y -> A. z ( z e. x <-> z e. y ) ) $=
+ ( weq wel wb elequ2 alrimiv ) ABDCAECBEFCABCGH $.
+ $}
+
$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -17963,7 +17965,7 @@ This axiom scheme is logically redundant (see ~ ax12w ) but is used as an
ax12v2 $p |- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) $=
( vz weq wi wal equtrr ax12v imim1d alimdv syl9r syld ax6evr exlimiiv ) C
DEZBCEZAQAFZBGZFZFDPQBDEZTCDBHZUAAUAAFZBGPSABDIPUCRBPQUAAUBJKLMDCNO $.
- $( $j usage 'ax12v2' avoids 'ax-10' 'ax-13'; $)
+ $( $j usage 'ax12v2' avoids 'ax-10' 'ax-11' 'ax-13'; $)
$}
${
@@ -24371,7 +24373,8 @@ number of additional axioms (mainly to replace definitions like ~ df-or and
$d x y z $.
$( Axiom of Extensionality. An axiom of Zermelo-Fraenkel set theory. It
states that two sets are identical if they contain the same elements.
- Axiom Ext of [BellMachover] p. 461.
+ Axiom Ext of [BellMachover] p. 461. Its converse is a theorem of
+ predicate logic, ~ elequ2g .
Set theory can also be formulated with a _single_ primitive predicate
` e. ` on top of traditional predicate calculus _without_ equality. In
@@ -24441,14 +24444,12 @@ number of additional axioms (mainly to replace definitions like ~ df-or and
) CDEZCBEZFZCGZDBHZICAEZRFZCGZABHZIDADAHZTUDUAUEUFSUCCUFQUBRDACJKLDABMNDB
COP $.
- $( A bidirectional version of Extensionality. Although this theorem
- "looks" like it is just a definition of equality, it requires the Axiom
- of Extensionality for its proof under our axiomatization. See the
- comments for ~ ax-ext and ~ df-cleq . (Contributed by NM,
- 14-Nov-2008.) $)
+ $( A bidirectional version of the axiom of extensionality. Although this
+ theorem looks like a definition of equality, it requires the axiom of
+ extensionality for its proof under our axiomatization. See the comments
+ for ~ ax-ext and ~ df-cleq . (Contributed by NM, 14-Nov-2008.) $)
axext4 $p |- ( x = y <-> A. z ( z e. x <-> z e. y ) ) $=
- ( weq wel wb wal elequ2 alrimiv axext3 impbii ) ABDZCAECBEFZCGLMCABCHIABC
- JK $.
+ ( weq wel wb wal elequ2g axext3 impbii ) ABDCAECBEFCGABCHABCIJ $.
$}
${
@@ -24500,7 +24501,7 @@ number of additional axioms (mainly to replace definitions like ~ df-or and
$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
- Class abstractions (a.k.a. class builders)
+ Classes
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)
@@ -24550,12 +24551,19 @@ Class abstractions (a.k.a. class builders)
$v T $.
$v U $.
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+ Class abstractions
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
$( Introduce the class builder or class abstraction notation ("the class of
- sets ` x ` such that ` ph ` is true"). Our class variables ` A ` ,
- ` B ` , etc. range over class builders (implicitly in the case of defined
- class terms such as ~ df-nul ). Note that a setvar variable can be
- expressed as a class builder per theorem ~ cvjust , justifying the
- assignment of setvar variables to class variables via the use of ~ cv . $)
+ sets ` x ` such that ` ph ` "). Our class variables ` A ` , ` B ` , etc.
+ range over class builders (implicitly in the case of defined class terms
+ such as ~ df-nul ). Note that a setvar variable can be expressed as a
+ class builder per theorem ~ cvjust , justifying the assignment of setvar
+ variables to class variables via the use of ~ cv . $)
cab $a class { x | ph } $.
$( $j primitive 'cv' 'wceq' 'wcel' 'cab'; $)
@@ -24813,10 +24821,41 @@ discussion in Quine (and under ~ abeq2 for a quick overview).
conservativity require external justification that is beyond the scope of
the definition checker.
+ In particular, note that ~ df-clab defines a class abstraction if only if
+ a class abstraction is completely determined by which elements it
+ contains, which is the content of the axiom of extensionality ~ ax-ext .
+ Therefore, ~ df-clab can be considered a definition only in systems that
+ can prove ~ ax-ext (and the necessary first-order logic).
+
For a general discussion of the theory of classes, see
~ mmset.html#class . (Contributed by NM, 26-May-1993.) $)
df-clab $a |- ( x e. { y | ph } <-> [ x / y ] ph ) $.
+ $( Instance of ~ eleq1w where the containing class is a class abstraction,
+ proved without ~ ax-ext , ~ df-cleq and ~ df-clel . See also ~ elequ1 for
+ setvars and ~ eleq1 for general classes. The straightforward yet
+ important fact that this statement can be proved from FOL= and ~ df-clab
+ (hence without ~ ax-ext , ~ df-cleq or ~ df-clel ) was stressed by Mario
+ Carneiro. (Contributed by BJ, 17-Aug-2023.) $)
+ eleq1ab $p |- ( x = y -> ( x e. { z | ph } <-> y e. { z | ph } ) ) $=
+ ( weq wsb cv cab wcel sbequ df-clab 3bitr4g ) BCEADBFADCFBGADHZICGMIABCDJAB
+ DKACDKL $.
+ $( $j usage 'eleq1ab' avoids 'ax-ext' 'df-cleq' 'df-clel' $)
+
+ ${
+ $d x z $. $d y z $. $d ph z $.
+ $( An instance of ~ df-clel where the LHS (the definiendum) has the form
+ "setvar ` e. ` class abstraction". See also ~ cleljust . The instance
+ of ~ df-clel where the LHS has the form "setvar ` e. ` setvar" is proved
+ as ~ cleljust , from FOL= and ~ ax-8 . (Contributed by BJ, 8-Nov-2021.)
+ (Proof shortened by Steven Nguyen, 19-May-2023.) $)
+ cleljustab $p |-
+ ( x e. { y | ph } <-> E. z ( z = x /\ z e. { y | ph } ) ) $=
+ ( weq cv cab wcel wa wex eleq1ab equsexvw bicomi ) DBEDFACGZHZIDJBFNHZOPD
+ BADBCKLM $.
+ $( $j usage 'cleljustab' avoids 'ax-ext' 'df-cleq' 'df-clel' $)
+ $}
+
$( Simplification of class abstraction notation when the free and bound
variables are identical. (Contributed by NM, 26-May-1993.) $)
abid $p |- ( x e. { x | ph } <-> ph ) $=
@@ -24853,24 +24892,31 @@ discussion in Quine (and under ~ abeq2 for a quick overview).
( cv cab wcel nf5ri hbab nf5i ) DFACGHBABCDABEIJK $.
$}
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+ Class equality
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
${
- $d x A $. $d x B $. $d x y z $.
- df-cleq.1 $e |- ( A. x ( x e. y <-> x e. z ) -> y = z ) $.
+ $d x y z t u v A $. $d x y z t u v B $.
+ df-cleq.1 $e |- ( y = z <-> A. u ( u e. y <-> u e. z ) ) $.
+ df-cleq.2 $e |- ( t = t <-> A. v ( v e. t <-> v e. t ) ) $.
$( Define the equality connective between classes. Definition 2.7 of
[Quine] p. 18. Also Definition 4.5 of [TakeutiZaring] p. 13; Chapter 4
provides its justification and methods for eliminating it. Note that
its elimination will not necessarily result in a single wff in the
original language but possibly a "scheme" of wffs.
- This is an example of a somewhat "risky" definition, meaning that it has
- a more complex than usual soundness justification (outside of Metamath),
- because it "overloads" or reuses the existing equality symbol rather
- than introducing a new symbol. This allows us to make statements that
- may not hold for the original symbol. For example, it permits us to
- deduce ` y = z <-> A. x ( x e. y <-> x e. z ) ` , which is not a theorem
- of logic but rather presupposes the Axiom of Extensionality (see theorem
- ~ axext4 ). We therefore include this axiom as a hypothesis, so that
- the use of Extensionality is properly indicated.
+ The hypotheses express that all instances of the conclusion where class
+ variables are replaced with setvar variables hold. Therefore, this
+ definition merely extends to class variables something that is true for
+ setvar variables, hence is conservative. This is only a proof sketch of
+ conservativity; for details see Appendix of [Levy] p. 357. This is the
+ reason why we call this axiomatic statement a "definition", even though
+ 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 ~ abeq2 .
@@ -24886,20 +24932,25 @@ of logic but rather presupposes the Axiom of Extensionality (see theorem
of the definition checker.
For a general discussion of the theory of classes, see
- ~ mmset.html#class . (Contributed by NM, 15-Sep-1993.) $)
+ ~ mmset.html#class . (Contributed by NM, 15-Sep-1993.) (Revised by BJ,
+ 24-Jun-2019.) $)
df-cleq $a |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $.
$}
${
- $d x A $. $d x B $. $d x y z $.
- $( The same as ~ df-cleq with the hypothesis removed using the Axiom of
- Extensionality ~ ax-ext . (Contributed by NM, 15-Sep-1993.) Revised to
- make use of ~ axext3 instead of ~ ax-ext , so that ~ ax-9 will appear in
- lists of axioms used by a proof, since ~ df-cleq implies ~ ax-9 by
- theorem ~ bj-ax9 . We may revisit this in the future. (Revised by NM,
- 28-Oct-2021.) (Proof modification is discouraged.) $)
+ $d x y z t u v A $. $d x y z t u v B $.
+ $( The defining characterization of class equality. It is proved, over
+ Tarski's FOL, from the axiom of (set) extensionality ( ~ ax-ext ) and
+ the definition of class equality ( ~ df-cleq ). Its forward implication
+ is called "class extensionality". Remark: the proof uses ~ axext4 to
+ prove also the hypothesis of ~ df-cleq that is a degenerate instance,
+ but it could be proved also from minimal propositional calculus and {
+ ~ ax-gen , ~ equid }. (Contributed by NM, 15-Sep-1993.) (Revised by
+ BJ, 24-Jun-2019.) $)
dfcleq $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $=
- ( vy vz axext3 df-cleq ) ADEBCDEAFG $.
+ ( vy vz vv vu vt axext4 df-cleq ) ADEFGHBCDEGIHHFIJ $.
+ $( $j usage 'dfcleq' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
+ 'df-clab' 'df-clel'; $)
$}
${
@@ -24920,36 +24971,23 @@ of logic but rather presupposes the Axiom of Extensionality (see theorem
cvjust $p |- x = { y | y e. x } $=
( vz cv wel cab wceq wcel wb dfcleq wsb df-clab elsb3 bitr2i mpgbir ) ADZ
BAEZBFZGCAEZCDRHZICCPRJTQBCKSQCBLCBAMNO $.
+ $( $j usage 'cvjust' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13' 'df-clel'; $)
$}
${
- $d x A $. $d x B $.
- $( Define the membership connective between classes. Theorem 6.3 of
- [Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we
- adopt as a definition. See these references for its metalogical
- justification. Note that like ~ df-cleq it extends or "overloads" the
- use of the existing membership symbol, but unlike ~ df-cleq it does not
- strengthen the set of valid wffs of logic when the class variables are
- replaced with setvar variables (see ~ cleljust ), so we don't include
- any set theory axiom as a hypothesis. See also comments about the
- syntax under ~ df-clab . Alternate definitions of ` A e. B ` (but that
- require either ` A ` or ` B ` to be a set) are shown by ~ clel2 ,
- ~ clel3 , and ~ clel4 .
-
- This is called the "axiom of membership" by [Levy] p. 338, who treats
- the theory of classes as an extralogical extension to our logic and set
- theory axioms.
-
- While the three class definitions ~ df-clab , ~ df-cleq , and ~ df-clel
- are eliminable and conservative and thus meet the requirements for sound
- definitions, they are technically axioms in that they do not satisfy the
- requirements for the current definition checker. The proofs of
- conservativity require external justification that is beyond the scope
- of the definition checker.
-
- For a general discussion of the theory of classes, see
- ~ mmset.html#class . (Contributed by NM, 26-May-1993.) $)
- df-clel $a |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $.
+ $d t x $. $d t y $. $d t z $.
+ $( Proof of ~ ax-9 from Tarski's FOL and ~ dfcleq . For a version not
+ using ~ ax-8 either, see ~ bj-ax9 . This shows that ~ dfcleq is too
+ powerful to be used as a definition instead of ~ df-cleq . Note that
+ ~ ax-ext is also a direct consequence of ~ dfcleq (as an instance of its
+ forward implication). (Contributed by BJ, 24-Jun-2019.)
+ (Proof modification is discouraged.) (New usage is discouraged.) $)
+ ax9ALT $p |- ( x = y -> ( z e. x -> z e. y ) ) $=
+ ( vt weq wel wi wal wb cv dfcleq biimpi biimp sylg equcoms imim12d spimvw
+ ax8 syl ) ABEZDAFZDBFZGZDHCAFZCBFZGZTUAUBIZUCDTUGDHDAJBJKLUAUBMNUCUFDCDCE
+ UDUAUBUEUDUAGCDCDARODCBRPQS $.
+ $( $j usage 'ax9ALT' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13' 'df-clab'
+ 'df-clel'; $)
$}
${
@@ -25515,21 +25553,87 @@ replaced with setvar variables (see ~ cleljust ), so we don't include
EBGLMPORPCFAHLMN $.
$}
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+ Class membership
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+ ${
+ $d x y z t u v A $. $d x y z t u v B $.
+ df-clel.1 $e |- ( y e. z <-> E. u ( u = y /\ u e. z ) ) $.
+ df-clel.2 $e |- ( t e. t <-> E. v ( v = t /\ v e. t ) ) $.
+ $( Define the membership connective between classes. Theorem 6.3 of
+ [Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we
+ adopt as a definition. See these references for its metalogical
+ justification.
+
+ The hypotheses express that all instances of the conclusion where class
+ variables are replaced with setvar variables hold. Therefore, this
+ definition merely extends to class variables something that is true for
+ setvar variables, hence is conservative. This is only a proof sketch of
+ conservativity; for details see Appendix of [Levy] p. 357. This is the
+ reason why we call this axiomatic statement a "definition", even though
+ 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 ~ abeq2 .
+
+ Alternate characterizations of ` A e. B ` when either ` A ` or ` B ` is
+ a set are given by ~ clel2 , ~ clel3 , and ~ clel4 .
+
+ This is called the "axiom of membership" by [Levy] p. 338, who treats
+ the theory of classes as an extralogical extension to our logic and set
+ theory axioms.
+
+ While the three class definitions ~ df-clab , ~ df-cleq , and ~ df-clel
+ are eliminable and conservative and thus meet the requirements for sound
+ definitions, they are technically axioms in that they do not satisfy the
+ requirements for the current definition checker. The proofs of
+ conservativity require external justification that is beyond the scope
+ of the definition checker.
+
+ For a general discussion of the theory of classes, see
+ ~ mmset.html#class . (Contributed by NM, 26-May-1993.) (Revised by BJ,
+ 27-Jun-2019.) $)
+ df-clel $a |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $.
+ $}
+
+ ${
+ $d x y z t u v A $. $d x y z t u v B $.
+ $( Characterization of the elements of a class. (Contributed by BJ,
+ 27-Jun-2019.) $)
+ dfclel $p |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $=
+ ( vy vz vv vu vt cleljust df-clel ) ADEFGHBCDEGIHHFIJ $.
+ $( $j usage 'dfclel' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
+ 'ax-ext' 'df-clab' 'df-cleq'; $)
+ $}
+
${
$d z x $. $d z y $. $d z A $.
$( Weaker version of ~ eleq1 (but more general than ~ elequ1 ) not
- depending on ~ ax-ext nor ~ df-cleq . (Contributed by BJ,
- 24-Jun-2019.) $)
+ depending on ~ ax-ext nor ~ df-cleq .
+
+ Note that this provides a proof of ~ ax-8 from Tarski's FOL and ~ dfclel
+ (simply consider an instance where ` A ` is replaced by a setvar and
+ deduce the forward implication by ~ biimpd ), which shows that ~ dfclel
+ is too powerful to be used as a definition instead of ~ df-clel .
+ (Contributed by BJ, 24-Jun-2019.) $)
eleq1w $p |- ( x = y -> ( x e. A <-> y e. A ) ) $=
- ( vz weq cv wcel wa wex equequ2 anbi1d exbidv df-clel 3bitr4g ) ABEZDAEZD
- FCGZHZDIDBEZQHZDIAFZCGBFZCGORTDOPSQABDJKLDUACMDUBCMN $.
+ ( vz weq cv wcel wa wex equequ2 anbi1d exbidv dfclel 3bitr4g ) ABEZDAEZDF
+ CGZHZDIDBEZQHZDIAFZCGBFZCGORTDOPSQABDJKLDUACMDUBCMN $.
+ $( $j usage 'eleq1w' avoids 'ax-9' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
+ 'ax-ext' 'df-clab' 'df-cleq'; $)
$( Weaker version of ~ eleq2 (but more general than ~ elequ2 ) not
depending on ~ ax-ext nor ~ df-cleq . (Contributed by BJ,
29-Sep-2019.) $)
eleq2w $p |- ( x = y -> ( A e. x <-> A e. y ) ) $=
- ( vz cv wceq wcel wa wex elequ2 anbi2d exbidv df-clel 3bitr4g ) AEZBEZFZD
- EZCFZROGZHZDISRPGZHZDICOGCPGQUAUCDQTUBSABDJKLDCOMDCPMN $.
+ ( vz cv wceq wcel wa wex elequ2 anbi2d exbidv dfclel 3bitr4g ) AEZBEZFZDE
+ ZCFZROGZHZDISRPGZHZDICOGCPGQUAUCDQTUBSABDJKLDCOMDCPMN $.
+ $( $j usage 'eleq2w' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'
+ 'ax-ext' 'df-clab' 'df-cleq'; $)
$}
${
@@ -25539,25 +25643,25 @@ replaced with setvar variables (see ~ cleljust ), so we don't include
NM, 21-Jun-1993.) Allow shortening of ~ eleq1 . (Revised by Wolf
Lammen, 20-Nov-2019.) $)
eleq1d $p |- ( ph -> ( A e. C <-> B e. C ) ) $=
- ( vx cv wceq wcel wa wex eqeq2d anbi1d exbidv df-clel 3bitr4g ) AFGZBHZQD
- IZJZFKQCHZSJZFKBDICDIATUBFARUASABCQELMNFBDOFCDOP $.
+ ( vx cv wceq wcel wa wex eqeq2d anbi1d exbidv dfclel 3bitr4g ) AFGZBHZQDI
+ ZJZFKQCHZSJZFKBDICDIATUBFARUASABCQELMNFBDOFCDOP $.
$( Deduction from equality to equivalence of membership. (Contributed by
NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf
Lammen, 5-Dec-2019.) $)
eleq2d $p |- ( ph -> ( C e. A <-> C e. B ) ) $=
- ( vx cv wceq wa wex wb wal dfcleq sylib anbi2 alexbii syl df-clel 3bitr4g
- wcel ) AFGZDHZUABTZIZFJZUBUACTZIZFJZDBTDCTAUCUFKZFLZUEUHKABCHUJEFBCMNUIUD
- UGFUCUFUBOPQFDBRFDCRS $.
+ ( vx cv wceq wcel wa wex wb wal dfcleq sylib anbi2 alexbii dfclel 3bitr4g
+ syl ) AFGZDHZUABIZJZFKZUBUACIZJZFKZDBIDCIAUCUFLZFMZUEUHLABCHUJEFBCNOUIUDU
+ GFUCUFUBPQTFDBRFDCRS $.
$( Alternate proof of ~ eleq2d , shorter at the expense of requiring
~ ax-12 . (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen,
20-Nov-2019.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
eleq2dALT $p |- ( ph -> ( C e. A <-> C e. B ) ) $=
- ( vx cv wceq wcel wa wex wal dfcleq 19.21bi anbi2d exbidv df-clel 3bitr4g
- wb sylib ) AFGZDHZUABIZJZFKUBUACIZJZFKDBIDCIAUDUFFAUCUEUBAUCUESZFABCHUGFL
- EFBCMTNOPFDBQFDCQR $.
+ ( vx cv wceq wcel wa wex wb wal dfcleq sylib 19.21bi anbi2d exbidv dfclel
+ 3bitr4g ) AFGZDHZUABIZJZFKUBUACIZJZFKDBIDCIAUDUFFAUCUEUBAUCUELZFABCHUGFME
+ FBCNOPQRFDBSFDCST $.
$}
$( Equality implies equivalence of membership. (Contributed by NM,
@@ -25948,6 +26052,13 @@ replaced with setvar variables (see ~ cleljust ), so we don't include
CBDKZOPAQLM $.
$}
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+ Elementary properties of class abstractions
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
${
$d x A y $. $d ph y $.
$( Equality of a class variable and a class abstraction (also called a
@@ -26248,9 +26359,9 @@ choice between (what we call) a "definitional form" where the shorter
$( Membership of a class variable in a class abstraction. (Contributed by
NM, 23-Dec-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) $)
clelab $p |- ( A e. { x | ph } <-> E. x ( x = A /\ ph ) ) $=
- ( vy cab wcel cv wceq wa wex df-clel nfv nfsab1 weq eqeq1 sbequ12 df-clab
- nfan wsb syl6bbr anbi12d cbvexv1 bitr4i ) CABEZFDGZCHZUEUDFZIZDJBGZCHZAIZ
- BJDCUDKUKUHBDUKDLUFUGBUFBLABDMRBDNZUJUFAUGUIUECOULAABDSUGABDPADBQTUAUBUC
+ ( vy cab wcel cv wceq wa wex dfclel nfv nfsab1 nfan weq eqeq1 wsb sbequ12
+ df-clab syl6bbr anbi12d cbvexv1 bitr4i ) CABEZFDGZCHZUEUDFZIZDJBGZCHZAIZB
+ JDCUDKUKUHBDUKDLUFUGBUFBLABDMNBDOZUJUFAUGUIUECPULAABDQUGABDRADBSTUAUBUC
$.
$}
@@ -26260,8 +26371,8 @@ choice between (what we call) a "definitional form" where the shorter
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 abeq2 anbi2ci exbii bitri ) ABEZ
- DFCGZRHZSDFZIZCJUABGSFAKBLZIZCJCRDMUBUDCTUCUAABSNOPQ $.
+ ( cab wcel cv wceq wa wex wb wal dfclel abeq2 anbi2ci exbii bitri ) ABEZD
+ FCGZRHZSDFZIZCJUABGSFAKBLZIZCJCRDMUBUDCTUCUAABSNOPQ $.
$}
${
@@ -26391,11 +26502,9 @@ choice between (what we call) a "definitional form" where the shorter
nfceqi $p |- ( F/_ x A <-> F/_ x B ) $=
( vy cv wcel wnf wal wnfc eleq2i nfbii albii df-nfc 3bitr4i ) EFZBGZAHZEI
PCGZAHZEIABJACJRTEQSABCPDKLMAEBNAECNO $.
-
- $( $j usage 'nfceqi' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13' ; $)
+ $( $j usage 'nfceqi' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13' 'df-clab' ; $)
$}
-
${
nfcxfr.1 $e |- A = B $.
$( Obsolete proof of ~ nfceqi as of 19-Jun-2023. (Contributed by Mario
@@ -26495,7 +26604,7 @@ choice between (what we call) a "definitional form" where the shorter
$( Hypothesis builder for elementhood. (Contributed by Mario Carneiro,
7-Oct-2016.) $)
nfeld $p |- ( ph -> F/ x A e. B ) $=
- ( vy wcel cv wceq wa wex df-clel nfv nfcvd nfeqd nfcrd nfand nfexd nfxfrd
+ ( vy wcel cv wceq wa wex dfclel nfv nfcvd nfeqd nfcrd nfand nfexd nfxfrd
) CDHGIZCJZUADHZKZGLABGCDMAUDBGAGNAUBUCBABUACABUAOEPABGDFQRST $.
$}
@@ -27908,7 +28017,6 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed
( A. x e. A ph <-> A. x e. A ps ) ) $=
( wb wral biimp ral2imi biimpr impbid ) ABEZCDFACDFBCDFKABCDABGHKBACDABIHJ
$.
-
$( $j usage 'ralbi' avoids 'ax-5' 'ax-6' 'ax-7' 'ax-10' 'ax-12' ; $)
$( Cancellation law for restricted universal quantification. (Contributed by
@@ -28720,8 +28828,8 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed
$( Two ways to say " ` A ` belongs to ` B ` ". (Contributed by NM,
22-Nov-1994.) $)
risset $p |- ( A e. B <-> E. x e. B x = A ) $=
- ( cv wcel wceq wa wex wrex exancom df-rex df-clel 3bitr4ri ) ADZCEZNBFZGA
- HPOGAHPACIBCEOPAJPACKABCLM $.
+ ( cv wcel wceq wa wex wrex exancom df-rex dfclel 3bitr4ri ) ADZCEZNBFZGAH
+ POGAHPACIBCEOPAJPACKABCLM $.
$}
${
@@ -29218,10 +29326,9 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed
( wral wrex cv wcel wex df-rex nfv nfra1 nfan nfex nfxfr ax-1 rsp com12
wa reximdv sylcom ralrimi ) ACEFZBDGZABDGZCEUEBHDIZUDTZBJCUDBDKUHCBUGUDCU
GCLACEMNOPUECHEIZUEUFUEUIQUIUDABDUDUIAACERSUAUBUC $.
+ $( $j usage 'r19.12' avoids 'ax-13' 'ax-ext'; $)
$}
- $( $j usage 'r19.12' avoids 'ax-13' 'ax-ext'; $)
-
${
$d x y $.
r2exf.1 $e |- F/_ y A $.
@@ -30646,8 +30753,8 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed
constants in the distinct variable list.) (Contributed by NM,
26-May-1993.) $)
isset $p |- ( A e. _V <-> E. x x = A ) $=
- ( cvv wcel cv wceq wa wex df-clel vex biantru exbii bitr4i ) BCDAEZBFZNCD
- ZGZAHOAHABCIOQAPOAJKLM $.
+ ( cvv wcel cv wceq wa wex dfclel vex biantru exbii bitr4i ) BCDAEZBFZNCDZ
+ GZAHOAHABCIOQAPOAJKLM $.
$}
${
@@ -30691,8 +30798,8 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed
of [Quine] p. 44. (Contributed by NM, 26-May-1993.) (Proof shortened
by Andrew Salmon, 8-Jun-2011.) $)
elex $p |- ( A e. B -> A e. _V ) $=
- ( vx cv wceq wcel wa wex cvv exsimpl df-clel isset 3imtr4i ) CDZAEZNBFZGC
- HOCHABFAIFOPCJCABKCALM $.
+ ( vx cv wceq wcel wa wex cvv exsimpl dfclel isset 3imtr4i ) CDZAEZNBFZGCH
+ OCHABFAIFOPCJCABKCALM $.
$}
${
@@ -32637,7 +32744,6 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed
UBUGUCUHUEUAAUDDCMNUDDDSOEPQRT $.
$}
-
${
$d y ph $. $d x y ps $. $d x y A $.
eqeu.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
@@ -34127,7 +34233,6 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
( cvv wcel wb wsbc sbcex sbcbig biimpd mpcom ) DEFZABGZCDHZACDHBCDHGZNCDIMO
PABCDEJKL $.
-
$( Substituting into equivalent wff's gives equivalent results. (Contributed
by Giovanni Mascellani, 9-Apr-2018.) (Proof shortened by Wolf Lammen,
4-May-2023.) $)
@@ -34441,11 +34546,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
{ y | [. A / x ]. ph } e. B ) ) $=
( vw wcel cvv cab wsbc wb cv wceq wa wex wal syl5bb abeq2 elex sbcan sbcg
sbcex2 sbcal sbcbig bibi1d bitrd albidv sbcbii 3bitr4g nfcri sbcgf exbidv
- anbi12d df-clel syl ) DFIDJIZACKZEIZBDLZABDLZCKZEIZMDFUAURHNZUSOZVEEIZPZH
- QZBDLZVEVCOZVGPZHQZVAVDVJVHBDLZHQURVMVHHBDUDURVNVLHVNVFBDLZVGBDLZPURVLVFV
- GBDUBURVOVKVPVGURCNVEIZAMZCRZBDLZVQVBMZCRZVOVKVTVRBDLZCRURWBVRCBDUEURWCWA
- CURWCVQBDLZVBMWAVQABDJUFURWDVQVBVQBDJUCUGUHUISVFVSBDACVETUJVBCVETUKVGBDJB
- HEGULUMUOSUNSUTVIBDHUSEUPUJHVCEUPUKUQ $.
+ anbi12d dfclel syl ) DFIDJIZACKZEIZBDLZABDLZCKZEIZMDFUAURHNZUSOZVEEIZPZHQ
+ ZBDLZVEVCOZVGPZHQZVAVDVJVHBDLZHQURVMVHHBDUDURVNVLHVNVFBDLZVGBDLZPURVLVFVG
+ BDUBURVOVKVPVGURCNVEIZAMZCRZBDLZVQVBMZCRZVOVKVTVRBDLZCRURWBVRCBDUEURWCWAC
+ URWCVQBDLZVBMWAVQABDJUFURWDVQVBVQBDJUCUGUHUISVFVSBDACVETUJVBCVETUKVGBDJBH
+ EGULUMUOSUNSUTVIBDHUSEUPUJHVCEUPUKUQ $.
$}
${
@@ -35354,9 +35459,9 @@ technically classes despite morally (and provably) being sets, like ` 1 `
$( Membership relationships follow from a subclass relationship.
(Contributed by NM, 5-Aug-1993.) $)
ssel $p |- ( A C_ B -> ( C e. A -> C e. B ) ) $=
- ( vx wss cv wceq wa wex wi wal dfss2 biimpi 19.21bi anim2d eximdv df-clel
- wcel 3imtr4g ) ABEZDFZCGZUAARZHZDIUBUABRZHZDICARCBRTUDUFDTUCUEUBTUCUEJZDT
- UGDKDABLMNOPDCAQDCBQS $.
+ ( vx wss cv wceq wcel wa wex wi dfss2 biimpi 19.21bi anim2d eximdv dfclel
+ wal 3imtr4g ) ABEZDFZCGZUAAHZIZDJUBUABHZIZDJCAHCBHTUDUFDTUCUEUBTUCUEKZDTU
+ GDRDABLMNOPDCAQDCBQS $.
$}
$( Membership relationships follow from a subclass relationship.
@@ -37932,9 +38037,9 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets,
(Revised by Steven Nguyen, 3-May-2023.) $)
noel $p |- -. A e. (/) $=
( vx vy c0 wcel cv wceq wa wex cvv cab pm3.24 nex wsb df-clab spsbe sylbi
- wn mto mtbir cdif df-nul df-dif eqtri eleq2i intnan df-clel ) ADEBFZAGZUH
- DEZHZBIUKBUJUIUJUHCFJEZULRHZCKZEZUOUMCIZUMCULLMUOUMCBNUPUMBCOUMCBPQSDUNUH
- DJJUAUNUBCJJUCUDUETUFMBADUGT $.
+ wn mto mtbir cdif df-nul df-dif eqtri eleq2i intnan dfclel ) ADEBFZAGZUHD
+ EZHZBIUKBUJUIUJUHCFJEZULRHZCKZEZUOUMCIZUMCULLMUOUMCBNUPUMBCOUMCBPQSDUNUHD
+ JJUAUNUBCJJUCUDUETUFMBADUGT $.
$}
$( Obsolete version of ~ noel as of 3-May-2023. The empty set has no
@@ -41017,9 +41122,9 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) $)
disjsn $p |- ( ( A i^i { B } ) = (/) <-> -. B e. A ) $=
( vx csn cin c0 wceq cv wcel wn wi wal wa disj1 con2b velsn imbi1i 3bitri
- imnan albii wex alnex df-clel xchbinxr ) ABDZEFGCHZAIZUFUEIZJKZCLUFBGZUGM
- ZJZCLZBAIZJCAUENUIULCUIUHUGJZKUJUOKULUGUHOUHUJUOCBPQUJUGSRTUMUKCUAUNUKCUB
- CBAUCUDR $.
+ imnan albii wex alnex dfclel xchbinxr ) ABDZEFGCHZAIZUFUEIZJKZCLUFBGZUGMZ
+ JZCLZBAIZJCAUENUIULCUIUHUGJZKUJUOKULUGUHOUHUJUOCBPQUJUGSRTUMUKCUAUNUKCUBC
+ BAUCUDR $.
$}
$( Two distinct singletons are disjoint. (Contributed by NM,
@@ -41781,13 +41886,13 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
show a direct elementary proof. (Contributed by NM, 7-Aug-1994.) $)
pwpw0 $p |- ~P { (/) } = { (/) , { (/) } } $=
( vx vy cv c0 csn wss cab wceq wo cpw cpr wn wa wcel wi dfss2 velsn sylbi
- wal wex imbi2i albii bitri neq0 exintr syl5bi exancom df-clel bitr4i syl6
- snssi anc2li eqss syl6ibr orrd 0ss sseq1 mpbiri eqimss impbii abbii df-pw
- jaoi dfpr2 3eqtr4i ) ACZDEZFZAGVFDHZVFVGHZIZAGVGJDVGKVHVKAVHVKVHVIVJVHVIL
- ZVHVGVFFZMVJVHVLVMVHBCZVFNZVNDHZOZBSZVLVMOVHVOVNVGNZOZBSVRBVFVGPVTVQBVSVP
- VOBDQUAUBUCVRVLVOVPMBTZVMVLVOBTVRWABVFUDVOVPBUEUFWADVFNZVMWAVPVOMBTWBVOVP
- BUGBDVFUHUIDVFUKRUJRULVFVGUMUNUOVIVHVJVIVHDVGFVGUPVFDVGUQURVFVGUSVCUTVAAV
- GVBADVGVDVE $.
+ wal wex imbi2i albii bitri neq0 exintr syl5bi exancom dfclel bitr4i snssi
+ syl6 anc2li eqss syl6ibr orrd sseq1 mpbiri eqimss jaoi impbii abbii df-pw
+ 0ss dfpr2 3eqtr4i ) ACZDEZFZAGVFDHZVFVGHZIZAGVGJDVGKVHVKAVHVKVHVIVJVHVILZ
+ VHVGVFFZMVJVHVLVMVHBCZVFNZVNDHZOZBSZVLVMOVHVOVNVGNZOZBSVRBVFVGPVTVQBVSVPV
+ OBDQUAUBUCVRVLVOVPMBTZVMVLVOBTVRWABVFUDVOVPBUEUFWADVFNZVMWAVPVOMBTWBVOVPB
+ UGBDVFUHUIDVFUJRUKRULVFVGUMUNUOVIVHVJVIVHDVGFVGVCVFDVGUPUQVFVGURUSUTVAAVG
+ VBADVGVDVE $.
$}
$( A singleton is a subset of an unordered pair containing its member.
@@ -42575,13 +42680,13 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
(New usage is discouraged.) $)
pwsnALT $p |- ~P { A } = { (/) , { A } } $=
( vx vy cv csn wss cab c0 wceq wo cpw cpr wn wa wcel wal dfss2 wex sylbi
- wi velsn imbi2i albii bitri neq0 exintr syl5bi df-clel exancom snssi syl6
- bitr2i anc2li eqss syl6ibr orrd 0ss sseq1 mpbiri eqimss jaoi impbii abbii
- df-pw dfpr2 3eqtr4i ) BDZAEZFZBGVGHIZVGVHIZJZBGVHKHVHLVIVLBVIVLVIVJVKVIVJ
- MZVIVHVGFZNVKVIVMVNVICDZVGOZVOAIZTZCPZVMVNTVIVPVOVHOZTZCPVSCVGVHQWAVRCVTV
- QVPCAUAUBUCUDVSVMVPVQNCRZVNVMVPCRVSWBCVGUEVPVQCUFUGWBAVGOZVNWCVQVPNCRWBCA
- VGUHVQVPCUIULAVGUJSUKSUMVGVHUNUOUPVJVIVKVJVIHVHFVHUQVGHVHURUSVGVHUTVAVBVC
- BVHVDBHVHVEVF $.
+ wi velsn imbi2i albii bitri neq0 exintr syl5bi dfclel exancom bitr2i syl6
+ snssi anc2li eqss syl6ibr orrd 0ss sseq1 mpbiri eqimss impbii abbii df-pw
+ jaoi dfpr2 3eqtr4i ) BDZAEZFZBGVGHIZVGVHIZJZBGVHKHVHLVIVLBVIVLVIVJVKVIVJM
+ ZVIVHVGFZNVKVIVMVNVICDZVGOZVOAIZTZCPZVMVNTVIVPVOVHOZTZCPVSCVGVHQWAVRCVTVQ
+ VPCAUAUBUCUDVSVMVPVQNCRZVNVMVPCRVSWBCVGUEVPVQCUFUGWBAVGOZVNWCVQVPNCRWBCAV
+ GUHVQVPCUIUJAVGULSUKSUMVGVHUNUOUPVJVIVKVJVIHVHFVHUQVGHVHURUSVGVHUTVDVAVBB
+ VHVCBHVHVEVF $.
$( The power set of an unordered pair. (Contributed by NM, 1-May-2009.) $)
pwpr $p |- ~P { A , B } = ( { (/) , { A } } u. { { B } , { A , B } } ) $=
@@ -46248,7 +46353,7 @@ conditioning it (with ` x e. z ` ) so that it asserts the existence of a
$( Alternate proof of ~ axnul , proved from propositional calculus,
~ ax-gen , ~ ax-4 , ~ sp , and ~ ax-rep . To check this, replace ~ sp
with the obsolete axiom ~ ax-c5 in the proof of ~ axnulALT and type the
- Metamath program "MM> SHOW TRACE_BACK axnulALT / AXIOMS" command.
+ Metamath program "MM> SHOW TRACE axnulALT / AXIOMS" command.
(Contributed by Jeff Hoffman, 3-Feb-2008.) (Proof shortened by Mario
Carneiro, 17-Nov-2016.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
@@ -47502,11 +47607,9 @@ This theorem is proved directly from set theory axioms (no set theory
( vw wel wn wal wex ax-pow pm2.21 alimi a1i imim1d alimdv eximdv exlimiiv
wi mpi ax-nul ) CDEZFCGZCBEZFZCGZBAEZQZBGZAHZDUAUBTQZCGZUEQZBGZAHUHDABCIU
AULUGAUAUKUFBUAUDUJUEUDUJQUAUCUICUBTJKLMNORDCSP $.
-
+ $( $j usage 'axprlem1' avoids 'ax-ext' 'ax-sep'; $)
$}
- $( $j usage 'axprlem1' avoids 'ax-ext' 'ax-sep'; $)
-
${
$d x y z w v $.
$( Lemma for ~ axpr . There exists a set to which all sets whose only
@@ -47517,10 +47620,9 @@ This theorem is proved directly from set theory axioms (no set theory
wral eximdv mpi axprlem1 exlimiiv ) DCFGDHZCEFZIZCHZUDCBJZSZBAFZIZBHZAKZE
UGCBFZUEIZCHZUJIZBHZAKUMEABCLUGURULAUGUQUKBUGUIUPUJUIUNUDIZCHUGUPUDCUHMUF
USUOCUDUEUNNOPQRTUAECDUBUC $.
+ $( $j usage 'axprlem2' avoids 'ax-ext' 'ax-sep'; $)
$}
- $( $j usage 'axprlem2' avoids 'ax-ext' 'ax-sep'; $)
-
${
$d x z w $. $d y z w $. $d z w n $. $d z w s p $.
$( Lemma for ~ axpr . Eliminate the antecedent of the relevant replacement
@@ -47533,10 +47635,9 @@ This theorem is proved directly from set theory axioms (no set theory
UNUDUQVDUQACKZCJVDCAOUQVEVCCVEUQVCVEUQNVBDUQUTURVEVAUQUTURUQURUSUEPACDUFU
GQRSTUQUBZBCKZCJVDCBOVFVGVCCVGVFVCVGVFNZVBDVHUTUSVGVAVFUTUSLVGVFUTUSUQURU
SUHPUIVGVFUJDBCUKULQRSTUMUO $.
+ $( $j usage 'axprlem3' avoids 'ax-ext'; $)
$}
- $( $j usage 'axprlem3' avoids 'ax-ext'; $)
-
${
$d x s $. $d w s $. $d t n s $.
$( Lemma for ~ axpr . The first element of the pair is included in any
@@ -47551,10 +47652,9 @@ This theorem is proved directly from set theory axioms (no set theory
ZEJZFPVDVIEPZVGCBNZUAZOZFPVAFEFEDUBUCVHVKVOFVFVGFVEFQVGFUEUFVKVHVOVKVHOVD
VNVKVFVDVGVKVCVFVDVKVIVAMZEJVCVJVPEVIVAUGUHVAEVBUIUJVEFRUKULVKVLVHVGVNVKV
AEPVLEDUMVKVAVIEVJEQVKVIVAVJERUNSTVKVFVGUOVLVNVGVLVGVMUPUQURUSUTST $.
+ $( $j usage 'axprlem4' avoids 'ax-ext'; $)
$}
- $( $j usage 'axprlem4' avoids 'ax-ext'; $)
-
${
$d y s $. $d w s $. $d n s $.
$( Lemma for ~ axpr . The second element of the pair is included in any
@@ -47569,10 +47669,9 @@ This theorem is proved directly from set theory axioms (no set theory
DVIEPZCANZVGQZOZFPFERVHVKVOFVFVGFVEFSVGFTUAVKVHVOVKVHOZVDVNVPVCVDVPVIVAMZ
EJZVCVKVRVHVJVQEVIVAUBUDUCVAEVBUEUFVFVEVKVGVEFUOUGUHVPVLIZVGVNVPVKVSVKVHU
IVIEUJUKVKVFVGULVSVNVGVLVMVGUPUMUNUQURUSUT $.
+ $( $j usage 'axprlem5' avoids 'ax-ext'; $)
$}
- $( $j usage 'axprlem5' avoids 'ax-ext'; $)
-
${
$d x z w s p $. $d y z w s p $. $d z w t n s p $.
$( Unabbreviated version of the Axiom of Pairing of ZF set theory, derived
@@ -47592,10 +47691,9 @@ This theorem is proved directly from set theory axioms (no set theory
exlimiiv ) EFIJEKFGLMGHIZNGKZDAOZDBOZPZDCIZNZDKZCQZHUPUOFGIFQUQURRSGQZUTN
ZDKZCQVCUTVDTZDKVFCABCDFGHUDVGVEDUTVDUAUEUBUPVFVBCUPVEVADUPUSVDUTUPUSVDUP
UQVDURABDEFGHUFABDEFGHUGUHUCUIUJUKULHGFEUMUN $.
+ $( $j usage 'axpr' avoids 'ax-ext'; $)
$}
- $( $j usage 'axpr' avoids 'ax-ext'; $)
-
${
$d x z w v $. $d y z w v $.
$( The Axiom of Pairing of ZF set theory. It was derived as theorem ~ axpr
@@ -54659,12 +54757,12 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
O'Rear, 25-Jan-2015.) $)
mptpreima $p |- ( `' F " C ) = { x e. A | B e. C } $=
( vy ccnv cima cv wcel wceq wa copab crab eqtri crn wex cab bitri cnvopab
- cmpt df-mpt cnveqi imaeq1i df-ima resopab rneqi ancom anass exbii df-clel
- cres 19.42v bicomi anbi2i abbii rnopab df-rab 3eqtr4i ) EHZDIAJBKZGJZCLZM
- ZGANZDIZCDKZABOZVAVFDVAVEAGNZHVFEVJEABCUBVJFAGBCUCPUDVEAGUAPUEVGVFDUMZQZV
- IVFDUFVLVCDKZVEMZGANZQZVIVKVOVEGADUGUHVNGRZASVBVHMZASVPVIVQVRAVQVBVDVMMZM
- ZGRZVRVNVTGVNVEVMMVTVMVEUIVBVDVMUJTUKWAVBVSGRZMVRVBVSGUNWBVHVBVHWBGCDULUO
- UPTTUQVNGAURVHABUSUTPPP $.
+ cmpt df-mpt cnveqi imaeq1i df-ima resopab rneqi ancom anass 19.42v dfclel
+ cres exbii bicomi anbi2i abbii rnopab df-rab 3eqtr4i ) EHZDIAJBKZGJZCLZMZ
+ GANZDIZCDKZABOZVAVFDVAVEAGNZHVFEVJEABCUBVJFAGBCUCPUDVEAGUAPUEVGVFDUMZQZVI
+ VFDUFVLVCDKZVEMZGANZQZVIVKVOVEGADUGUHVNGRZASVBVHMZASVPVIVQVRAVQVBVDVMMZMZ
+ GRZVRVNVTGVNVEVMMVTVMVEUIVBVDVMUJTUNWAVBVSGRZMVRVBVSGUKWBVHVBVHWBGCDULUOU
+ PTTUQVNGAURVHABUSUTPPP $.
$( Converse singleton image of a function defined by maps-to. (Contributed
by Stefan O'Rear, 25-Jan-2015.) $)
@@ -62935,7 +63033,6 @@ from the cartesian product of two singletons onto a singleton (case where
TWCWBCUNUOOWAVMWBTVTVIEVLUPRWAVKWCTVTWAVJECWAVJAEIEVIEAUQAURUSMRUTVAVBVCQVD
VE $.
-
${
$d A x $. $d B x $. $d C x $. $d ph x $.
rnmptc.f $e |- F = ( x e. A |-> B ) $.
@@ -147051,54 +147148,54 @@ Proper unordered pairs and triples (sets of size 2 and 3)
AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) $)
fi1uzind $p |- ( ( [. V / a ]. [. E / b ]. rh
/\ V e. Fin /\ L <_ ( # ` V ) ) -> ph ) $=
- ( vx wsbc cfn wcel chash cfv cle wbr cn0 wi cv wceq wa wex df-clel wal cz
- nn0z ad2antlr wb breq2 eqcoms biimpcd adantr imp c1 caddc co eqeq1 anbi2d
- mp1i imbi1d 2albidv weq eqcom sylan2b gen2 a1i w3a simpl sbceq1d sbceqbid
- simpr fveq2 eqeq2d anbi12d imbi12d cbval2v cc0 nn0ge0 0red nn0re zre letr
- cr syl3anc 0nn0 pm3.22 0z eluz1 mpbird eluznn0 sylancr ex syl6com pm2.43a
- cuz com14 com12 3adant1 clt nn0p1gt0 breqtrrd adantrl cvv hashgt0elex csn
- mp2b vex hashdifsnp1 syl5bi peano2nn0 ad2antrr simplrr simprlr jca spc2gv
- cdif com15 com23 mpcom mpd exlimiv sbcex sylbi 3jca difexi fveqeq2 syl5bb
- mp2an expdimp 3anbi2i anbi2i sylanb syl6an exp41 com4l com25 impcom sylan
- syl elv impancom alrimivv uzind sbccom syl5com exp31 expcom com24 pm2.43i
- expd hashcl syl11 3imp ) EQLUGZPOUGZOUHUIZNOUJUKZULUMZAUVNUNUIZUVLUVOAUOZ
- UVMUVPKUPZUVNUQZUVRUNUIZURZKUSUVLUVQUOZKUVNUNUTUWAUWBKUVSUVTUWBUVSUVTUWBU
- OUVSUVLUVTUVSUVQUVLUVSUVTUVSUVQUOUOUVOUVTUVSUVLUVSURZAUVOUVTUVSUWCAUOZUVO
- UVTURZUVSURZEQIUPZUGZPHUPZUGZUVRUWIUJUKZUQZURZBUOZIVAHVAZUWCAUWFNVBUIZUVR
- VBUIZNUVRULUMZUWONUNUIZUWPUWFSNVCVPUVTUWQUVOUVSUVRVCVDUWEUVSUWRUVOUVSUWRU
- OUVTUVSUVOUWRUVOUWRVEUVNUVRUVNUVRNULVFVGVHVIVJUWJUFUPZUWKUQZURZBUOZIVAHVA
- UWJNUWKUQZURZBUOZIVAHVAZUWJFUPZUWKUQZURZBUOZIVAHVAZUWJUXHVKVLVMZUWKUQZURZ
- BUOZIVAHVAZUWOUFFNUVRUWTNUQZUXCUXFHIUXRUXBUXEBUXRUXAUXDUWJUWTNUWKVNVOVQVR
- UFFVSZUXCUXKHIUXSUXBUXJBUXSUXAUXIUWJUWTUXHUWKVNVOVQVRUWTUXMUQZUXCUXPHIUXT
- UXBUXOBUXTUXAUXNUWJUWTUXMUWKVNVOVQVRUFKVSZUXCUWNHIUYAUXBUWMBUYAUXAUWLUWJU
- WTUVRUWKVNVOVQVRUXGUWPUXFHIUXDUWJUWKNUQBNUWKVTUDWAWBWCUXLEQJUPZUGZPGUPZUG
- ZUXHUYDUJUKZUQZURZDUOZJVAGVAZUWPUXHVBUIZNUXHULUMZWDZUXQUXKUYIHIGJHGVSZIJV
- SZURZUXJUYHBDUYPUWJUYEUXIUYGUYPUWHUYCPUWIUYDUYNUYOWEUYPEQUWGUYBUYNUYOWHWF
- WGUYNUXIUYGVEUYOUYNUWKUYFUXHUWIUYDUJWIWJVIWKUAWLWMUYMUYJUXQUYMUYJURUXPHIU
- YMUXOUYJBUYMUXHUNUIZUXOUYJBUOZUYKUYLUYQUWPUWSWNNULUMZUYKUYLURZUYQUOSNWOUY
- TUYSUYQUYKUYLUYSUYQUOZUYLUYKVUAUYSUYLUYKUYKUYQUYSUYLUYKUYKUYQUOZUOUYKUYSU
- YLURZWNUXHULUMZVUBUYKWNWTUINWTUIZUXHWTUIVUCVUDUOUYKWPUWSVUEUYKSNWQVPUXHWR
- WNNUXHWSXAVUDUYKUYQVUDUYKURZWNUNUIUXHWNXLUKUIZUYQXBVUFVUGUYKVUDURZVUDUYKX
- CWNVBUIVUGVUHVEVUFXDWNUXHXEVPXFUXHWNXGXHXIXJXIXMXKVJXNYCXOUYQUXOURWNUWKXP
- UMZUYRUYQUXNVUIUWJUXNUYQUWKUXMUQZVUIUXMUWKVTZUYQVUJURWNUXMUWKXPUYQWNUXMXP
- UMVUJUXHXQVIUYQVUJWHXRWAXSUXOUYQVUIUYRUOZUWJUXNUYQVULUOZUWJUXNVUMUOUOHUWI
- XTUIZVUIUXNUYQUWJUYRVUNVUIUXNUYQUWJUYRUOZUOUOZVUNVUIURUVRUWIUIZKUSVUPKUWI
- XTYAVUQVUPKUWJVUQUXNUYQUYRUWJVUQUXNUYQUYRUOUOZUWJVUQUREQMUGZPUWIUVRYBZYMZ
- UGZVURUBUWJVUQVVBVURUOUYQVUQVVBUXNUWJUYRUYQVUQVVBUXNVUOUOUOUYQVUQURZUXNVV
- BVUOVVCUXNVVBVUOUOZVVAUJUKUXHUQZVVCUXNURZVVDVVCUXNVVEVVCVUNVUQUYQUXNVVEUO
- VUNVVCHYDZWCUYQVUQWHUYQVUQWEUXNVUJVUNVUQUYQWDVVEVUKUVRUWIXTUXHYEYFXAVJVVE
- VVBVVFVUOUYJVVBVVFUWJVVEBUYJVVBVVFUWJVVEBUOUYJVVBURZVVFURZUWJURZUXMUNUIZU
- WJUXNVUQWDZURZVVECBVVJVVKVVLVVFVVKVVHUWJUYQVVKVUQUXNUXHYGYHVDVVJUWJUXNVUQ
- VVIUWJWHVVHVVCUXNUWJYIVVIVUQUWJVVHUYQVUQUXNYJVIUUAYKVVHVVECUOVVFUWJUYJVVB
- VVECVVAXTUIMXTUIUYJVVBVVEURZCUOZUOUWIVUTVVGUUBRUYIVVOGJVVAMXTXTUYDVVAUQZU
- YBMUQZURZUYHVVNDCVVRUYEVVBUYGVVEVVRUYCVUSPUYDVVAVVPVVQWEVVREQUYBMVVPVVQWH
- WFWGVVPUYGVVEVEVVQUYGUYFUXHUQVVPVVEUXHUYFVTUYDVVAUXHUJUUCUUDVIWKUCWLYLUUE
- UUFYHVVMVVKUWJVUJVUQWDZURCBVVLVVSVVKUXNVUJUWJVUQVUKUUGUUHUEUUIUUJUUKYNYOY
- PXIYOXIYNVJYQXIUULYRUUPXIUUMUUQVJUUNYQUUOUURUUSXIYFUUTXAUVLUVSUWOAUOZOXTU
- IZLXTUIZURZUVLUVSVVTUOUVLVWAVWBUVKPOYSUVLEPOUGZQLUGVWBEPQOLUVAVWDQLYSYTYK
- VWCUVLUVSVVTVWCUWOUWCAUWNUWDHIOLXTXTUWIOUQZUWGLUQZURZUWMUWCBAVWGUWJUVLUWL
- UVSVWGUWHUVKPUWIOVWEVWFWEVWGEQUWGLVWEVWFWHWFWGVWEUWLUVSVEVWFVWEUWKUVNUVRU
- WIOUJWIWJVIWKTWLYLYOUVGYPVJUVBUVCXMUVDUVEUVFVJYRYTOUVHUVIUVJ $.
+ ( vx wsbc cfn wcel chash cfv cle wbr cn0 wi cv wceq wa wex dfclel cz nn0z
+ wal mp1i ad2antlr wb breq2 eqcoms biimpcd adantr c1 caddc co eqeq1 anbi2d
+ imp imbi1d 2albidv weq eqcom sylan2b a1i w3a simpl simpr sbceq1d sbceqbid
+ gen2 fveq2 eqeq2d anbi12d imbi12d cbval2v cc0 nn0ge0 cr nn0re zre syl3anc
+ 0red letr cuz 0nn0 pm3.22 0z eluz1 mpbird eluznn0 sylancr syl6com pm2.43a
+ ex com14 com12 mp2b 3adant1 clt nn0p1gt0 breqtrrd adantrl cvv hashgt0elex
+ csn cdif vex hashdifsnp1 syl5bi peano2nn0 ad2antrr simplrr simprlr spc2gv
+ jca com15 com23 mpcom mpd exlimiv sbcex sylbi difexi fveqeq2 syl5bb mp2an
+ 3jca expdimp 3anbi2i anbi2i sylanb syl6an exp41 com4l syl com25 elv sylan
+ impcom impancom alrimivv uzind sbccom syl5com exp31 expcom pm2.43i hashcl
+ expd com24 syl11 3imp ) EQLUGZPOUGZOUHUIZNOUJUKZULUMZAUVNUNUIZUVLUVOAUOZU
+ VMUVPKUPZUVNUQZUVRUNUIZURZKUSUVLUVQUOZKUVNUNUTUWAUWBKUVSUVTUWBUVSUVTUWBUO
+ UVSUVLUVTUVSUVQUVLUVSUVTUVSUVQUOUOUVOUVTUVSUVLUVSURZAUVOUVTUVSUWCAUOZUVOU
+ VTURZUVSURZEQIUPZUGZPHUPZUGZUVRUWIUJUKZUQZURZBUOZIVCHVCZUWCAUWFNVAUIZUVRV
+ AUIZNUVRULUMZUWONUNUIZUWPUWFSNVBVDUVTUWQUVOUVSUVRVBVEUWEUVSUWRUVOUVSUWRUO
+ UVTUVSUVOUWRUVOUWRVFUVNUVRUVNUVRNULVGVHVIVJVPUWJUFUPZUWKUQZURZBUOZIVCHVCU
+ WJNUWKUQZURZBUOZIVCHVCZUWJFUPZUWKUQZURZBUOZIVCHVCZUWJUXHVKVLVMZUWKUQZURZB
+ UOZIVCHVCZUWOUFFNUVRUWTNUQZUXCUXFHIUXRUXBUXEBUXRUXAUXDUWJUWTNUWKVNVOVQVRU
+ FFVSZUXCUXKHIUXSUXBUXJBUXSUXAUXIUWJUWTUXHUWKVNVOVQVRUWTUXMUQZUXCUXPHIUXTU
+ XBUXOBUXTUXAUXNUWJUWTUXMUWKVNVOVQVRUFKVSZUXCUWNHIUYAUXBUWMBUYAUXAUWLUWJUW
+ TUVRUWKVNVOVQVRUXGUWPUXFHIUXDUWJUWKNUQBNUWKVTUDWAWHWBUXLEQJUPZUGZPGUPZUGZ
+ UXHUYDUJUKZUQZURZDUOZJVCGVCZUWPUXHVAUIZNUXHULUMZWCZUXQUXKUYIHIGJHGVSZIJVS
+ ZURZUXJUYHBDUYPUWJUYEUXIUYGUYPUWHUYCPUWIUYDUYNUYOWDUYPEQUWGUYBUYNUYOWEWFW
+ GUYNUXIUYGVFUYOUYNUWKUYFUXHUWIUYDUJWIWJVJWKUAWLWMUYMUYJUXQUYMUYJURUXPHIUY
+ MUXOUYJBUYMUXHUNUIZUXOUYJBUOZUYKUYLUYQUWPUWSWNNULUMZUYKUYLURZUYQUOSNWOUYT
+ UYSUYQUYKUYLUYSUYQUOZUYLUYKVUAUYSUYLUYKUYKUYQUYSUYLUYKUYKUYQUOZUOUYKUYSUY
+ LURZWNUXHULUMZVUBUYKWNWPUINWPUIZUXHWPUIVUCVUDUOUYKWTUWSVUEUYKSNWQVDUXHWRW
+ NNUXHXAWSVUDUYKUYQVUDUYKURZWNUNUIUXHWNXBUKUIZUYQXCVUFVUGUYKVUDURZVUDUYKXD
+ WNVAUIVUGVUHVFVUFXEWNUXHXFVDXGUXHWNXHXIXLXJXLXMXKVPXNXOXPUYQUXOURWNUWKXQU
+ MZUYRUYQUXNVUIUWJUXNUYQUWKUXMUQZVUIUXMUWKVTZUYQVUJURWNUXMUWKXQUYQWNUXMXQU
+ MVUJUXHXRVJUYQVUJWEXSWAXTUXOUYQVUIUYRUOZUWJUXNUYQVULUOZUWJUXNVUMUOUOHUWIY
+ AUIZVUIUXNUYQUWJUYRVUNVUIUXNUYQUWJUYRUOZUOUOZVUNVUIURUVRUWIUIZKUSVUPKUWIY
+ AYBVUQVUPKUWJVUQUXNUYQUYRUWJVUQUXNUYQUYRUOUOZUWJVUQUREQMUGZPUWIUVRYCZYDZU
+ GZVURUBUWJVUQVVBVURUOUYQVUQVVBUXNUWJUYRUYQVUQVVBUXNVUOUOUOUYQVUQURZUXNVVB
+ VUOVVCUXNVVBVUOUOZVVAUJUKUXHUQZVVCUXNURZVVDVVCUXNVVEVVCVUNVUQUYQUXNVVEUOV
+ UNVVCHYEZWBUYQVUQWEUYQVUQWDUXNVUJVUNVUQUYQWCVVEVUKUVRUWIYAUXHYFYGWSVPVVEV
+ VBVVFVUOUYJVVBVVFUWJVVEBUYJVVBVVFUWJVVEBUOUYJVVBURZVVFURZUWJURZUXMUNUIZUW
+ JUXNVUQWCZURZVVECBVVJVVKVVLVVFVVKVVHUWJUYQVVKVUQUXNUXHYHYIVEVVJUWJUXNVUQV
+ VIUWJWEVVHVVCUXNUWJYJVVIVUQUWJVVHUYQVUQUXNYKVJUUEYMVVHVVECUOVVFUWJUYJVVBV
+ VECVVAYAUIMYAUIUYJVVBVVEURZCUOZUOUWIVUTVVGUUARUYIVVOGJVVAMYAYAUYDVVAUQZUY
+ BMUQZURZUYHVVNDCVVRUYEVVBUYGVVEVVRUYCVUSPUYDVVAVVPVVQWDVVREQUYBMVVPVVQWEW
+ FWGVVPUYGVVEVFVVQUYGUYFUXHUQVVPVVEUXHUYFVTUYDVVAUXHUJUUBUUCVJWKUCWLYLUUDU
+ UFYIVVMVVKUWJVUJVUQWCZURCBVVLVVSVVKUXNVUJUWJVUQVUKUUGUUHUEUUIUUJUUKYNYOYP
+ XLYOXLYNVPYQXLUULYRUUMXLUUNUUOVPUUQYQUUPUURUUSXLYGUUTWSUVLUVSUWOAUOZOYAUI
+ ZLYAUIZURZUVLUVSVVTUOUVLVWAVWBUVKPOYSUVLEPOUGZQLUGVWBEPQOLUVAVWDQLYSYTYMV
+ WCUVLUVSVVTVWCUWOUWCAUWNUWDHIOLYAYAUWIOUQZUWGLUQZURZUWMUWCBAVWGUWJUVLUWLU
+ VSVWGUWHUVKPUWIOVWEVWFWDVWGEQUWGLVWEVWFWEWFWGVWEUWLUVSVFVWFVWEUWKUVNUVRUW
+ IOUJWIWJVJWKTWLYLYOUVGYPVPUVBUVCXMUVDUVHUVEVPYRYTOUVFUVIUVJ $.
$}
${
@@ -147159,40 +147256,40 @@ Proper unordered pairs and triples (sets of size 2 and 3)
(Contributed by Alexander van der Vekens, 7-Jan-2018.)
(New usage is discouraged.) (Proof modification is discouraged.) $)
brfi1indALT $p |- ( ( V G E /\ V e. Fin ) -> ph ) $=
- ( vx cfn wcel wbr chash cfv cn0 wi hashcl cv wa wex df-clel wal cc0 caddc
- wceq c1 co eqeq2 anbi2d imbi1d 2albidv gen2 breq12 wb fveq2 eqeq1d adantr
- anbi12d imbi12d cbval2v clt nn0re 1re a1i nn0ge0 addgegt0d simpr breqtrrd
- cr 0lt1 adantrl cvv vex hashgt0elex csn simpl hashdifsnp1 syl3anc imp w3a
- cdif peano2nn0 ad2antrr ad2antlr simplrr simprlr 3jca difexg ax-mp spc2gv
- jca mp2an expdimp syl6an exp41 com15 com23 mpcom ex mpd com4l exlimiv syl
- com25 impcom impancom alrimivv syl5bi nn0ind brrelex1i expd expcom eqcoms
- brrelex2i syl5 sylbi ) NUDUEZNKMUFZAYKNUGUHZUIUEZYLAUJZNUKYNJULZYMUSZYPUI
- UEZUMZJUNYOJYMUIUOYSYOJYQYRYOYRYOUJYMYPYMYPUSZYLYRAYLYTYRAUJYRGULZHULZMUF
- ZUUAUGUHZYPUSZUMZBUJZHUPGUPZYLYTUMZAUUCUUDUCULZUSZUMZBUJZHUPGUPUUCUUDUQUS
- ZUMZBUJZHUPGUPUUCUUDEULZUSZUMZBUJZHUPGUPZUUCUUDUUQUTURVAZUSZUMZBUJZHUPGUP
- ZUUHUCEYPUUJUQUSZUUMUUPGHUVGUULUUOBUVGUUKUUNUUCUUJUQUUDVBVCVDVEUUJUUQUSZU
- UMUUTGHUVHUULUUSBUVHUUKUURUUCUUJUUQUUDVBVCVDVEUUJUVBUSZUUMUVEGHUVIUULUVDB
- UVIUUKUVCUUCUUJUVBUUDVBVCVDVEUUJYPUSZUUMUUGGHUVJUULUUFBUVJUUKUUEUUCUUJYPU
- UDVBVCVDVEUUPGHUAVFUVAFULZIULZMUFZUVKUGUHZUUQUSZUMZDUJZIUPFUPZUUQUIUEZUVF
- UUTUVQGHFIUUAUVKUSZUUBUVLUSZUMZUUSUVPBDUWBUUCUVMUURUVOUUAUVKUUBUVLMVGUVTU
- URUVOVHUWAUVTUUDUVNUUQUUAUVKUGVIVJVKVLRVMVNUVSUVRUVFUVSUVRUMUVEGHUVSUVDUV
- RBUVSUVDUMUQUUDVOUFZUVRBUJZUVSUVCUWCUUCUVSUVCUMUQUVBUUDVOUVSUQUVBVOUFUVCU
- VSUUQUTUUQVPUTWCUEUVSVQVRUUQVSUQUTVOUFUVSWDVRVTVKUVSUVCWAWBWEUVDUVSUWCUWD
- UJZUUCUVCUVSUWEUJZUUAWFUEZUUCUVCUWFUJUJGWGZUWGUWCUVCUVSUUCUWDUWGUWCUVCUVS
- UUCUWDUJZUJUJZUWGUWCUMYPUUAUEZJUNUWJJUUAWFWHUWKUWJJUUCUWKUVCUVSUWDUUCUWKU
- VCUVSUWDUJUJZUUCUWKUMUUAYPWIZWOZLMUFZUWLSUUCUWKUWOUWLUJUVSUWKUWOUVCUUCUWD
- UVSUWKUWOUVCUWIUJUJUVSUWKUMZUVCUWOUWIUWPUVCUWOUWIUJZUWNUGUHZUUQUSZUWPUVCU
- MZUWQUWPUVCUWSUWPUWGUWKUVSUVCUWSUJUWGUWPUWHVRUVSUWKWAUVSUWKWJYPUUAWFUUQWK
- WLWMUWSUWOUWTUWIUVRUWOUWTUUCUWSBUVRUWOUWTUUCUWSBUJUVRUWOUMZUWTUMZUUCUMZUV
- BUIUEZUUCUVCUWKWNZUMUWSCBUXCUXDUXEUWTUXDUXAUUCUVSUXDUWKUVCUUQWPWQWRUXCUUC
- UVCUWKUXBUUCWAUXAUWPUVCUUCWSUXBUWKUUCUXAUVSUWKUVCWTVKXAXEUXAUWSCUJUWTUUCU
- VRUWOUWSCUWNWFUEZLWFUEUVRUWOUWSUMZCUJZUJUWGUXFUWHUUAUWMWFXBXCPUVQUXHFIUWN
- LWFWFUVKUWNUSZUVLLUSZUMZUVPUXGDCUXKUVMUWOUVOUWSUVKUWNUVLLMVGUXIUVOUWSVHUX
- JUXIUVNUWRUUQUVKUWNUGVIVJVKVLTVMXDXFXGWQUBXHXIXJXKXLXMXKXMXJWMXNXMXOXPXQX
- MXRXCWMXSXNXTYAXMYBYCYLYTUUHAUJZNWFUEZKWFUEZUMZYLYTUXLUJYLUXMUXNNKMOYDNKM
- OYHXEUXOYLYTUXLUXOUUHUUIAUUGUUIAUJGHNKWFWFUUANUSZUUBKUSZUMZUUFUUIBAUXRUUC
- YLUUEYTUUANUUBKMVGUXPUUEYTVHUXQUXPUUDYMYPUUANUGVIVJVKVLQVMXDXKYEXLWMYIYFX
- KYGWMXPYJXQXS $.
+ ( vx cfn wcel wbr chash cfv cn0 wi hashcl cv wceq wa wex dfclel wal caddc
+ cc0 c1 co eqeq2 anbi2d imbi1d 2albidv gen2 breq12 wb fveq2 eqeq1d anbi12d
+ adantr imbi12d cbval2v clt nn0re cr 1re a1i 0lt1 addgegt0d simpr breqtrrd
+ nn0ge0 adantrl cvv vex hashgt0elex csn cdif simpl hashdifsnp1 syl3anc imp
+ w3a peano2nn0 ad2antrr ad2antlr simplrr simprlr difexg ax-mp spc2gv mp2an
+ jca expdimp syl6an exp41 com15 com23 mpcom ex mpd com4l exlimiv syl com25
+ 3jca impcom impancom alrimivv syl5bi nn0ind brrelex1i brrelex2i expd syl5
+ expcom eqcoms sylbi ) NUDUEZNKMUFZAYKNUGUHZUIUEZYLAUJZNUKYNJULZYMUMZYPUIU
+ EZUNZJUOYOJYMUIUPYSYOJYQYRYOYRYOUJYMYPYMYPUMZYLYRAYLYTYRAUJYRGULZHULZMUFZ
+ UUAUGUHZYPUMZUNZBUJZHUQGUQZYLYTUNZAUUCUUDUCULZUMZUNZBUJZHUQGUQUUCUUDUSUMZ
+ UNZBUJZHUQGUQUUCUUDEULZUMZUNZBUJZHUQGUQZUUCUUDUUQUTURVAZUMZUNZBUJZHUQGUQZ
+ UUHUCEYPUUJUSUMZUUMUUPGHUVGUULUUOBUVGUUKUUNUUCUUJUSUUDVBVCVDVEUUJUUQUMZUU
+ MUUTGHUVHUULUUSBUVHUUKUURUUCUUJUUQUUDVBVCVDVEUUJUVBUMZUUMUVEGHUVIUULUVDBU
+ VIUUKUVCUUCUUJUVBUUDVBVCVDVEUUJYPUMZUUMUUGGHUVJUULUUFBUVJUUKUUEUUCUUJYPUU
+ DVBVCVDVEUUPGHUAVFUVAFULZIULZMUFZUVKUGUHZUUQUMZUNZDUJZIUQFUQZUUQUIUEZUVFU
+ UTUVQGHFIUUAUVKUMZUUBUVLUMZUNZUUSUVPBDUWBUUCUVMUURUVOUUAUVKUUBUVLMVGUVTUU
+ RUVOVHUWAUVTUUDUVNUUQUUAUVKUGVIVJVLVKRVMVNUVSUVRUVFUVSUVRUNUVEGHUVSUVDUVR
+ BUVSUVDUNUSUUDVOUFZUVRBUJZUVSUVCUWCUUCUVSUVCUNUSUVBUUDVOUVSUSUVBVOUFUVCUV
+ SUUQUTUUQVPUTVQUEUVSVRVSUUQWDUSUTVOUFUVSVTVSWAVLUVSUVCWBWCWEUVDUVSUWCUWDU
+ JZUUCUVCUVSUWEUJZUUAWFUEZUUCUVCUWFUJUJGWGZUWGUWCUVCUVSUUCUWDUWGUWCUVCUVSU
+ UCUWDUJZUJUJZUWGUWCUNYPUUAUEZJUOUWJJUUAWFWHUWKUWJJUUCUWKUVCUVSUWDUUCUWKUV
+ CUVSUWDUJUJZUUCUWKUNUUAYPWIZWJZLMUFZUWLSUUCUWKUWOUWLUJUVSUWKUWOUVCUUCUWDU
+ VSUWKUWOUVCUWIUJUJUVSUWKUNZUVCUWOUWIUWPUVCUWOUWIUJZUWNUGUHZUUQUMZUWPUVCUN
+ ZUWQUWPUVCUWSUWPUWGUWKUVSUVCUWSUJUWGUWPUWHVSUVSUWKWBUVSUWKWKYPUUAWFUUQWLW
+ MWNUWSUWOUWTUWIUVRUWOUWTUUCUWSBUVRUWOUWTUUCUWSBUJUVRUWOUNZUWTUNZUUCUNZUVB
+ UIUEZUUCUVCUWKWOZUNUWSCBUXCUXDUXEUWTUXDUXAUUCUVSUXDUWKUVCUUQWPWQWRUXCUUCU
+ VCUWKUXBUUCWBUXAUWPUVCUUCWSUXBUWKUUCUXAUVSUWKUVCWTVLXRXEUXAUWSCUJUWTUUCUV
+ RUWOUWSCUWNWFUEZLWFUEUVRUWOUWSUNZCUJZUJUWGUXFUWHUUAUWMWFXAXBPUVQUXHFIUWNL
+ WFWFUVKUWNUMZUVLLUMZUNZUVPUXGDCUXKUVMUWOUVOUWSUVKUWNUVLLMVGUXIUVOUWSVHUXJ
+ UXIUVNUWRUUQUVKUWNUGVIVJVLVKTVMXCXDXFWQUBXGXHXIXJXKXLXJXLXIWNXMXLXNXOXPXL
+ XQXBWNXSXMXTYAXLYBYCYLYTUUHAUJZNWFUEZKWFUEZUNZYLYTUXLUJYLUXMUXNNKMOYDNKMO
+ YEXEUXOYLYTUXLUXOUUHUUIAUUGUUIAUJGHNKWFWFUUANUMZUUBKUMZUNZUUFUUIBAUXRUUCY
+ LUUEYTUUANUUBKMVGUXPUUEYTVHUXQUXPUUDYMYPUUANUGVIVJVLVKQVMXCXJYFXKWNYGYHXJ
+ YIWNXOYJXPXS $.
$}
${
@@ -152628,7 +152725,6 @@ because the border cases ( ` M = N ` , ` -. ( M ..^ N ) C_ ( 0 ..^ L ) `
BAJSTOEFVBGELZTOZTVDFLVDUGUHZUISZVFPQSZVDMVGPQSZRSZUJJECFDUKVETVJULVHVIRU
MUOUNVAUTVCVAUPUQBAVBGJURUS $.
-
$d N n w $.
$( Cyclically shifting an empty set/word always results in the empty
word/set. (Contributed by AV, 25-Oct-2018.) (Revised by AV,
@@ -415132,7 +415228,6 @@ prime number equals this length (in an undirected simple graph).
FFVQWIUPZWPVQUQURWOWJWNRVQIVCUSUTVAVDVBTVQVEQWEVPVRVFQWDVRVNOVOWDVNVRWMVGVH
VIVJVKST $.
-
$( Obsolete version of ~ clwlknf1oclwwlknlem1 as of 12-Oct-2022.
(Contributed by AV, 26-May-2022.) (New usage is discouraged.)
(Proof modification is discouraged.) $)
@@ -420468,7 +420563,6 @@ that the number n of vertices in G is exactly k(k-1)+1.". Variant of
YCYDYJVATVGYEYFVGYJVGWNWNYOUWNUWOUWQOUKZUWLYNYMUUTUYKUVAABCDEFGYTILUMUNTY
GHYTYPYKYHYIYL $.
-
$( Obsolete proof of ~ 2clwwlk2clwwlk as of 12-Oct-2022. (Contributed by
AV, 28-Apr-2022.) (New usage is discouraged.)
(Proof modification is discouraged.) $)
@@ -422354,31 +422448,26 @@ summarized form such as in the Theorem List (click on "Nearby theorems"
for the hyperbolic sine.
- Minimizing axioms and the axiom of choice.
- We prefer proofs that depend on fewer and/or weaker axioms,
- even if the proofs are longer. In particular, we prefer proofs that do
- not use the axiom of choice ( ~ df-ac ) where such proofs can be found.
- The axiom of choice is widely accepted, and ZFC is the most
- commonly-accepted fundamental set of axioms for mathematics.
- However, there have been and still are some lingering controversies
- about the Axiom of Choice. Therefore, where a proof
- does not require the axiom of choice, we prefer that proof instead.
- E.g., our proof of the Schroeder-Bernstein Theorem ( ~ sbth )
- does not use the axiom of choice.
- In some cases, the weaker axiom of countable choice ( ~ ax-cc )
- or axiom of dependent choice ( ~ ax-dc ) can be used instead.
- Similarly, any theorem in first order logic (FOL) that
- contains only set variables that are all mutually distinct,
- and has no wff variables, can be proved *without* using
- ~ ax-10 through ~ ax-13 , by invoking ~ ax10w through ~ ax13w .
- We encourage proving theorems *without* ~ ax-10 through ~ ax-13
- and moving them up to the ~ ax-4 through ~ ax-9 section.
-
- For these purposes, ~ df-clel and ~ df-cleq should be considered
- axioms rather than definitions. In particular, there is no reason to
- make a proof longer if the result is that it avoids ~ ax-8 but still
- uses ~ df-clel (the latter implies the former by ~ bj-ax8 ).
- Likewise ~ df-cleq implies ~ ax-9 by ~ bj-ax9 .
+ Minimizing axiom dependencies.
+ We prefer proofs that depend on fewer and/or weaker axioms, even if
+ the proofs are longer. In particular, because of the non-constructive
+ nature of the axiom of choice ~ df-ac , we prefer proofs that do not use
+ it, or use weaker versions like countable choice ~ ax-cc or dependent
+ choice ~ ax-dc . An example is our proof of the Schroeder-Bernstein
+ Theorem ~ sbth , which does not use the axiom of choice. Similarly,
+ any theorem in first order logic (FOL) that contains only setvar
+ variables that are all mutually distinct, and has no wff variables, can
+ be proved without using ~ ax-10 through ~ ax-13 , by using ~ ax10w
+ through ~ ax13w instead.
+
+
+ We do not try to similarly reduce dependencies on definitions, since
+ definitions are conservative (they do not increase the proving power of
+ a deductive system), and are introduced in order to be used to increase
+ readability). An exception is made for the definitions ~ df-clab ,
+ ~ df-cleq , ~ df-clel , since they can be considered as axioms under
+ some definitions of what a definition is exactly (see their comments).
+
Alternate (ALT) proofs.
@@ -485111,43 +485200,42 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry
(Contributed by Thierry Arnoux, 23-Nov-2016.) $)
ballotlem2 $p |- ( P ` { c e. O | -. 1 e. c } ) = ( N / ( M + N ) ) $=
( vi c1 wcel cfv co c2 wa cle wbr mp2an cv wn crab caddc cmin cbc chash
- cdiv wceq ssrab2 ballotlemoex elpw2 mpbir fveq2 oveq1d ovex fvmpt ax-mp
- cpw wss cfz cab an32 cuz 2eluzge1 fzss1 sspwb mpbi sseli clt 1re ltnlei
- 1lt2 2re elfzle1 mto elelpwi ancom mtbi imnani jca cin ssin wo wb 1p1e2
- 1le2 cn nnge1 nnrei le2addi eqbrtrri readdcli nnaddcl nnzi eluz elfzp12
- letri cz biimpi orcanai oveq1i syl6eleq ss2abi inab abid2 ineq1i eqtr3i
- 1z 3sstr3i sstr mpan2 sylbi selpw wi wal ssab wex df-ex con1bii df-clel
- bicomi notbii imnang albii bitr4i 3bitr4ri bitr2i anbi12i anbi1i df-rab
- 3imtr4i cneg cc nncni 2cn ax-1cn 3eqtri eqtri cc0 rabeq2i 3bitr4i abbii
- impbii 3eqtr4i fveq2i cfn hashbc eluz1i mpbir2an hashfz addcli subadd23
- fzfi 2z mp3an negsubdi2i 2m1e1 negeqi oveq2i negsubi ballotlem1 oveq12i
- 0le1 0re cr crp nngt0i elrpii ltaddrp w3a elfzm11 mpbir3an bcm1n pncan2
- 0z ) LFUAZMZUBZFEUCZBNZCDUDOZLUEOZCUFOZUWBCUFOZUHOZUWBCUEOZUWBUHOZDUWBU
- HOUWAUVTUGNZEUGNZUHOZUWFUVTEUSZMZUWAUWKUIUWMUVTEUTUVSFEUJUVTECDEFGHIUKU
- LUMAUVTAUAZUGNZUWJUHOUWKUWLBUWNUVTUIUWOUWIUWJUHUWNUVTUGUNUOJUWIUWJUHUPU
- QURUWIUWDUWJUWEUHUVQUGNCUIZFPUWBVAOZUSZUCZUGNZUWIUWDUWSUVTUGUVQUWRMZUWP
- QZFVBUVQEMZUVSQZFVBUWSUVTUXBUXDFUVQLUWBVAOZUSZMZUVSQZUWPQUXGUWPQZUVSQUX
- BUXDUXGUVSUWPVCUXAUXHUWPUXAUXHUXAUXGUVSUWRUXFUVQUWQUXEUTZUWRUXFUTPLVDNZ
- MUXJVEPLUWBVFURUWQUXEVGVHVIUXAUVRUVRUXAQZUXAUVRQUXLLUWQMZUXMPLRSZLPVJSU
- XNUBVMLPVKVNVLVHLPUWBVOVPLUVQUWQVQVPUVRUXAVRVSVTWAUVQUXEUTZUVQKUAZLUIZU
- BZKVBZUTZQZUVQUWQUTZUXHUXAUYAUVQUXEUXSWBZUTZUYBUVQUXEUXSWCUYDUYCUWQUTUY
- BUXPUXEMZUXRQZKVBZUXPUWQMZKVBUYCUWQUYFUYHKUYFUXPLLUDOZUWBVAOZUWQUYEUXQU
- XPUYJMZUYEUXQUYKWDZUWBUXKMZUYEUYLWEUYMLUWBRSZLPRSPUWBRSZUYNWGUYIPUWBRWF
- LCRSZLDRSZUYIUWBRSCWHMZUYPGCWIURZDWHMZUYQHDWIURLLCDVKVKCGWJZDHWJZWKTWLZ
- LPUWBVKVNCDVUAVUBWMWRTLWSMUWBWSMZUYMUYNWEXIUWBUYRUYTUWBWHMZGHCDWNTZWOZL
- UWBWPTUMUXPLUWBWQURWTXAUYIPUWBVAWFXBXCXDUYEKVBZUXSWBUYGUYCUYEUXRKXEVUHU
- XEUXSKUXEXFXGXHKUWQXFXJUVQUYCUWQXKXLXMUXGUXOUVSUXTFUXEXNUXTUXPUVQMZUXRX
- OKXPZUVSUXRKUVQXQUXQVUIQZKXRZUBVUKUBZKXPZUVSVUJVUNVULVULVUNUBVUKKXSYBXT
- UVRVULKLUVQYAYCVUJVUIUXQQZUBZKXPVUNVUIUXQKYDVUMVUPKVUKVUOUXQVUIVRYCYEYF
- YGYHYIFUWQXNYLUUDYJUXCUXIUVSUWPFEUXFIUUAYJUUBUUCUWPFUWRYKUVSFEYKUUEUUFU
- WQUGNZCUFOZUWTUWDUWQUUGMCWSMZVURUWTUIPUWBUUNCGWOZFUWQCUUHTVUQUWCCUFVUQU
- WBLYMZUDOZUWCVUQUWBPUEOLUDOZUWBLPUEOZUDOZVVBUWBPVDNMZVUQVVCUIVVFVUDUYOV
- UGVUCPUWBUUOUUIUUJPUWBUUKURUWBYNMPYNMLYNMVVCVVEUICDCGYOZDHYOZUULZYPYQUW
- BPLUUMUUPVVDVVAUWBUDPLUEOZYMVVDVVAPLYPYQUUQVVJLUURUUSXHUUTYRUWBLVVIYQUV
- AYSXBXHXHCDEFGHIUVBUVCYSCYTUWCVAOMZVUEUWFUWHUIVVKVUSYTCRSZCUWBVJSZVUTYT
- LRSUYPVVLUVDUYSYTLCUVEVKVUAWRTCUVFMDUVGMVVMVUADVUBDHUVHUVICDUVJTYTWSMVU
- DVVKVUSVVLVVMUVKWEUVPVUGCYTUWBUVLTUVMVUFCUWBUVNTUWGDUWBUHCYNMDYNMUWGDUI
- VVGVVHCDUVOTXBYR $.
+ cdiv cpw wceq cvv ballotlemoex ssrab2 elpwi2 fveq2 ovex fvmpt ax-mp cfz
+ oveq1d an32 wss cuz 2eluzge1 fzss1 sspwb mpbi sseli clt 1lt2 1re ltnlei
+ 2re elfzle1 mto elelpwi ancom mtbi imnani jca cab ssin wo wb 1le2 1p1e2
+ cin cn nnge1 nnrei le2addi eqbrtrri readdcli letri cz nnaddcl nnzi eluz
+ mpbir elfzp12 biimpi orcanai oveq1i syl6eleq ss2abi abid2 ineq1i eqtr3i
+ 1z inab 3sstr3i sstr mpan2 sylbi selpw wi wal ssab df-ex bicomi con1bii
+ dfclel notbii imnang bitr4i 3bitr4ri bitr2i anbi12i 3imtr4i anbi1i cneg
+ wex albii cc nncni 2cn ax-1cn 3eqtri eqtri cc0 rabeq2i 3bitr4i cfn fzfi
+ impbii rabbia2 fveq2i hashbc eluz1i mpbir2an hashfz subadd23 negsubdi2i
+ 2z addcli mp3an 2m1e1 negeqi oveq2i negsubi ballotlem1 oveq12i 0le1 0re
+ cr crp nngt0i elrpii ltaddrp w3a 0z elfzm11 mpbir3an bcm1n pncan2 ) LFU
+ AZMZUBZFEUCZBNZCDUDOZLUEOZCUFOZUWACUFOZUHOZUWACUEOZUWAUHOZDUWAUHOUVTUVS
+ UGNZEUGNZUHOZUWEUVSEUIZMUVTUWJUJUVSEUKCDEFGHIULUVRFEUMUNAUVSAUAZUGNZUWI
+ UHOUWJUWKBUWLUVSUJUWMUWHUWIUHUWLUVSUGUOUTJUWHUWIUHUPUQURUWHUWCUWIUWDUHU
+ VPUGNCUJZFPUWAUSOZUIZUCZUGNZUWHUWCUWQUVSUGUWNUVRFUWPEUVPLUWAUSOZUIZMZUV
+ RQZUWNQUXAUWNQZUVRQUVPUWPMZUWNQUVPEMZUVRQUXAUVRUWNVAUXDUXBUWNUXDUXBUXDU
+ XAUVRUWPUWTUVPUWOUWSVBZUWPUWTVBPLVCNZMUXFVDPLUWAVEURUWOUWSVFVGVHUXDUVQU
+ VQUXDQZUXDUVQQUXHLUWOMZUXIPLRSZLPVISUXJUBVJLPVKVMVLVGLPUWAVNVOLUVPUWOVP
+ VOUVQUXDVQVRVSVTUVPUWSVBZUVPKUAZLUJZUBZKWAZVBZQZUVPUWOVBZUXBUXDUXQUVPUW
+ SUXOWGZVBZUXRUVPUWSUXOWBUXTUXSUWOVBUXRUXLUWSMZUXNQZKWAZUXLUWOMZKWAUXSUW
+ OUYBUYDKUYBUXLLLUDOZUWAUSOZUWOUYAUXMUXLUYFMZUYAUXMUYGWCZUWAUXGMZUYAUYHW
+ DUYILUWARSZLPRSPUWARSZUYJWEUYEPUWARWFLCRSZLDRSZUYEUWARSCWHMZUYLGCWIURZD
+ WHMZUYMHDWIURLLCDVKVKCGWJZDHWJZWKTWLZLPUWAVKVMCDUYQUYRWMWNTLWOMUWAWOMZU
+ YIUYJWDXIUWAUYNUYPUWAWHMZGHCDWPTZWQZLUWAWRTWSUXLLUWAWTURXAXBUYEPUWAUSWF
+ XCXDXEUYAKWAZUXOWGUYCUXSUYAUXNKXJVUDUWSUXOKUWSXFXGXHKUWOXFXKUVPUXSUWOXL
+ XMXNUXAUXKUVRUXPFUWSXOUXPUXLUVPMZUXNXPKXQZUVRUXNKUVPXRUXMVUEQZKYLZUBVUG
+ UBZKXQZUVRVUFVUJVUHVUHVUJUBVUGKXSXTYAUVQVUHKLUVPYBYCVUFVUEUXMQZUBZKXQVU
+ JVUEUXMKYDVUIVULKVUGVUKUXMVUEVQYCYMYEYFYGYHFUWOXOYIUUEYJUXEUXCUVRUWNFEU
+ WTIUUAYJUUBUUFUUGUWOUGNZCUFOZUWRUWCUWOUUCMCWOMZVUNUWRUJPUWAUUDCGWQZFUWO
+ CUUHTVUMUWBCUFVUMUWALYKZUDOZUWBVUMUWAPUEOLUDOZUWALPUEOZUDOZVURUWAPVCNMZ
+ VUMVUSUJVVBUYTUYKVUCUYSPUWAUUNUUIUUJPUWAUUKURUWAYNMPYNMLYNMVUSVVAUJCDCG
+ YOZDHYOZUUOZYPYQUWAPLUULUUPVUTVUQUWAUDPLUEOZYKVUTVUQPLYPYQUUMVVFLUUQUUR
+ XHUUSYRUWALVVEYQUUTYSXCXHXHCDEFGHIUVAUVBYSCYTUWBUSOMZVUAUWEUWGUJVVGVUOY
+ TCRSZCUWAVISZVUPYTLRSUYLVVHUVCUYOYTLCUVDVKUYQWNTCUVEMDUVFMVVIUYQDUYRDHU
+ VGUVHCDUVITYTWOMUYTVVGVUOVVHVVIUVJWDUVKVUCCYTUWAUVLTUVMVUBCUWAUVNTUWFDU
+ WAUHCYNMDYNMUWFDUJVVCVVDCDUVOTXCYR $.
$}
$d c i F $. $d j F $. $d k F $.
@@ -508631,14 +508719,14 @@ Real and complex numbers (cont.)
Scott Fenton, 21-Jan-2017.) $)
eldm3 $p |- ( A e. dom B <-> ( B |` { A } ) =/= (/) ) $=
( vx vy vp vz cdm wcel cvv csn cres c0 wne wceq cv eleq1 cop wex wa exbii
- elex wn snprc reseq2 res0 syl6eq necon1ai sneq reseq2d neeq1d df-clel vex
- sylbi eldm2 n0 elres weq pm5.32i opeq1 eqeq2d anbi1d syl5bbr exbidv rexsn
- wrex bitri excom 3bitri 3bitr4i vtoclbg pm5.21nii ) ABGZHZAIHZBAJZKZLMZAV
- LUAVNVPLVNUBVOLNZVPLNAUCVRVPBLKLVOLBUDBUEUFUMUGCOZVLHZBVSJZKZLMZVMVQCAIVS
- AVLPVSANZWBVPLWDWAVOBVSAUHUIUJVSDOZQZBHZDREOZWFNZWHBHZSZERZDRZVTWCWGWLDEW
- FBUKTDVSBCULZUNWCWHWBHZERWKDRZERWMEWBUOWOWPEWOWHFOZWEQZNZWRBHZSZDRZFWAVEW
- PFDWHBWAUPXBWPFVSWNFCUQZXAWKDXAWSWJSXCWKWSWJWTWHWRBPURXCWSWIWJXCWRWFWHWQV
- SWEUSUTVAVBVCVDVFTWKEDVGVHVIVJVK $.
+ elex wn snprc reseq2 res0 syl6eq sylbi necon1ai reseq2d neeq1d dfclel vex
+ sneq eldm2 n0 wrex elres pm5.32i opeq1 eqeq2d anbi1d syl5bbr exbidv rexsn
+ weq bitri excom 3bitri 3bitr4i vtoclbg pm5.21nii ) ABGZHZAIHZBAJZKZLMZAVL
+ UAVNVPLVNUBVOLNZVPLNAUCVRVPBLKLVOLBUDBUEUFUGUHCOZVLHZBVSJZKZLMZVMVQCAIVSA
+ VLPVSANZWBVPLWDWAVOBVSAUMUIUJVSDOZQZBHZDREOZWFNZWHBHZSZERZDRZVTWCWGWLDEWF
+ BUKTDVSBCULZUNWCWHWBHZERWKDRZERWMEWBUOWOWPEWOWHFOZWEQZNZWRBHZSZDRZFWAUPWP
+ FDWHBWAUQXBWPFVSWNFCVEZXAWKDXAWSWJSXCWKWSWJWTWHWRBPURXCWSWIWJXCWRWFWHWQVS
+ WEUSUTVAVBVCVDVFTWKEDVGVHVIVJVK $.
$}
$( Quantifier-free definition of membership in a range. (Contributed by
@@ -524639,16 +524727,6 @@ Utility lemmas or strengthenings of theorems in the main part (biconditional
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
$)
- ${
- $d x z $. $d y z $.
- $( A form of ~ elequ2 with a universal quantifier. Its converse is
- ~ ax-ext . (TODO: move to main part, minimize ~ axext4 --- as of
- 4-Nov-2020, minimizes only ~ axext4 , by 13 bytes; and link to it in the
- comment of ~ ax-ext .) (Contributed by BJ, 3-Oct-2019.) $)
- bj-elequ2g $p |- ( x = y -> A. z ( z e. x <-> z e. y ) ) $=
- ( weq wel wb elequ2 alrimiv ) ABDCAECBEFCABCGH $.
- $}
-
$( A theorem which could be used as sole axiom for the non-logical predicate
instead of ~ ax-8 and ~ ax-9 . Indeed, it is implied over propositional
calculus by the conjunction of ~ ax-8 and ~ ax-9 , as proved here. In the
@@ -525481,11 +525559,6 @@ at least two objects (see ~ bj-dtru ). (Contributed by BJ,
( vw wel wb wal wi elequ2 bibi1d albidv equequ1 imbi12d ax-ext bj-chvarvv
weq ) CDEZCBEZFZCGZDBPZHCAEZRFZCGZABPZHDADAPZTUDUAUEUFSUCCUFQUBRDACIJKDAB
LMDBCNO $.
-
- $( Remove dependency on ~ ax-13 from ~ axext4 . (Contributed by BJ,
- 6-Oct-2019.) (Proof modification is discouraged.) $)
- bj-axext4 $p |- ( x = y <-> A. z ( z e. x <-> z e. y ) ) $=
- ( weq wel wb wal bj-elequ2g bj-axext3 impbii ) ABDCAECBEFCGABCHABCIJ $.
$}
${
@@ -525596,7 +525669,7 @@ at least two objects (see ~ bj-dtru ). (Contributed by BJ,
23-Jun-2019.) (Proof modification is discouraged.) $)
bj-clabel $p |- ( { x | ph } e. A <->
E. y ( y e. A /\ A. x ( x e. y <-> ph ) ) ) $=
- ( cab wcel cv wceq wa wex wel wb wal df-clel bj-abeq2 anbi2ci exbii bitri
+ ( cab wcel cv wceq wa wex wel wb wal dfclel bj-abeq2 anbi2ci exbii bitri
) ABEZDFCGZSHZTDFZIZCJUBBCKALBMZIZCJCSDNUCUECUAUDUBABTOPQR $.
$}
@@ -526388,14 +526461,14 @@ The proof goes by induction on the complexity of the formula (see op. cit.
(Proof modification is discouraged.) (New usage is discouraged.) $)
eliminable3a $p |-
( { x | ph } e. y <-> E. z ( z = { x | ph } /\ z e. y ) ) $=
- ( cab cv df-clel ) DABECFG $.
+ ( cab cv dfclel ) DABECFG $.
$( A theorem used to prove the base case of the Eliminability Theorem (see
section comment). (Contributed by BJ, 19-Oct-2019.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
eliminable3b $p |- ( { x | ph } e. { y | ps } <->
E. z ( z = { x | ph } /\ z e. { y | ps } ) ) $=
- ( cab df-clel ) EACFBDFG $.
+ ( cab dfclel ) EACFBDFG $.
$}
${
@@ -526436,8 +526509,9 @@ written as (is equal to) a class abstraction does not require these
last statement should be ~ df-cleq .
Note that without ~ ax-ext , the $a-statements ~ df-clab , ~ df-cleq , and
- ~ df-clel are no longer eliminable (see previous section) (but PROBABLY are
- still conservative). This is not a reason not to study what is provable
+ ~ df-clel are no longer eliminable (see previous section) (but PROBABLY
+ ~ df-clab is still conservative , while ~ df-cleq and ~ df-clel are not).
+ This is not a reason not to study what is provable
with them but without ~ ax-ext , in order to gauge their strengths more
precisely.
@@ -526456,23 +526530,6 @@ written as (is equal to) a class abstraction does not require these
$)
- ${
- $d x z $. $d y z $. $d ph z $.
- $( An instance of ~ df-clel where the LHS (the definiendum) has the form
- "setvar ` e. ` class abstraction". The straightforward yet important
- fact that this statement can be proved from FOL= and ~ df-clab (hence
- without ~ df-clel or ~ df-cleq ) was stressed by Mario Carneiro. The
- instance of ~ df-clel where the LHS has the form "setvar ` e. ` setvar"
- is proved as ~ cleljust , from FOL= and ~ ax-8 . (Contributed by BJ,
- 8-Nov-2021.) (Proof modification is discouraged.) $)
- bj-cleljustab $p |-
- ( x e. { y | ph } <-> E. z ( z = x /\ z e. { y | ph } ) ) $=
- ( cv cab wcel wsb weq wa df-clab ax6ev biantrur 19.41v bicomi sbequ exbii
- wex wb 3bitri equcoms pm5.32i anbi2i ) BEACFZGACBHZDBIZACDHZJZDRZUFDEUDGZ
- JZDRABCKUEUFDRZUEJZUFUEJZDRZUIULUEDBLMUOUMUFUEDNOUNUHDUFUEUGUEUGSBDABDCPU
- AUBQTUHUKDUGUJUFUJUGADCKOUCQT $.
- $}
-
$( Closed form of ~ bj-vexw . (Contributed by BJ, 14-Jun-2019.)
(Proof modification is discouraged.) $)
bj-vexwt $p |- ( A. x ph -> y e. { x | ph } ) $=
@@ -526532,9 +526589,9 @@ to being a member of a class abstraction (that every class is equal to a
See also ~ bj-denotesv and comments there. (Contributed by BJ,
29-Apr-2019.) (Proof modification is discouraged.) $)
bj-denotes $p |- ( E. x x = A <-> E. y y = A ) $=
- ( vz cv wceq wex wi cab wcel wa id bj-vexw biantru df-clel 3bitr2i bicomi
- exbii bitri ) AEZCFZAGZBEZCFZUCDEZUEFZUFHZDIZJZKZBGZUDBGUBUATUHJZKZAGCUHJ
- UKUAUMAULUAUGDAUFLZMNRACUHOBCUHOPUJUDBUDUJUIUDUGDBUNMNQRS $.
+ ( vz cv wceq wex wi cab wa id bj-vexw biantru exbii dfclel 3bitr2i bicomi
+ wcel bitri ) AEZCFZAGZBEZCFZUCDEZUEFZUFHZDIZRZJZBGZUDBGUBUATUHRZJZAGCUHRU
+ KUAUMAULUAUGDAUFKZLMNACUHOBCUHOPUJUDBUDUJUIUDUGDBUNLMQNS $.
$}
${
@@ -526556,9 +526613,9 @@ to being a member of a class abstraction (that every class is equal to a
$( Closed form of ~ bj-issetw . (Contributed by BJ, 29-Apr-2019.)
(Proof modification is discouraged.) $)
bj-issetwt $p |- ( A. x ph -> ( A e. { x | ph } <-> E. y y = A ) ) $=
- ( vz wal cab wcel cv wceq wex df-clel a1i bj-vexwt biantrud bicomd exbidv
- wa wb bj-denotes 3bitrd ) ABFZDABGZHZEIZDJZUEUCHZRZEKZUFEKZCIDJCKZUDUISUB
- EDUCLMUBUHUFEUBUFUHUBUGUFABENOPQUJUKSUBECDTMUA $.
+ ( vz wal cab wcel cv wa wex wb dfclel a1i bj-vexwt biantrud bicomd exbidv
+ wceq bj-denotes 3bitrd ) ABFZDABGZHZEIZDSZUEUCHZJZEKZUFEKZCIDSCKZUDUILUBE
+ DUCMNUBUHUFEUBUFUHUBUGUFABEOPQRUJUKLUBECDTNUA $.
$}
${
@@ -526581,8 +526638,8 @@ to being a member of a class abstraction (that every class is equal to a
~ bj-elisset when sufficient. (Contributed by BJ, 14-Sep-2019.)
(Proof modification is discouraged.) $)
bj-elissetv $p |- ( A e. V -> E. x x = A ) $=
- ( wcel cv wceq wa wex df-clel exsimpl sylbi ) BCDAEZBFZLCDZGAHMAHABCIMNAJ
- K $.
+ ( wcel cv wceq wa wex dfclel exsimpl sylbi ) BCDAEZBFZLCDZGAHMAHABCIMNAJK
+ $.
$}
${
@@ -526933,126 +526990,24 @@ but the latter requires a domain with at least two objects (hence uses
Proposal for the definitions of class membership and class equality
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
- In this section, we show ( ~ bj-ax8 and ~ bj-ax9 ) that the current forms of
- the definitions of class membership ( ~ df-clel ) and class equality
- ( ~ df-cleq ) are too powerful, and we propose alternate definitions
- ( ~ bj-df-clel and ~ bj-df-cleq ) which also have the advantage of making it
- clear that these definitions are conservative.
+ Note: now that the proposals have been adopted as ~ df-cleq and ~ df-clel ,
+ and that ~ ax9ALT is in the main section, we only keep ~ bj-ax9 here as a
+ weaker version of ~ ax9ALT proved without ~ ax-8 .
$)
- ${
- $d u x $. $d u y $. $d u z $.
- $( Proof of ~ ax-8 from ~ df-clel (and FOL). This shows that ~ df-clel is
- "too powerful". A possible definition is given by ~ bj-df-clel .
- (Contributed by BJ, 27-Jun-2019.) Also a direct consequence of
- ~ eleq1w , which has essentially the same proof.
- (Proof modification is discouraged.) $)
- bj-ax8 $p |- ( x = y -> ( x e. z -> y e. z ) ) $=
- ( vu weq wel wa wex equequ2 anbi1d exbidv cv df-clel 3bitr4g biimpd ) ABE
- ZACFZBCFZPDAEZDCFZGZDHDBEZTGZDHQRPUAUCDPSUBTABDIJKDALCLZMDBLUDMNO $.
- $}
-
- ${
- $d u v w x A $. $d u v w x B $.
- bj-df-clel.1 $e |- A. u A. v ( u e. v <-> E. w ( w = u /\ w e. v ) ) $.
- $( Candidate definition for ~ df-clel (the need for it is exposed in
- ~ bj-ax8 ). The similarity of the hypothesis
- ` |- A. u A. v ( u e. v <-> E. w ( w = u /\ w e. v ) ) ` and the
- conclusion, together with all possible disjoint variable conditions,
- makes it clear that this definition merely extends to class variables
- something that is true for setvar variables, hence is conservative.
- This definition should be directly referenced only by ~ bj-dfclel ,
- which should be used instead. The proof is irrelevant since this is a
- proposal for an axiom.
-
- Note: the current definition ~ df-clel already mentions ~ cleljust as a
- justification; here, we merely propose to put it (more preciesly: its
- universal closure) as a hypothesis to make things more explicit.
- (Contributed by BJ, 27-Jun-2019.)
- (Proof modification is discouraged.) $)
- bj-df-clel $p |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $=
- ( df-clel ) AEFH $.
- $}
-
- ${
- $d u v w x A $. $d u v w x B $.
- $( Characterization of the elements of a class. Note: ~ cleljust could be
- relabeled "clelhyp". (Contributed by BJ, 27-Jun-2019.)
- (Proof modification is discouraged.) $)
- bj-dfclel $p |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $=
- ( vw vv vu wel weq wa wex wb cleljust gen2 bj-df-clel ) ADEFBCFEGDFHDEGID
- JKFEFEDLMN $.
- $}
-
${
$d x z $. $d y z $. $d u w z $.
- $( Proof of ~ ax-9 from Tarski's FOL=, ~ sp , ~ df-cleq and ~ ax-ext (with
+ $( Proof of ~ ax-9 from Tarski's FOL=, ~ sp , ~ dfcleq and ~ ax-ext (with
two extra disjoint variable conditions on ` x , z ` and ` y , z ` ).
- For a version without these disjoint variable conditions, see
- ~ bj-ax9-2 . This shows that ~ df-cleq is "too powerful". A possible
- definition is given by ~ bj-df-cleq . (Contributed by BJ, 24-Jun-2019.)
- (Proof modification is discouraged.) $)
+ See ~ ax9ALT for a more general version, proved using also ~ ax-8 .
+ (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
+ (New usage is discouraged.) $)
bj-ax9 $p |- ( x = y -> ( z e. x -> z e. y ) ) $=
- ( vu vw weq wel wb wal wi cv ax-ext df-cleq biimp sps sylbi ) ABFCAGZCBGZ
- HZCIQRJZCDEAKBKDECLMSTCQRNOP $.
- $}
-
- ${
- $d u v w $. $d u x $. $d u y $. $d u z $.
- $( Proof of ~ ax-9 from Tarski's FOL=, ~ ax-8 (specifically, ~ ax8v1 and
- ~ ax8v2 ) , ~ df-cleq and ~ ax-ext . For a version not using ~ ax-8 ,
- see ~ bj-ax9 . This shows that ~ df-cleq is "too powerful". A possible
- definition is given by ~ bj-df-cleq . (Contributed by BJ, 24-Jun-2019.)
- (Proof modification is discouraged.) $)
- bj-ax9-2 $p |- ( x = y -> ( z e. x -> z e. y ) ) $=
- ( vu vv vw weq wel wi wal wb cv ax-ext df-cleq biimpi biimp ax8v2 equcoms
- sylg ax8v1 imim12d spimvw syl ) ABGZDAHZDBHZIZDJCAHZCBHZIZUDUEUFKZUGDUDUK
- DJDEFALBLEFDMNOUEUFPSUGUJDCDCGUHUEUFUIUHUEICDCDAQRDCBTUAUBUC $.
- $}
-
- ${
- $d z x $. $d z y $.
- $( The hypothesis of ~ bj-df-cleq . Note that the hypothesis of
- ~ bj-df-cleq actually has an additional disjoint variable condition on
- ` x , y ` and therefore is provable by simply using ~ ax-ext in place of
- ~ axext3 in the current proof. (Contributed by BJ, 24-Jun-2019.)
- (Proof modification is discouraged.) $)
- bj-cleqhyp $p |- ( x = y <-> A. z ( z e. x <-> z e. y ) ) $=
- ( weq wel wb wal bj-elequ2g axext3 impbii ) ABDCAECBEFCGABCHABCIJ $.
- $}
-
- ${
- $d u v w x A $. $d u v w x B $.
- bj-df-cleq.1 $e |- A. u A. v ( u = v <-> A. w ( w e. u <-> w e. v ) ) $.
- $( Candidate definition for ~ df-cleq (the need for it is exposed in
- ~ bj-ax9 ). The similarity of the hypothesis
- ` |- A. u A. v ( u = v <-> A. w ( w e. u <-> w e. v ) ) ` and the
- conclusion makes it clear that this definition merely extends to class
- variables something that is true for setvar variables, hence is
- conservative. This definition should be directly referenced only by
- ~ bj-dfcleq , which should be used instead. The proof is irrelevant
- since this is a proposal for an axiom.
-
- Another definition, which would give finer control, is actually the pair
- of definitions where each has one implication of the present
- biconditional as hypothesis and conclusion. They assert that
- extensionality (respectively, the left-substitution axiom for the
- membership predicate) extends from setvars to classes. (Contributed by
- BJ, 24-Jun-2019.) (Proof modification is discouraged.) $)
- bj-df-cleq $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $=
- ( dfcleq ) AEFH $.
- $}
-
- ${
- $d u v w x A $. $d u v w x B $.
- $( Proof of class extensionality from the axiom of set extensionality
- ( ~ ax-ext ) and the definition of class equality ( ~ bj-df-cleq ).
- (Contributed by BJ, 24-Jun-2019.)
- (Proof modification is discouraged.) $)
- bj-dfcleq $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $=
- ( vw vv vu weq wel wb wal bj-cleqhyp gen2 bj-df-cleq ) ADEFBCFEGDFHDEHIDJ
- IFEFEDKLM $.
+ ( weq wel wb wal wi cv dfcleq biimp sps sylbi ) ABDCAEZCBEZFZCGNOHZCAIBIJ
+ PQCNOKLM $.
+ $( $j usage 'bj-ax9' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-13' 'df-clab'
+ 'df-clel'; $)
$}
@@ -527549,11 +527504,9 @@ FOL part ( ~ bj-ru0 ) and then two versions ( ~ bj-ru1 and ~ bj-ru ).
${
$d x y $. $d y V $.
$( Remove dependency on ~ ax-13 (and ~ df-v ) from Russell's paradox ~ ru
- expressed with primitive symbols and with a class variable ` V ` (note
- that ~ axsep2 does require ~ ax-8 and ~ ax-9 since it requires ~ df-clel
- and ~ df-cleq --- see ~ bj-df-clel and ~ bj-df-cleq ). Note the more
- economical use of ~ bj-elissetv instead of ~ isset to avoid use of
- ~ df-v . (Contributed by BJ, 12-Oct-2019.)
+ expressed with primitive symbols and with a class variable ` V ` . Note
+ the more economical use of ~ bj-elissetv instead of ~ isset to avoid use
+ of ~ df-v . (Contributed by BJ, 12-Oct-2019.)
(Proof modification is discouraged.) $)
bj-ru $p |- -. { x | -. x e. x } e. V $=
( vy wel wn cab wcel cv wceq wex bj-ru1 bj-elissetv mto ) AADEAFZBGCHNICJ
@@ -527934,11 +527887,11 @@ quantifiers appear (since they typically require ~ ax-10 to work with).
$( Characterization of the elements of the singletonization of a class.
(Contributed by BJ, 6-Oct-2018.) $)
bj-elsngl $p |- ( A e. sngl B <-> E. x e. B A = { x } ) $=
- ( vy bj-csngl wcel cv wceq wa wex csn wrex df-bj-sngl abeq2i anbi2i exbii
- df-clel r19.42v bicomi 3bitri rexcom4 eqcom snex eqvinc exancom rexbii )
- BCEZFDGZBHZUHUGFZIZDJUIUHAGZKZHZACLZIZDJZBUMHZACLZDBUGQUKUPDUJUOUIUODUGDA
- CMNOPUQUIUNIZACLZDJZUTDJZACLZUSUPVADVAUPUIUNACRSPVDVBUTADCUASVCURACURVCUR
- UMBHUNUIIDJVCBUMUBDUMBULUCUDUNUIDUETSUFTT $.
+ ( vy bj-csngl wcel cv wceq wa wex csn wrex dfclel df-bj-sngl abeq2i exbii
+ anbi2i r19.42v bicomi 3bitri rexcom4 eqcom snex eqvinc exancom rexbii ) B
+ CEZFDGZBHZUHUGFZIZDJUIUHAGZKZHZACLZIZDJZBUMHZACLZDBUGMUKUPDUJUOUIUODUGDAC
+ NOQPUQUIUNIZACLZDJZUTDJZACLZUSUPVADVAUPUIUNACRSPVDVBUTADCUASVCURACURVCURU
+ MBHUNUIIDJVCBUMUBDUMBULUCUDUNUIDUETSUFTT $.
$}
${
@@ -529209,8 +529162,7 @@ automatically a set (see ~ bj-mooreset ). (Contributed by BJ,
PUSURFGUOHUBUETUFTUGUHCIUMFUIABIDEGCUJUK $.
$}
- $( Extend the definition of a class to include maps-to notation for functions
- with three arguments. $)
+ $( Syntax for maps-to notation for functions with three arguments. $)
cmpt3 $a class ( x e. A , y e. B , z e. C |-> D ) $.
${
@@ -533807,9 +533759,9 @@ sides of the biconditional correlate (they are the same), if they exist at
$( Rederive ~ df-clab from ~ wl-clabv . (Contributed by Wolf Lammen,
31-May-2023.) $)
wl-dfclab $p |- ( x e. { y | ph } <-> [ x / y ] ph ) $=
- ( vz cv cab wcel weq wex wsb df-clel wl-clabv sbequ syl5bb pm5.32i 19.41v
- wa exbii ax6ev biantrur bitr4i 3bitri ) BEZACFZGDBHZDEUDGZQZDIUEACBJZQZDI
- ZUHDUCUDKUGUIDUEUFUHUFACDJUEUHADCLADBCMNORUJUEDIZUHQUHUEUHDPUKUHDBSTUAUB
+ ( vz cv cab wcel weq wa wex wsb dfclel wl-clabv sbequ syl5bb exbii 19.41v
+ pm5.32i ax6ev biantrur bitr4i 3bitri ) BEZACFZGDBHZDEUDGZIZDJUEACBKZIZDJZ
+ UHDUCUDLUGUIDUEUFUHUFACDKUEUHADCMADBCNORPUJUEDJZUHIUHUEUHDQUKUHDBSTUAUB
$.
$}
@@ -619705,18 +619657,6 @@ fixed reference functional determined by this vector (corresponding to
UCBCGHLLPUDAUGDHLTGJLNAGUAJUBUCCDHLQUEADEHKLORSUFUFUF $.
$}
- ${
- $d x a $. $d x b $. $d x ph $.
- $( A version of ~ cleljust where the second class is instead replaced with
- a class abstraction. This provides another part of the justification
- for ~ df-clel . See also ~ bj-cleljustab . (Contributed by Steven
- Nguyen, 19-May-2023.) $)
- cleljust2 $p |-
- ( a e. { b | ph } <-> E. x ( x = a /\ x e. { b | ph } ) ) $=
- ( weq cv cab wcel wa wex wsb sbequ df-clab 3bitr4g equsexvw bicomi ) BCEZ
- BFADGZHZIBJCFRHZSTBCQADBKADCKSTABCDLABDMACDMNOP $.
- $}
-
${
sn-vexw.1 $e |- ph $.
$( A universal class. Proof of ~ bj-vexw using only ~ ax-mp through