HomeHome Intuitionistic Logic Explorer
Theorem List (p. 73 of 152)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 7201-7300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcarden2bex 7201* If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
 |-  ( ( A  ~~  B  /\  E. x  e. 
 On  x  ~~  A )  ->  ( card `  A )  =  ( card `  B ) )
 
Theorempm54.43 7202 Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.)
 |-  ( ( A  ~~  1o  /\  B  ~~  1o )  ->  ( ( A  i^i  B )  =  (/) 
 <->  ( A  u.  B )  ~~  2o ) )
 
Theorempr2nelem 7203 Lemma for pr2ne 7204. (Contributed by FL, 17-Aug-2008.)
 |-  ( ( A  e.  C  /\  B  e.  D  /\  A  =/=  B ) 
 ->  { A ,  B }  ~~  2o )
 
Theorempr2ne 7204 If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)
 |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( { A ,  B }  ~~  2o  <->  A  =/=  B ) )
 
Theoremexmidonfinlem 7205* Lemma for exmidonfin 7206. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
 |-  A  =  { { x  e.  { (/) }  |  ph
 } ,  { x  e.  { (/) }  |  -.  ph
 } }   =>    |-  ( om  =  ( On  i^i  Fin )  -> DECID  ph )
 
Theoremexmidonfin 7206 If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6885 and nnon 4621. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
 |-  ( om  =  ( On  i^i  Fin )  -> EXMID )
 
Theoremen2eleq 7207 Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
 |-  ( ( X  e.  P  /\  P  ~~  2o )  ->  P  =  { X ,  U. ( P 
 \  { X }
 ) } )
 
Theoremen2other2 7208 Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
 |-  ( ( X  e.  P  /\  P  ~~  2o )  ->  U. ( P  \  { U. ( P  \  { X } ) }
 )  =  X )
 
Theoremdju1p1e2 7209 Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
 |-  ( 1o 1o )  ~~  2o
 
Theoreminfpwfidom 7210 The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption 
( ~P A  i^i  Fin )  e.  _V because this theorem also implies that  A is a set if  ~P A  i^i  Fin is.) (Contributed by Mario Carneiro, 17-May-2015.)
 |-  ( ( ~P A  i^i  Fin )  e.  _V  ->  A  ~<_  ( ~P A  i^i  Fin ) )
 
Theoremexmidfodomrlemeldju 7211 Lemma for exmidfodomr 7216. A variant of djur 7081. (Contributed by Jim Kingdon, 2-Jul-2022.)
 |-  ( ph  ->  A  C_ 
 1o )   &    |-  ( ph  ->  B  e.  ( A 1o )
 )   =>    |-  ( ph  ->  ( B  =  (inl `  (/) )  \/  B  =  (inr `  (/) ) ) )
 
Theoremexmidfodomrlemreseldju 7212 Lemma for exmidfodomrlemrALT 7215. A variant of eldju 7080. (Contributed by Jim Kingdon, 9-Jul-2022.)
 |-  ( ph  ->  A  C_ 
 1o )   &    |-  ( ph  ->  B  e.  ( A 1o )
 )   =>    |-  ( ph  ->  (
 ( (/)  e.  A  /\  B  =  ( (inl  |`  A ) `  (/) ) )  \/  B  =  ( (inr  |`  1o ) `  (/) ) ) )
 
Theoremexmidfodomrlemim 7213* Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
 |-  (EXMID 
 ->  A. x A. y
 ( ( E. z  z  e.  y  /\  y 
 ~<_  x )  ->  E. f  f : x -onto-> y ) )
 
Theoremexmidfodomrlemr 7214* The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
 |-  ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  -> EXMID )
 
TheoremexmidfodomrlemrALT 7215* The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 7214. In particular, this proof uses eldju 7080 instead of djur 7081 and avoids djulclb 7067. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
 |-  ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  -> EXMID )
 
Theoremexmidfodomr 7216* Excluded middle is equivalent to the existence of a mapping from any set onto any inhabited set that it dominates. (Contributed by Jim Kingdon, 1-Jul-2022.)
 |-  (EXMID  <->  A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y ) )
 
2.6.42  Axiom of Choice equivalents
 
Syntaxwac 7217 Formula for an abbreviation of the axiom of choice.
 wff CHOICE
 
Definitiondf-ac 7218* The expression CHOICE will be used as a readable shorthand for any form of the axiom of choice; all concrete forms are long, cryptic, have dummy variables, or all three, making it useful to have a short name. Similar to the Axiom of Choice (first form) of [Enderton] p. 49.

