HomeTheorem List (p. 331 of 368)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 331 of 368) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-25497) |
Hilbert Space Explorer
(25498-27022) |
Users' Mathboxes
(27023-36798) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bnj1127 33001 |
Property of  .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
   
      | ||
| Theorem | bnj1125 33002 |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
 ![/\](wedge.gif "/\"){kind=small}
| ||
| Theorem | bnj1145 33003* | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
      
      
   ![\](setminus.gif "\"){kind=small}     
 
 
 | ||
| Theorem | bnj1147 33004 |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
|
| ||
| Theorem | bnj1137 33005* |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.)
(New usage is discouraged.)
|
| ||
| Theorem | bnj1148 33006 |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
 | ||
| Theorem | bnj1136 33007* | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1152 33008 | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1154 33009* |
Property of  .
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(New usage is discouraged.)
|
  | ||
| Theorem | bnj1171 33010 | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 
| ||
| Theorem | bnj1172 33011 | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1173 33012 | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1174 33013 | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1175 33014 | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1176 33015* | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1177 33016 | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1186 33017* | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1190 33018* | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1189 33019* | Technical lemma for bnj69 33020. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj69 33020* |
Existence of a minimal element in certain classes: if is
well-founded and set-like on , then every nonempty subclass of
has a minimal
element. The proof has been taken from Chapter 4 of
Don Monk's notes on Set Theory. See
http://euclid.colorado.edu/~monkd/setth.pdf.
(Contributed by
Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|
| | ||
| Theorem | bnj1228 33021* |
Existence of a minimal element in certain classes: if is
well-founded and set-like on , then every nonempty subclass of
has a minimal
element. The proof has been taken from Chapter 4 of
Don Monk's notes on Set Theory. See
http://euclid.colorado.edu/~monkd/setth.pdf.
(Contributed by
Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|
|
| ||
| Theorem | bnj1204 33022* | Well-founded induction. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
  ![].](_drbrack.gif "]."){kind=small}
| ||
| Theorem | bnj1234 33023* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 
 
  
| ||
| Theorem | bnj1245 33024* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
  
| ||
| Theorem | bnj1256 33025* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1259 33026* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1253 33027* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1279 33028* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1286 33029* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1280 33030* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1296 33031* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1309 33032* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1307 33033* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1311 33034* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1318 33035 | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1326 33036* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1321 33037* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 | ||
| Theorem | bnj1364 33038 |
Property of .
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(New usage is discouraged.)
|
 | ||
| Theorem | bnj1371 33039* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 
   | ||
| Theorem | bnj1373 33040* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1374 33041* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1384 33042* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1388 33043* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1398 33044* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1413 33045* |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
|
| ||
| Theorem | bnj1408 33046* | Technical lemma for bnj1414 33047. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1414 33047* |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
|
| ||
| Theorem | bnj1415 33048* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1416 33049 | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1418 33050 |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
|
| ||
| Theorem | bnj1417 33051* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1421 33052* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1444 33053* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1445 33054* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1446 33055* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1447 33056* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1448 33057* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1449 33058* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1442 33059* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1450 33060* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1423 33061* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1452 33062* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1466 33063* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1467 33064* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1463 33065* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1489 33066* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1491 33067* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1312 33068* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1493 33069* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1497 33070* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1498 33071* | Technical lemma for bnj60 33072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 | ||
| Theorem | bnj60 33072* | Well-founded recursion, part 1 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1514 33073* | Technical lemma for bnj1500 33078. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1518 33074* | Technical lemma for bnj1500 33078. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1519 33075* | Technical lemma for bnj1500 33078. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1520 33076* | Technical lemma for bnj1500 33078. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1501 33077* | Technical lemma for bnj1500 33078. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1500 33078* | Well-founded recursion, part 2 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1525 33079* | Technical lemma for bnj1522 33082. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1529 33080* | Technical lemma for bnj1522 33082. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1523 33081* | Technical lemma for bnj1522 33082. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1522 33082* | Well-founded recursion, part 3 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
In this mathbox, we try to respect the ordering of the sections of the main part. There are strengthenings of theorems of the main part, as well as work on reducing axiom dependencies. | ||
Miscellaneous utility theorems of propositional calculus. | ||
In this section, we prove a few rules of inference derived from modus ponens, and which do not depend on any axioms. | ||
| Theorem | bj-mp2c 33083 | A double modus ponens inference. (Contributed by BJ, 24-Sep-2019.) |
|
| ||
| Theorem | bj-mp2d 33084 | A double modus ponens inference. (Contributed by BJ, 24-Sep-2019.) |
| | ||
In this section, we prove a syntactic theorem (bj-0 33085) asserting that some formula is indeed a formula. Then, we use this syntactic theorem to shorten the proof of a "usual" theorem (bj-1 33086) and explain in the comment of that theorem why this phenomenon is unusual. | ||
| Theorem | bj-0 33085 | A syntactic theorem. See the comment of bj-1 33086. The only other syntactic theorems in the main part of set.mm are wel 1763 and weq 1700. (Contributed by BJ, 24-Sep-2019.) (New usage is discouraged.) |
| ||
| Theorem | bj-1 33086 |
In this proof, the use of the syntactic theorem bj-0 33085
allows to reduce
the length of the proof by one (non-essential) step. Since bj-0 33085
is used
in a non-essential step, this use does not appear in the html page (but
the present theorem appears on the html page of bj-0 33085
as a theorem using
it.
Suppose that the syntactic theorem thm0 proves that PHI is a formula, and that thm0 is used to shorten the proof of thm1. Assume that PHI does have proper non-atomic subformulas of type wff (which is not the case of the formula proved by weq 1700 or wel 1763). Then, the proof of thm1 does not construct all the proper non-atomic subformulas of PHI (if it did, then using thm0 would not shorten it). Therefore, thm1 is a special instance of a more general theorem with essentially the same proof. This explains why syntactic theorems are not useful in set.mm. In the present case, bj-1 33086 is a special instance of id 22. (Contributed by BJ, 24-Sep-2019.) (New usage is discouraged.) |
|
| ||
The three theorems sylbbr 33087, sylbb1 33088 and sylbb2 33089 could be placed, together with sylbb 197, after the theorems sylibr 212 and sylbir 213. Together with them and the theorems sylib 196 and sylbi 195, they are the 8 possible inferences inferring an implication from an implication and a biconditional (4) or from two biconditionals (4). The 4 inferences proving a biconditional from two biconditionals are bitri 249, bitr2i 250, bitr3i 251 and bitr4i 252, while the inference proving an implication from two implications is syl 16 (for consistency, it could be labelled "imtri" but "syl" is classical). There are also closed forms and deduction versions of these, like, among many others, syld 44, syl5 32, syl6 33, mpbid 210, bitrd 253, syl5bb 257, syl6bb 261 and variants. Additionally, the three newly added theorems help shorten 17 existing proofs by a total of around 250 bytes. | ||
| Theorem | sylbbr 33087 | A mixed syllogism inference from two biconditionals. (Minimizes bitri 249.) (Contributed by BJ, 21-Apr-2019.) |
| | ||
| Theorem | sylbb1 33088 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
| | ||
| Theorem | sylbb2 33089 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
| | ||
A few lemmas about disjunction. The fundamental theorems in this family are the dual statements pm4.71 630 and pm4.72 872. See also biort 892 and biorf 405. | ||
| Theorem | bj-jaoi1 33090 | Shortens 11 proofs by a total of around 60 bytes. (Contributed by BJ, 30-Sep-2019.) |
| ||
| Theorem | bj-jaoi2 33091 | Shortens 9 proofs by a total of around 50 bytes. (Contributed by BJ, 30-Sep-2019.) |
|
| ||
| Theorem | bj-animorl 33092 | Conjunction implies disjunction with one common formula (1/4). (Contributed by BJ, 4-Oct-2019.) |
|
| ||
| Theorem | bj-animorr 33093 | Conjunction implies disjunction with one common formula (2/4). (Contributed by BJ, 4-Oct-2019.) |
|
| ||
| Theorem | bj-animorlr 33094 | Conjunction implies disjunction with one common formula (3/4). (Contributed by BJ, 4-Oct-2019.) |
|
| ||
| Theorem | bj-animorrl 33095 | Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.) |
|
| ||
A few other characterizations of the bicondional. The inter-definability of logical connectives offers many ways to express a given statement. Some useful theorems in this regard are df-or 370, df-an 371, pm4.64 372, imor 412, pm4.62 419 through pm4.67 428, and, for the De Morgan laws, ianor 488 through pm4.57 497. | ||
| Theorem | bj-dfbi4 33096 | Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.) |
|
| ||
| Theorem | bj-dfbi5 33097 | Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.) |
|
| ||
| Theorem | bj-dfbi6 33098 | Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.) |
|
| ||
This section introduces the conditional operator for propositions, denoted by
if-. It is the analogue for propositions of | ||
| Syntax | wif 33099 | Extend class notation to include the conditional operator for propositions. |
| if- | ||
| Definition | df-bj-if 33100 | Definition of the conditional operator for propositions. See bj-dfif2 33101, bj-dfif3 33102, bj-dfif4 33103, bj-dfif5 33104, bj-dfif6 33106 and bj-dfif7 33107 for alternate definitions. (Contributed by BJ, 22-Jun-2019.) |
| if-
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |
(see