Home | Metamath
Proof ExplorerTheorem List
(p. 293 of 327)
| < 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-22409) |
Hilbert Space Explorer
(22410-23932) |
Users' Mathboxes
(23933-32601) |

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

Statement | ||

Theorem | bnj1083 29201 | Technical lemma for bnj69 29233. 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 | bnj1090 29202* | Technical lemma for bnj69 29233. 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 | bnj1093 29203* | Technical lemma for bnj69 29233. 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 | bnj1097 29204 | |

Theorem | bnj1110 29205* | |

Theorem | bnj1112 29206* | |

Theorem | bnj1118 29207* | |

Theorem | bnj1121 29208 | |

Theorem | bnj1123 29209* | |

Theorem | bnj1030 29210* | |

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

Theorem | bnj1133 29212* | |

Theorem | bnj1128 29213* | |

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

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

Theorem | bnj1145 29216* | |

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

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

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

Theorem | bnj1136 29220* | |

Theorem | bnj1152 29221 | |

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

Theorem | bnj1171 29223 | |

Theorem | bnj1172 29224 | |

Theorem | bnj1173 29225 | |

Theorem | bnj1174 29226 | |

Theorem | bnj1175 29227 | |

Theorem | bnj1176 29228* | |

Theorem | bnj1177 29229 | |

Theorem | bnj1186 29230* | |

Theorem | bnj1190 29231* | |

Theorem | bnj1189 29232* | |

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

Theorem | bnj69 29233* | 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 29234* | 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 29235* | 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 29236* | Technical lemma for bnj60 29285. 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 29237* | Technical lemma for bnj60 29285. 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 29238* | Technical lemma for bnj60 29285. 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 29239* | |

Theorem | bnj1253 29240* | |

Theorem | bnj1279 29241* | |

Theorem | bnj1286 29242* | |

Theorem | bnj1280 29243* | |

Theorem | bnj1296 29244* | |

Theorem | bnj1309 29245* | |

Theorem | bnj1307 29246* | |

Theorem | bnj1311 29247* | |

Theorem | bnj1318 29248 | |

Theorem | bnj1326 29249* | |

Theorem | bnj1321 29250* | |

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

Theorem | bnj1371 29252* | |

Theorem | bnj1373 29253* | |

Theorem | bnj1374 29254* | |

Theorem | bnj1384 29255* | |

Theorem | bnj1388 29256* | |

Theorem | bnj1398 29257* | |

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

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

Theorem | bnj1415 29261* | |

Theorem | bnj1416 29262 | |

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

Theorem | bnj1417 29264* | Technical lemma for bnj60 29285. 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 29265* | |

Theorem | bnj1444 29266* | |

Theorem | bnj1445 29267* | |

Theorem | bnj1446 29268* | |

Theorem | bnj1447 29269* | |

Theorem | bnj1448 29270* | |

Theorem | bnj1449 29271* | |

Theorem | bnj1442 29272* | |

Theorem | bnj1450 29273* | |

Theorem | bnj1423 29274* | |

Theorem | bnj1452 29275* | |

Theorem | bnj1466 29276* | |

Theorem | bnj1467 29277* | |

Theorem | bnj1463 29278* | |

Theorem | bnj1489 29279* | |

Theorem | bnj1491 29280* | |

Theorem | bnj1312 29281* | |

Theorem | bnj1493 29282* | |

Theorem | bnj1497 29283* | |

Theorem | bnj1498 29284* | |

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

Theorem | bnj60 29285* | 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 29286* | Technical lemma for bnj1500 29291. 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 29287* | Technical lemma for bnj1500 29291. 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 29288* | Technical lemma for bnj1500 29291. 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 29289* | |

Theorem | bnj1501 29290* | |

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

Theorem | bnj1500 29291* | 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 29292* | Technical lemma for bnj1522 29295. 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 29293* | Technical lemma for bnj1522 29295. 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 29294* | Technical lemma for bnj1522 29295. 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.) |

19.25.7 Well-founded recursion, part 3 of
3 | ||

Theorem | bnj1522 29295* | 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.) |

19.26 Mathbox for Norm
MegillNote: A label suffixed with "N" (after the "Atoms..." section below), such as lshpnel2N 29622, means that the definition or theorem is not used for the derivation of hlathil 32601. This is a temporary renaming to assist cleaning up the theorems needed by hlathil 32601. Please inform me of any changes that might affect my mathbox, since I may be working on it independently of the github commits. - Norm 30-Nov-2015 | ||

19.26.1 Experiments to study ax-7
unbundlingThis section reproduces all predicate calculus theorems through sbal2 2210 that depend on ax-7 1749. It is an experiment to see how much of predicate calculus can be derived using the weaker (unbundled) ax-7v 29296. The theorems in this section with suffix "NEW7" are direct replacements for the existing ones without the suffix but have proofs that avoid ax-7 1749 in favor of ax-7v 29296. Theorems with suffix "AUX7" are new theorems that do not appear in the main predicate calculus section but assist the proofs of the "NEW7" suffixed theorems. They also use at most ax-7v 29296 and not ax-7 1749. Theorems with suffix "OLD7" are the remaining predicate calculus theorems (through sbal2 2210) that haven't been proved from ax-7v 29296. In order to isolate them, they are derived from ax-7OLD7 29517 which replicates ax-7 1749. Whenever a proof of a *OLD7 theorem is found from ax-7v 29296, the suffix is changed to "NEW7" and the theorem is moved up to the "NEW7" section. Theorems with suffix "AUXOLD7" (currently just nfsb4tw2AUXOLD7 29585) are results of an unsuccessful attempt to prove a helper theorem from ax-7v 29296, but still needs the help of ax-7 1749. Currently there are about 138 "NEW7" theorems (starting after ax-7v 29296) and 90 "OLD7" theorems (starting after ax-7OLD7 29517). | ||

19.26.1.1 Theorems derived from ax-7v (suffixes
NEW7 and AUX7) | ||

Axiom | ax-7v 29296* | Experiment to see if ax-7 1749 can be unbundled i.e. can be derived from ax-7v 29296. This axiom is temporary. It will be replaced with a theorem derived from ax-7 1749 if we are successful, otherwise will be deleted. (Contributed by NM, 9-Oct-2017.) |

Theorem | ax7vAUX7 29297* |
A weaker version of ax-7 1749 with distinct variable restrictions. In
order to show that this weakening is adequate, this should be the only
theorem referencing ax-7 1749 directly.
(Right now we derive this from the temporary axiom ax-7v 29296 for easier 'show trace'. If this project is successful, which is seeming more and more unlikely, we will derive this from ax-7 1749 just as we derive ax9v 1667 from ax-9 1666.) (Contributed by NM, 9-Oct-2017.) |

Theorem | alcomwAUX7 29298* | Weak version of alcom 1752 not requiring ax-7 1749. (Contributed by NM, 27-Oct-2017.) |

Theorem | a7swAUX7 29299* | Weak version of a7s 1750 not requiring ax-7 1749. (Contributed by NM, 28-Oct-2017.) |

Theorem | cbv3hvNEW7 29300* | Lemma for ax10NEW7 29327. Similar to cbv3h 1972. Requires distinct variables but avoids ax-12 1950. (Contributed by NM, 25-Jul-2015.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29296 instead of ax-7 1749. |

< Previous Next > |