There are some decisions about how to write this definition especially around whether ax-setind 4548 is needed to show equivalence to other ways of stating choice, and about whether choice functions are available for nonempty sets or inhabited sets. (Contributed by Mario Carneiro, 22-Feb-2015.)

 |-  (CHOICE  <->  A. x E. f ( f  C_  x  /\  f  Fn  dom  x )
 )
 
Theoremacfun 7219* A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.)
 |-  ( ph  -> CHOICE )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  A. x  e.  A  E. w  w  e.  x )   =>    |-  ( ph  ->  E. f
 ( f  Fn  A  /\  A. x  e.  A  ( f `  x )  e.  x )
 )
 
Theoremexmidaclem 7220* Lemma for exmidac 7221. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)
 |-  A  =  { x  e.  { (/) ,  { (/) } }  |  ( x  =  (/)  \/  y  =  { (/) } ) }   &    |-  B  =  { x  e.  { (/) ,  { (/) } }  |  ( x  =  { (/)
 }  \/  y  =  { (/) } ) }   &    |-  C  =  { A ,  B }   =>    |-  (CHOICE 
 -> EXMID )
 
Theoremexmidac 7221 The axiom of choice implies excluded middle. See acexmid 5887 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.)
 |-  (CHOICE 
 -> EXMID )
 
2.6.43  Cardinal number arithmetic
 
Theoremendjudisj 7222 Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.)
 |-  ( ( A  e.  V  /\  B  e.  W  /\  ( A  i^i  B )  =  (/) )  ->  ( A B )  ~~  ( A  u.  B ) )
 
Theoremdjuen 7223 Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
 |-  ( ( A  ~~  B  /\  C  ~~  D )  ->  ( A C ) 
 ~~  ( B D ) )
 
Theoremdjuenun 7224 Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.)
 |-  ( ( A  ~~  B  /\  C  ~~  D  /\  ( B  i^i  D )  =  (/) )  ->  ( A C )  ~~  ( B  u.  D ) )
 
Theoremdju1en 7225 Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
 |-  ( ( A  e.  V  /\  -.  A  e.  A )  ->  ( A 1o )  ~~  suc  A )
 
Theoremdju0en 7226 Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
 |-  ( A  e.  V  ->  ( A (/) )  ~~  A )
 
Theoremxp2dju 7227 Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
 |-  ( 2o  X.  A )  =  ( A A )
 
Theoremdjucomen 7228 Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
 |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A B ) 
 ~~  ( B A ) )
 
Theoremdjuassen 7229 Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
 |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X ) 
 ->  ( ( A B ) C )  ~~  ( A ( B C ) ) )
 
Theoremxpdjuen 7230 Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
 |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X ) 
 ->  ( A  X.  ( B C ) )  ~~  ( ( A  X.  B ) ( A  X.  C ) ) )
 
Theoremdjudoml 7231 A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
 |-  ( ( A  e.  V  /\  B  e.  W )  ->  A  ~<_  ( A B ) )
 
Theoremdjudomr 7232 A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
 |-  ( ( A  e.  V  /\  B  e.  W )  ->  B  ~<_  ( A B ) )
 
2.6.44  Ordinal trichotomy
 
Theoremexmidontriimlem1 7233 Lemma for exmidontriim 7237. A variation of r19.30dc 2634. (Contributed by Jim Kingdon, 12-Aug-2024.)
 |-  ( ( A. x  e.  A  ( ph  \/  ps 
 \/  ch )  /\ EXMID )  ->  ( E. x  e.  A  ph  \/  E. x  e.  A  ps  \/  A. x  e.  A  ch ) )
 
Theoremexmidontriimlem2 7234* Lemma for exmidontriim 7237. (Contributed by Jim Kingdon, 12-Aug-2024.)
 |-  ( ph  ->  B  e.  On )   &    |-  ( ph  -> EXMID )   &    |-  ( ph  ->  A. y  e.  B  ( A  e.  y  \/  A  =  y  \/  y  e.  A ) )   =>    |-  ( ph  ->  ( A  e.  B  \/  A. y  e.  B  y  e.  A ) )
 
Theoremexmidontriimlem3 7235* Lemma for exmidontriim 7237. What we get to do based on induction on both  A and  B. (Contributed by Jim Kingdon, 10-Aug-2024.)
 |-  ( ph  ->  A  e.  On )   &    |-  ( ph  ->  B  e.  On )   &    |-  ( ph  -> EXMID
 )   &    |-  ( ph  ->  A. z  e.  A  A. y  e. 
 On  ( z  e.  y  \/  z  =  y  \/  y  e.  z ) )   &    |-  ( ph  ->  A. y  e.  B  ( A  e.  y  \/  A  =  y  \/  y  e.  A ) )   =>    |-  ( ph  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A )
 )
 
Theoremexmidontriimlem4 7236* Lemma for exmidontriim 7237. The induction step for the induction on  A. (Contributed by Jim Kingdon, 10-Aug-2024.)
 |-  ( ph  ->  A  e.  On )   &    |-  ( ph  ->  B  e.  On )   &    |-  ( ph  -> EXMID
 )   &    |-  ( ph  ->  A. z  e.  A  A. y  e. 
 On  ( z  e.  y  \/  z  =  y  \/  y  e.  z ) )   =>    |-  ( ph  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A )
 )
 
Theoremexmidontriim 7237* Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.)
 |-  (EXMID 
 ->  A. x  e.  On  A. y  e.  On  ( x  e.  y  \/  x  =  y  \/  y  e.  x )
 )
 
2.6.45  Excluded middle and the power set of a singleton
 
Theorempw1on 7238 The power set of  1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
 |- 
 ~P 1o  e.  On
 
Theorempw1dom2 7239 The power set of  1o dominates  2o. Also see pwpw0ss 3816 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.)
 |- 
 2o  ~<_  ~P 1o
 
Theorempw1ne0 7240 The power set of  1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
 |- 
 ~P 1o  =/=  (/)
 
Theorempw1ne1 7241 The power set of  1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
 |- 
 ~P 1o  =/=  1o
 
Theorempw1ne3 7242 The power set of  1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |- 
 ~P 1o  =/=  3o
 
Theorempw1nel3 7243 Negated excluded middle implies that the power set of  1o is not an element of  3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |-  ( -. EXMID  ->  -.  ~P 1o  e.  3o )
 
Theoremsucpw1ne3 7244 Negated excluded middle implies that the successor of the power set of  1o is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |-  ( -. EXMID  ->  suc  ~P 1o  =/=  3o )
 
Theoremsucpw1nel3 7245 The successor of the power set of 
1o is not an element of  3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |- 
 -.  suc  ~P 1o  e.  3o
 
Theorem3nelsucpw1 7246 Three is not an element of the successor of the power set of  1o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |- 
 -.  3o  e.  suc  ~P 1o
 
Theoremsucpw1nss3 7247 Negated excluded middle implies that the successor of the power set of  1o is not a subset of  3o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
 |-  ( -. EXMID  ->  -.  suc  ~P 1o  C_ 
 3o )
 
Theorem3nsssucpw1 7248 Negated excluded middle implies that  3o is not a subset of the successor of the power set of 
1o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
 |-  ( -. EXMID  ->  -.  3o  C_  suc  ~P 1o )
 
Theoremonntri35 7249* Double negated ordinal trichotomy.

There are five equivalent statements: (1)  -.  -.  A. x  e.  On A. y  e.  On ( x  e.  y  \/  x  =  y  \/  y  e.  x ), (2)  -.  -.  A. x  e.  On A. y  e.  On ( x  C_  y  \/  y  C_  x ), (3)  A. x  e.  On A. y  e.  On -.  -.  (
x  e.  y  \/  x  =  y  \/  y  e.  x ), (4)  A. x  e.  On A. y  e.  On -.  -.  (
x  C_  y  \/  y  C_  x ), and (5)  -.  -. EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7250), (3) implies (5) (onntri35 7249), (5) implies (1) (onntri51 7252), (2) implies (4) (onntri24 7254), (4) implies (5) (onntri45 7253), and (5) implies (2) (onntri52 7256).

Another way of stating this is that EXMID is equivalent to trichotomy, either the  x  e.  y  \/  x  =  y  \/  y  e.  x or the  x  C_  y  \/  y  C_  x form, as shown in exmidontri 7251 and exmidontri2or 7255, respectively. Thus  -.  -. EXMID is equivalent to (1) or (2). In addition, 
-.  -. EXMID is equivalent to (3) by onntri3or 7257 and (4) by onntri2or 7258.

(Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)

 |-  ( A. x  e. 
 On  A. y  e.  On  -. 
 -.  ( x  e.  y  \/  x  =  y  \/  y  e.  x )  ->  -.  -. EXMID )
 
Theoremonntri13 7250 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( -.  -.  A. x  e.  On  A. y  e.  On  ( x  e.  y  \/  x  =  y  \/  y  e.  x )  ->  A. x  e.  On  A. y  e. 
 On  -.  -.  ( x  e.  y  \/  x  =  y  \/  y  e.  x )
 )
 
Theoremexmidontri 7251* Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
 |-  (EXMID  <->  A. x  e.  On  A. y  e.  On  ( x  e.  y  \/  x  =  y  \/  y  e.  x )
 )
 
Theoremonntri51 7252* Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( -.  -. EXMID  ->  -.  -.  A. x  e.  On  A. y  e.  On  ( x  e.  y  \/  x  =  y  \/  y  e.  x )
 )
 
Theoremonntri45 7253* Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( A. x  e. 
 On  A. y  e.  On  -. 
 -.  ( x  C_  y  \/  y  C_  x )  ->  -.  -. EXMID )
 
Theoremonntri24 7254 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( -.  -.  A. x  e.  On  A. y  e.  On  ( x  C_  y  \/  y  C_  x )  ->  A. x  e.  On  A. y  e.  On  -.  -.  ( x  C_  y  \/  y  C_  x ) )
 
Theoremexmidontri2or 7255* Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
 |-  (EXMID  <->  A. x  e.  On  A. y  e.  On  ( x  C_  y  \/  y  C_  x ) )
 
Theoremonntri52 7256* Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( -.  -. EXMID  ->  -.  -.  A. x  e.  On  A. y  e.  On  ( x  C_  y  \/  y  C_  x ) )
 
Theoremonntri3or 7257* Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
 |-  ( -.  -. EXMID  <->  A. x  e.  On  A. y  e.  On  -.  -.  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) )
 
Theoremonntri2or 7258* Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
 |-  ( -.  -. EXMID  <->  A. x  e.  On  A. y  e.  On  -.  -.  ( x  C_  y  \/  y  C_  x ) )
 
2.6.46  Apartness relations
 
Syntaxwap 7259 Apartness predicate symbol.
 wff  R Ap  A
 
Definitiondf-pap 7260* Apartness predicate. A relation  R is an apartness if it is irreflexive, symmetric, and cotransitive. (Contributed by Jim Kingdon, 14-Feb-2025.)
 |-  ( R Ap  A  <->  ( ( R 
 C_  ( A  X.  A )  /\  A. x  e.  A  -.  x R x )  /\  ( A. x  e.  A  A. y  e.  A  ( x R y  ->  y R x )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R y  ->  ( x R z  \/  y R z ) ) ) ) )
 
Syntaxwtap 7261 Tight apartness predicate symbol.
 wff  R TAp  A
 
Definitiondf-tap 7262* Tight apartness predicate. A relation  R is a tight apartness if it is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim Kingdon, 5-Feb-2025.)
 |-  ( R TAp  A  <->  ( R Ap  A  /\  A. x  e.  A  A. y  e.  A  ( -.  x R y 
 ->  x  =  y
 ) ) )
 
Theoremdftap2 7263* Tight apartness with the apartness properties from df-pap 7260 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.)
 |-  ( R TAp  A  <->  ( R  C_  ( A  X.  A ) 
 /\  ( A. x  e.  A  -.  x R x  /\  A. x  e.  A  A. y  e.  A  ( x R y  ->  y R x ) )  /\  ( A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R y  ->  ( x R z  \/  y R z ) ) 
 /\  A. x  e.  A  A. y  e.  A  ( -.  x R y 
 ->  x  =  y
 ) ) ) )
 
Theoremtapeq1 7264 Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
 |-  ( R  =  S  ->  ( R TAp  A  <->  S TAp  A )
 )
 
Theoremtapeq2 7265 Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.)
 |-  ( A  =  B  ->  ( R TAp  A  <->  R TAp  B )
 )
 
Theoremnetap 7266* Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.)
 |-  ( A. x  e.  A  A. y  e.  A DECID  x  =  y  ->  { <. u ,  v >.  |  ( ( u  e.  A  /\  v  e.  A )  /\  u  =/=  v ) } TAp  A )
 
Theorem2onetap 7267* Negated equality is a tight apartness on  2o. (Contributed by Jim Kingdon, 6-Feb-2025.)
 |- 
 { <. u ,  v >.  |  ( ( u  e.  2o  /\  v  e.  2o )  /\  u  =/=  v ) } TAp  2o
 
Theorem2oneel 7268*  (/) and  1o are two unequal elements of  2o. (Contributed by Jim Kingdon, 8-Feb-2025.)
 |- 
 <. (/) ,  1o >.  e. 
 { <. u ,  v >.  |  ( ( u  e.  2o  /\  v  e.  2o )  /\  u  =/=  v ) }
 
Theorem2omotaplemap 7269* Lemma for 2omotap 7271. (Contributed by Jim Kingdon, 6-Feb-2025.)
 |-  ( -.  -.  ph  ->  { <. u ,  v >.  |  ( ( u  e.  2o  /\  v  e.  2o )  /\  ( ph  /\  u  =/=  v
 ) ) } TAp  2o )
 
Theorem2omotaplemst 7270* Lemma for 2omotap 7271. (Contributed by Jim Kingdon, 6-Feb-2025.)
 |-  ( ( E* r  r TAp  2o  /\  -.  -.  ph )  ->  ph )
 
Theorem2omotap 7271 If there is at most one tight apartness on  2o, excluded middle follows. Based on online discussions by Tom de Jong, Andrew W Swan, and Martin Escardo. (Contributed by Jim Kingdon, 6-Feb-2025.)
 |-  ( E* r  r TAp 
 2o  -> EXMID
 )
 
Theoremexmidapne 7272* Excluded middle implies there is only one tight apartness on any class, namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.)
 |-  (EXMID 
 ->  ( R TAp  A  <->  R  =  { <. u ,  v >.  |  ( ( u  e.  A  /\  v  e.  A )  /\  u  =/=  v ) } )
 )
 
Theoremexmidmotap 7273* The proposition that every class has at most one tight apartness is equivalent to excluded middle. (Contributed by Jim Kingdon, 14-Feb-2025.)
 |-  (EXMID  <->  A. x E* r  r TAp 
 x )
 
PART 3  CHOICE PRINCIPLES

We have already introduced the full Axiom of Choice df-ac 7218 but since it implies excluded middle as shown at exmidac 7221, it is not especially relevant to us. In this section we define countable choice and dependent choice, which are not as strong as thus often considered in mathematics which seeks to avoid full excluded middle.

 
3.1  Countable Choice and Dependent Choice
 
3.1.1  Introduce Countable Choice
 
Syntaxwacc 7274 Formula for an abbreviation of countable choice.
 wff CCHOICE
 
Definitiondf-cc 7275* The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7218 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.)
 |-  (CCHOICE  <->  A. x ( dom  x  ~~ 
 om  ->  E. f ( f 
 C_  x  /\  f  Fn  dom  x ) ) )
 
Theoremccfunen 7276* Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  A 
 ~~  om )   &    |-  ( ph  ->  A. x  e.  A  E. w  w  e.  x )   =>    |-  ( ph  ->  E. f
 ( f  Fn  A  /\  A. x  e.  A  ( f `  x )  e.  x )
 )
 
