Home | Metamath
Proof ExplorerTheorem List
(p. 295 of 329)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-22423) |
Hilbert Space Explorer
(22424-23946) |
Users' Mathboxes
(23947-32824) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | bnj1034 29401* | Technical lemma for bnj69 29441. 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 | bnj1039 29402 | Technical lemma for bnj69 29441. 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 | bnj1040 29403* | Technical lemma for bnj69 29441. 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 | bnj1047 29404 | |

Theorem | bnj1049 29405 | |

Theorem | bnj1052 29406* | |

Theorem | bnj1053 29407* | |

Theorem | bnj1071 29408 | |

Theorem | bnj1083 29409 | |

Theorem | bnj1090 29410* | |

Theorem | bnj1093 29411* | |

Theorem | bnj1097 29412 | |

Theorem | bnj1110 29413* | |

Theorem | bnj1112 29414* | |

Theorem | bnj1118 29415* | |

Theorem | bnj1121 29416 | |

Theorem | bnj1123 29417* | |

Theorem | bnj1030 29418* | |

Theorem | bnj1124 29419 | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1133 29420* | |

Theorem | bnj1128 29421* | |

Theorem | bnj1127 29422 | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1125 29423 | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1145 29424* | |

Theorem | bnj1147 29425 | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1137 29426* | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |

Theorem | bnj1148 29427 | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1136 29428* | |

Theorem | bnj1152 29429 | |

Theorem | bnj1154 29430* | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1171 29431 | |

Theorem | bnj1172 29432 | |

Theorem | bnj1173 29433 | |

Theorem | bnj1174 29434 | |

Theorem | bnj1175 29435 | |

Theorem | bnj1176 29436* | |

Theorem | bnj1177 29437 | |

Theorem | bnj1186 29438* | |

Theorem | bnj1190 29439* | |

Theorem | bnj1189 29440* | |

19.25.3 The existence of a minimal element in
certain classes | ||

Theorem | bnj69 29441* | Existence of a minimal element in certain classes: if is well-founded and set-like on , then every non-empty 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 29442* | Existence of a minimal element in certain classes: if is well-founded and set-like on , then every non-empty 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.) |

19.25.4 Well-founded induction | ||

Theorem | bnj1204 29443* | 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.) |

Theorem | bnj1234 29444* | Technical lemma for bnj60 29493. 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 29445* | Technical lemma for bnj60 29493. 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 29446* | Technical lemma for bnj60 29493. 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 29447* | |

Theorem | bnj1253 29448* | |

Theorem | bnj1279 29449* | |

Theorem | bnj1286 29450* | |

Theorem | bnj1280 29451* | |

Theorem | bnj1296 29452* | |

Theorem | bnj1309 29453* | |

Theorem | bnj1307 29454* | |

Theorem | bnj1311 29455* | |

Theorem | bnj1318 29456 | |

Theorem | bnj1326 29457* | |

Theorem | bnj1321 29458* | |

Theorem | bnj1364 29459 | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1371 29460* | |

Theorem | bnj1373 29461* | |

Theorem | bnj1374 29462* | |

Theorem | bnj1384 29463* | |

Theorem | bnj1388 29464* | |

Theorem | bnj1398 29465* | |

Theorem | bnj1413 29466* | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1408 29467* | Technical lemma for bnj1414 29468. 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 29468* | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1415 29469* | |

Theorem | bnj1416 29470 | |

Theorem | bnj1418 29471 | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1417 29472* | Technical lemma for bnj60 29493. 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 29473* | |

Theorem | bnj1444 29474* | |

Theorem | bnj1445 29475* | |

Theorem | bnj1446 29476* | |

Theorem | bnj1447 29477* | |

Theorem | bnj1448 29478* | |

Theorem | bnj1449 29479* | |

Theorem | bnj1442 29480* | |

Theorem | bnj1450 29481* | |

Theorem | bnj1423 29482* | |

Theorem | bnj1452 29483* | |

Theorem | bnj1466 29484* | |

Theorem | bnj1467 29485* | |

Theorem | bnj1463 29486* | |

Theorem | bnj1489 29487* | |

Theorem | bnj1491 29488* | |

Theorem | bnj1312 29489* | |

Theorem | bnj1493 29490* | |

Theorem | bnj1497 29491* | |

Theorem | bnj1498 29492* | |

19.25.5 Well-founded recursion, part 1 of
3 | ||

Theorem | bnj60 29493* | 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 29494* | Technical lemma for bnj1500 29499. 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 29495* | Technical lemma for bnj1500 29499. 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 29496* | Technical lemma for bnj1500 29499. 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 29497* | |

Theorem | bnj1501 29498* | |

19.25.6 Well-founded recursion, part 2 of
3 | ||

Theorem | bnj1500 29499* | 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 29500* | Technical lemma for bnj1522 29503. 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.) |

< Previous Next > |