Theoremcc1 7277* Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
 |-  (CCHOICE 
 ->  A. x ( ( x  ~~  om  /\  A. z  e.  x  E. w  w  e.  z
 )  ->  E. f A. z  e.  x  ( f `  z
 )  e.  z ) )
 
Theoremcc2lem 7278* Lemma for cc2 7279. (Contributed by Jim Kingdon, 27-Apr-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  F  Fn  om )   &    |-  ( ph  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )   &    |-  A  =  ( n  e.  om  |->  ( { n }  X.  ( F `  n ) ) )   &    |-  G  =  ( n  e.  om  |->  ( 2nd `  (
 f `  ( A `  n ) ) ) )   =>    |-  ( ph  ->  E. g
 ( g  Fn  om  /\ 
 A. n  e.  om  ( g `  n )  e.  ( F `  n ) ) )
 
Theoremcc2 7279* Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  F  Fn  om )   &    |-  ( ph  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )   =>    |-  ( ph  ->  E. g
 ( g  Fn  om  /\ 
 A. n  e.  om  ( g `  n )  e.  ( F `  n ) ) )
 
Theoremcc3 7280* Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  A. n  e.  N  F  e.  _V )   &    |-  ( ph  ->  A. n  e.  N  E. w  w  e.  F )   &    |-  ( ph  ->  N  ~~ 
 om )   =>    |-  ( ph  ->  E. f
 ( f  Fn  N  /\  A. n  e.  N  ( f `  n )  e.  F )
 )
 
Theoremcc4f 7281* Countable choice by showing the existence of a function  f which can choose a value at each index 
n such that  ch holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  A  e.  V )   &    |-  F/_ n A   &    |-  ( ph  ->  N  ~~ 
 om )   &    |-  ( x  =  ( f `  n )  ->  ( ps  <->  ch ) )   &    |-  ( ph  ->  A. n  e.  N  E. x  e.  A  ps )   =>    |-  ( ph  ->  E. f
 ( f : N --> A  /\  A. n  e.  N  ch ) )
 
Theoremcc4 7282* Countable choice by showing the existence of a function  f which can choose a value at each index 
n such that  ch holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 1-May-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  N  ~~  om )   &    |-  ( x  =  ( f `  n ) 
 ->  ( ps  <->  ch ) )   &    |-  ( ph  ->  A. n  e.  N  E. x  e.  A  ps )   =>    |-  ( ph  ->  E. f
 ( f : N --> A  /\  A. n  e.  N  ch ) )
 
Theoremcc4n 7283* Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7282, the hypotheses only require an A(n) for each value of  n, not a single set  A which suffices for every 
n  e.  om. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  A. n  e.  N  { x  e.  A  |  ps }  e.  V )   &    |-  ( ph  ->  N  ~~  om )   &    |-  ( x  =  ( f `  n ) 
 ->  ( ps  <->  ch ) )   &    |-  ( ph  ->  A. n  e.  N  E. x  e.  A  ps )   =>    |-  ( ph  ->  E. f
 ( f  Fn  N  /\  A. n  e.  N  ch ) )
 
PART 4  REAL AND COMPLEX NUMBERS

This section derives the basics of real and complex numbers.

To construct the real numbers constructively, we follow two main sources. The first is Metamath Proof Explorer, which has the advantage of being already formalized in metamath. Its disadvantage, for our purposes, is that it assumes the law of the excluded middle throughout. Since we have already developed natural numbers ( for example, nna0 6488 and similar theorems ), going from there to positive integers (df-ni 7316) and then positive rational numbers (df-nqqs 7360) does not involve a major change in approach compared with the Metamath Proof Explorer.

It is when we proceed to Dedekind cuts that we bring in more material from Section 11.2 of [HoTT], which focuses on the aspects of Dedekind cuts which are different without excluded middle or choice principles. With excluded middle, it is natural to define a cut as the lower set only (as Metamath Proof Explorer does), but here we define the cut as a pair of both the lower and upper sets, as [HoTT] does. There are also differences in how we handle order and replacing "not equal to zero" with "apart from zero".

When working constructively, there are several possible definitions of real numbers. Here we adopt the most common definition, as two-sided Dedekind cuts with the properties described at df-inp 7478. The Cauchy reals (without countable choice) fail to satisfy ax-caucvg 7944 and the MacNeille reals fail to satisfy axltwlin 8038, and we do not develop them here. For more on differing definitions of the reals, see the introduction to Chapter 11 in [HoTT] or Section 1.2 of [BauerHanson].

 
4.1  Construction and axiomatization of real and complex numbers
 
4.1.1  Dedekind-cut construction of real and complex numbers
 
Syntaxcnpi 7284 The set of positive integers, which is the set of natural numbers  om with 0 removed.

Note: This is the start of the Dedekind-cut construction of real and complex numbers.

 class  N.
 
Syntaxcpli 7285 Positive integer addition.
 class  +N
 
Syntaxcmi 7286 Positive integer multiplication.
 class  .N
 
Syntaxclti 7287 Positive integer ordering relation.
 class  <N
 
Syntaxcplpq 7288 Positive pre-fraction addition.
 class  +pQ
 
Syntaxcmpq 7289 Positive pre-fraction multiplication.
 class  .pQ
 
Syntaxcltpq 7290 Positive pre-fraction ordering relation.
 class  <pQ
 
Syntaxceq 7291 Equivalence class used to construct positive fractions.
 class  ~Q
 
Syntaxcnq 7292 Set of positive fractions.
 class  Q.
 
Syntaxc1q 7293 The positive fraction constant 1.
 class  1Q
 
Syntaxcplq 7294 Positive fraction addition.
 class  +Q
 
Syntaxcmq 7295 Positive fraction multiplication.
 class  .Q
 
Syntaxcrq 7296 Positive fraction reciprocal operation.
 class  *Q
 
Syntaxcltq 7297 Positive fraction ordering relation.
 class  <Q
 
Syntaxceq0 7298 Equivalence class used to construct nonnegative fractions.
 class ~Q0
 
Syntaxcnq0 7299 Set of nonnegative fractions.
 class Q0
 
Syntaxc0q0 7300 The nonnegative fraction constant 0.
 class 0Q0
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15104
  Copyright terms: Public domain < Previous  Next >