HomeTheorem List (p. 352 of 500)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 352 of 500) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30900) |
Hilbert Space Explorer
(30901-32423) |
Users' Mathboxes
(32424-49930) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bnj1500 35101* | 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.) |
| ⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} & ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩ & ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ 𝐹 = ∪ 𝐶 ⇒ ⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) | ||
| Theorem | bnj1525 35102* | Technical lemma for bnj1522 35105. 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.) |
| ⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} & ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩ & ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ 𝐹 = ∪ 𝐶 & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘⟨𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))⟩))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝐹 ≠ 𝐻)) ⇒ ⊢ (𝜓 → ∀𝑥𝜓) | ||
| Theorem | bnj1529 35103* | Technical lemma for bnj1522 35105. 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.) |
| ⊢ (𝜒 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) & ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹) ⇒ ⊢ (𝜒 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝐺‘⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩)) | ||
| Theorem | bnj1523 35104* | Technical lemma for bnj1522 35105. 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.) |
| ⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} & ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩ & ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ 𝐹 = ∪ 𝐶 & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘⟨𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))⟩))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝐹 ≠ 𝐻)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ (𝐻‘𝑥))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐻‘𝑥)} & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑦 ∈ 𝐷 ∧ ∀𝑧 ∈ 𝐷 ¬ 𝑧𝑅𝑦)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘⟨𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) → 𝐹 = 𝐻) | ||
| Theorem | bnj1522 35105* | 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.) |
| ⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} & ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩ & ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ 𝐹 = ∪ 𝐶 ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘⟨𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) → 𝐹 = 𝐻) | ||
| Theorem | nfan1c 35106 | Variant of nfan 1900 and commuted form of nfan1 2205. (Contributed by BTernaryTau, 31-Jul-2025.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ Ⅎ𝑥(𝜓 ∧ 𝜑) | ||
| Theorem | cbvex1v 35107* | Rule used to change bound variables, using implicit substitution. (Contributed by BTernaryTau, 31-Jul-2025.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑦𝜒)) | ||
| Theorem | dvelimalcased 35108* | Eliminate a disjoint variable condition from a universally quantified statement using cases. (Contributed by BTernaryTau, 31-Jul-2025.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜃) & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑥 → (𝜓 → 𝜃))) & ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (𝜒 → 𝜃)) & ⊢ (𝜑 → ∀𝑧𝜓) & ⊢ (𝜑 → ∀𝑥𝜒) ⇒ ⊢ (𝜑 → ∀𝑥𝜃) | ||
| Theorem | dvelimalcasei 35109* | Eliminate a disjoint variable condition from a universally quantified statement using cases. Inference form of dvelimalcased 35108. (Contributed by BTernaryTau, 31-Jul-2025.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜒) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑥 → (𝜑 → 𝜒))) & ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜓 → 𝜒)) & ⊢ ∀𝑧𝜑 & ⊢ ∀𝑥𝜓 ⇒ ⊢ ∀𝑥𝜒 | ||
| Theorem | dvelimexcased 35110* | Eliminate a disjoint variable condition from an existentially quantified statement using cases. (Contributed by BTernaryTau, 31-Jul-2025.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜃) & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑥 → (𝜓 → 𝜃))) & ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (𝜒 → 𝜃)) & ⊢ (𝜑 → ∃𝑧𝜓) & ⊢ (𝜑 → ∃𝑥𝜒) ⇒ ⊢ (𝜑 → ∃𝑥𝜃) | ||
| Theorem | dvelimexcasei 35111* | Eliminate a disjoint variable condition from an existentially quantified statement using cases. Inference form of dvelimexcased 35110. See axnulg 35140 for an example of its use. (Contributed by BTernaryTau, 31-Jul-2025.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜒) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑥 → (𝜑 → 𝜒))) & ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜓 → 𝜒)) & ⊢ ∃𝑧𝜑 & ⊢ ∃𝑥𝜓 ⇒ ⊢ ∃𝑥𝜒 | ||
| Theorem | exdifsn 35112 | There exists an element in a class excluding a singleton if and only if there exists an element in the original class not equal to the singleton element. (Contributed by BTernaryTau, 15-Sep-2023.) |
| ⊢ (∃𝑥 𝑥 ∈ (𝐴 ∖ {𝐵}) ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 𝐵) | ||
| Theorem | srcmpltd 35113 | If a statement is true for every element of a class and for every element of its complement relative to a second class, then it is true for every element in the second class. (Contributed by BTernaryTau, 27-Sep-2023.) |
| ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝜓)) & ⊢ (𝜑 → (𝐶 ∈ (𝐵 ∖ 𝐴) → 𝜓)) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → 𝜓)) | ||
| Theorem | prsrcmpltd 35114 | If a statement is true for all pairs of elements of a class, all pairs of elements of its complement relative to a second class, and all pairs with one element in each, then it is true for all pairs of elements of the second class. (Contributed by BTernaryTau, 27-Sep-2023.) |
| ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → 𝜓)) & ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ (𝐵 ∖ 𝐴)) → 𝜓)) & ⊢ (𝜑 → ((𝐶 ∈ (𝐵 ∖ 𝐴) ∧ 𝐷 ∈ 𝐴) → 𝜓)) & ⊢ (𝜑 → ((𝐶 ∈ (𝐵 ∖ 𝐴) ∧ 𝐷 ∈ (𝐵 ∖ 𝐴)) → 𝜓)) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → 𝜓)) | ||
| Theorem | axsepg2 35115* | A generalization of ax-sep 5236 in which 𝑦 and 𝑧 need not be distinct. See also axsepg 5237 which instead allows 𝑧 to occur in 𝜑. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.) |
| ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) | ||
| Theorem | axsepg2ALT 35116* | Alternate proof of axsepg2 35115, derived directly from ax-sep 5236 with no additional set theory axioms. (Contributed by BTernaryTau, 3-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) | ||
| Theorem | dff15 35117* | A one-to-one function in terms of different arguments never having the same function value. (Contributed by BTernaryTau, 24-Oct-2023.) |
| ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦))) | ||
| Theorem | f1resveqaeq 35118 | If a function restricted to a class is one-to-one, then for any two elements of the class, the values of the function at those elements are equal only if the two elements are the same element. (Contributed by BTernaryTau, 27-Sep-2023.) |
| ⊢ (((𝐹 ↾ 𝐴):𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷)) | ||
| Theorem | f1resrcmplf1dlem 35119 | Lemma for f1resrcmplf1d 35120. (Contributed by BTernaryTau, 27-Sep-2023.) |
| ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ((𝐹 “ 𝐶) ∩ (𝐹 “ 𝐷)) = ∅) ⇒ ⊢ (𝜑 → ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐷) → ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑋 = 𝑌))) | ||
| Theorem | f1resrcmplf1d 35120 | If a function's restriction to a subclass of its domain and its restriction to the relative complement of that subclass are both one-to-one, and if the ranges of those two restrictions are disjoint, then the function is itself one-to-one. (Contributed by BTernaryTau, 28-Sep-2023.) |
| ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵) & ⊢ (𝜑 → (𝐹 ↾ (𝐴 ∖ 𝐶)):(𝐴 ∖ 𝐶)–1-1→𝐵) & ⊢ (𝜑 → ((𝐹 “ 𝐶) ∩ (𝐹 “ (𝐴 ∖ 𝐶))) = ∅) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) | ||
| Theorem | funen1cnv 35121 | If a function is equinumerous to ordinal 1, then its converse is also a function. (Contributed by BTernaryTau, 8-Oct-2023.) |
| ⊢ ((Fun 𝐹 ∧ 𝐹 ≈ 1o) → Fun ◡𝐹) | ||
| Theorem | fissorduni 35122 | The union (supremum) of a finite set of ordinals less than a nonzero ordinal class is an element of that ordinal class. (Contributed by BTernaryTau, 15-Jan-2026.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (Ord 𝐵 ∧ 𝐵 ≠ ∅)) → ∪ 𝐴 ∈ 𝐵) | ||
| Theorem | fnrelpredd 35123* | A function that preserves a relation also preserves predecessors. (Contributed by BTernaryTau, 16-Jul-2024.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐹‘𝑥)𝑆(𝐹‘𝑦))) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → Pred(𝑆, (𝐹 “ 𝐶), (𝐹‘𝐷)) = (𝐹 “ Pred(𝑅, 𝐶, 𝐷))) | ||
| Theorem | cardpred 35124 | The cardinality function preserves predecessors. (Contributed by BTernaryTau, 18-Jul-2024.) |
| ⊢ ((𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card) → Pred( E , (card “ 𝐴), (card‘𝐵)) = (card “ Pred( ≺ , 𝐴, 𝐵))) | ||
| Theorem | nummin 35125* | Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024.) |
| ⊢ ((𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 Pred( ≺ , 𝐴, 𝑥) = ∅) | ||
| Theorem | r11 35126 | Value of the cumulative hierarchy of sets function at 1o. (Contributed by BTernaryTau, 24-Jan-2026.) |
| ⊢ (𝑅1‘1o) = 1o | ||
| Theorem | r12 35127 | Value of the cumulative hierarchy of sets function at 2o. (Contributed by BTernaryTau, 25-Jan-2026.) |
| ⊢ (𝑅1‘2o) = 2o | ||
| Theorem | r1wf 35128 | Each stage in the cumulative hierarchy is well-founded. (Contributed by BTernaryTau, 19-Jan-2026.) |
| ⊢ (𝑅1‘𝐴) ∈ ∪ (𝑅1 “ On) | ||
| Theorem | elwf 35129 | An element of a well-founded set is well-founded. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ ∪ (𝑅1 “ On)) | ||
| Theorem | r1elcl 35130 | Each set of the cumulative hierarchy is closed under membership. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ (𝑅1‘𝐵)) | ||
| Theorem | rankval2b 35131* | Value of an alternate definition of the rank function. Definition of [BellMachover] p. 478. This variant of rankval2 9718 does not use Regularity, and so requires the assumption that 𝐴 is in the range of 𝑅1. (Contributed by BTernaryTau, 19-Jan-2026.) |
| ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (𝑅1‘𝑥)}) | ||
| Theorem | rankval4b 35132* | The rank of a set is the supremum of the successors of the ranks of its members. Exercise 9.1 of [Jech] p. 72. Also a special case of Theorem 7V(b) of [Enderton] p. 204. This variant of rankval4 9767 does not use Regularity, and so requires the assumption that 𝐴 is in the range of 𝑅1. (Contributed by BTernaryTau, 19-Jan-2026.) |
| ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) | ||
| Theorem | rankfilimbi 35133* | If all elements in a finite well-founded set have a rank less than a limit ordinal, then the rank of that set is also less than the limit ordinal. (Contributed by BTernaryTau, 19-Jan-2026.) |
| ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ (𝑅1 “ On)) ∧ (∀𝑥 ∈ 𝐴 (rank‘𝑥) ∈ 𝐵 ∧ Lim 𝐵)) → (rank‘𝐴) ∈ 𝐵) | ||
| Theorem | rankfilimb 35134* | The rank of a finite well-founded set is less than a limit ordinal iff the ranks of all of its elements are less than that limit ordinal. (Contributed by BTernaryTau, 22-Jan-2026.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ (𝑅1 “ On) ∧ Lim 𝐵) → ((rank‘𝐴) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (rank‘𝑥) ∈ 𝐵)) | ||
| Theorem | r1filimi 35135* | If all elements in a finite set appear in the cumulative hierarchy prior to a limit ordinal, then that set also appears in the cumulative hierarchy prior to the limit ordinal. (Contributed by BTernaryTau, 19-Jan-2026.) |
| ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑅1 “ 𝐵) ∧ Lim 𝐵) → 𝐴 ∈ ∪ (𝑅1 “ 𝐵)) | ||
| Theorem | r1filim 35136* | A finite set appears in the cumulative hierarchy prior to a limit ordinal iff all of its elements appear in the cumulative hierarchy prior to that limit ordinal. (Contributed by BTernaryTau, 22-Jan-2026.) |
| ⊢ ((𝐴 ∈ Fin ∧ Lim 𝐵) → (𝐴 ∈ ∪ (𝑅1 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑅1 “ 𝐵))) | ||
| Theorem | r1omfi 35137 | Hereditarily finite sets are finite sets. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ ∪ (𝑅1 “ ω) ⊆ Fin | ||
| Theorem | r1omhf 35138* | A set is hereditarily finite iff it is finite and all of its elements are hereditarily finite. (Contributed by BTernaryTau, 19-Jan-2026.) |
| ⊢ (𝐴 ∈ ∪ (𝑅1 “ ω) ↔ (𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑅1 “ ω))) | ||
| Theorem | r1ssel 35139 | A set is a subset of the value of the cumulative hierarchy of sets function iff it is an element of the value at the successor. (Contributed by BTernaryTau, 15-Jan-2026.) |
| ⊢ (𝐵 ∈ On → (𝐴 ⊆ (𝑅1‘𝐵) ↔ 𝐴 ∈ (𝑅1‘suc 𝐵))) | ||
| Theorem | axnulg 35140 | A generalization of ax-nul 5246 in which 𝑥 and 𝑦 need not be distinct. Note that it is possible to use axc7e 2321 to derive elirrv 9490 from this theorem, which justifies the dependency on ax-reg 9485. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.) |
| ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | ||
| Theorem | axnulALT2 35141* | Alternate proof of axnul 5245, proved from propositional calculus, ax-gen 1796, ax-4 1810, ax-5 1911, and ax-inf2 9538. (Contributed by BTernaryTau, 22-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | ||
| Theorem | r1omfv 35142 | Value of the cumulative hierarchy of sets function at ω. (Contributed by BTernaryTau, 25-Jan-2026.) |
| ⊢ (𝑅1‘ω) = ∪ (𝑅1 “ ω) | ||
| Theorem | trssfir1om 35143 | If every element in a transitive class is finite, then every element is also hereditarily finite. (Contributed by BTernaryTau, 24-Jan-2026.) |
| ⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ ∪ (𝑅1 “ ω)) | ||
| Theorem | r1omhfb 35144* | The class of all hereditarily finite sets is the only class with the property that all sets are members of it iff they are finite and all of their elements are members of it. (Contributed by BTernaryTau, 24-Jan-2026.) |
| ⊢ (𝐻 = ∪ (𝑅1 “ ω) ↔ ∀𝑥(𝑥 ∈ 𝐻 ↔ (𝑥 ∈ Fin ∧ ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐻))) | ||
| Axiom | ax-regs 35145* | A strong version of the Axiom of Regularity. It states that if there exists a set with property 𝜑, then there must exist a set with property 𝜑 such that none of its elements have property 𝜑. This axiom can be derived from the axioms of ZF set theory as shown in axregs 35166, but this derivation relies on ax-inf2 9538 and is thus not possible in a finitist context. (Contributed by BTernaryTau, 29-Dec-2025.) |
| ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑)))) | ||
| Theorem | axreg 35146* | Derivation of ax-reg 9485 from ax-regs 35145 and Tarski's FOL axiom schemes. This demonstrates the sense in which ax-regs 35145 is a stronger version of ax-reg 9485. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) | ||
| Theorem | axregscl 35147* | A version of ax-regs 35145 with a class variable instead of a wff variable. Axiom D in Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory (1940), p. 6. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴))) | ||
| Theorem | axregszf 35148* | Derivation of zfregs 9629 using ax-regs 35145. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅) | ||
| Theorem | setindregs 35149* | Set (epsilon) induction. This version of setind 9644 replaces zfregs 9629 with axregszf 35148. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → 𝐴 = V) | ||
| Theorem | setinds2regs 35150* | Principle of set induction (or E-induction). If a property passes from all elements of 𝑥 to 𝑥 itself, then it holds for all 𝑥. (Contributed by BTernaryTau, 31-Dec-2025.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑) ⇒ ⊢ 𝜑 | ||
| Theorem | tz9.1regs 35151* | Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 9626 depends on ax-regs 35145 instead of ax-reg 9485 and ax-inf2 9538. This suggests a possible answer to the third question posed in tz9.1 9626, namely that the missing property is that countably infinite classes must obey regularity. In ZF set theory we can prove this by showing that countably infinite classes are sets and thus ax-reg 9485 applies to them directly, but in a finitist context it seems that an axiom like ax-regs 35145 is required since countably infinite classes are proper classes. (Contributed by BTernaryTau, 31-Dec-2025.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) | ||
| Theorem | unir1regs 35152 | The cumulative hierarchy of sets covers the universe. This version of unir1 9713 replaces setind 9644 with setindregs 35149. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ ∪ (𝑅1 “ On) = V | ||
| Theorem | trssfir1omregs 35153 | If every element in a transitive class is finite, then every element is also hereditarily finite. This version of trssfir1om 35143 replaces setinds2 9648 with setinds2regs 35150. (Contributed by BTernaryTau, 20-Jan-2026.) |
| ⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ ∪ (𝑅1 “ ω)) | ||
| Theorem | r1omhfbregs 35154* | The class of all hereditarily finite sets is the only class with the property that all sets are members of it iff they are finite and all of their elements are members of it. This version of r1omhfb 35144 replaces setinds2 9648 with setinds2regs 35150 and trssfir1om 35143 with trssfir1omregs 35153. (Contributed by BTernaryTau, 21-Jan-2026.) |
| ⊢ (𝐻 = ∪ (𝑅1 “ ω) ↔ ∀𝑥(𝑥 ∈ 𝐻 ↔ (𝑥 ∈ Fin ∧ ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐻))) | ||
| Theorem | fineqvomon 35155 | If the Axiom of Infinity is negated, then the class of all natural numbers equals the proper class of all ordinal numbers. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ (Fin = V → ω = On) | ||
| Theorem | fineqvr1ombregs 35156 | All sets are finite iff all sets are hereditarily finite. (Contributed by BTernaryTau, 30-Dec-2025.) |
| ⊢ (Fin = V ↔ ∪ (𝑅1 “ ω) = V) | ||
| Theorem | prcinf 35157* | Any proper class is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. This proof holds regardless of whether the Axiom of Infinity is accepted or negated. (Contributed by BTernaryTau, 22-Jun-2025.) |
| ⊢ (¬ 𝐴 ∈ V → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) | ||
| Theorem | fineqvrep 35158* | If the Axiom of Infinity is negated, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.) |
| ⊢ (Fin = V → (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))) | ||
| Theorem | fineqvpow 35159* | If the Axiom of Infinity is negated, then the Axiom of Power Sets becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.) |
| ⊢ (Fin = V → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | ||
| Theorem | fineqvac 35160 | If the Axiom of Infinity is negated, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep 5219 and ax-pow 5305, see fineqvacALT 35161. (Contributed by BTernaryTau, 21-Sep-2024.) |
| ⊢ (Fin = V → CHOICE) | ||
| Theorem | fineqvacALT 35161 | Shorter proof of fineqvac 35160 using ax-rep 5219 and ax-pow 5305. (Contributed by BTernaryTau, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (Fin = V → CHOICE) | ||
| Theorem | fineqvnttrclselem1 35162* | Lemma for fineqvnttrclse 35165. (Contributed by BTernaryTau, 12-Jan-2026.) |
| ⊢ (𝐵 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝐴 +o 𝑑) = 𝐵} ∈ ω) | ||
| Theorem | fineqvnttrclselem2 35163* | Lemma for fineqvnttrclse 35165. (Contributed by BTernaryTau, 12-Jan-2026.) |
| ⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵}) ⇒ ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵 ∧ 𝐴 ∈ suc suc 𝑁) → (𝐴 +o (𝐹‘𝐴)) = 𝐵) | ||
| Theorem | fineqvnttrclselem3 35164* | Lemma for fineqvnttrclse 35165. (Contributed by BTernaryTau, 12-Jan-2026.) |
| ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)} & ⊢ 𝐴 = ω & ⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵}) ⇒ ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵) → ∀𝑎 ∈ suc 𝑁(𝐹‘𝑎)𝑅(𝐹‘suc 𝑎)) | ||
| Theorem | fineqvnttrclse 35165* | A counterexample demonstrating that ttrclse 9624 does not hold when all sets are finite. (Contributed by BTernaryTau, 12-Jan-2026.) |
| ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)} & ⊢ 𝐴 = ω ⇒ ⊢ (Fin = V → (𝑅 Se 𝐴 ∧ ¬ t++(𝑅 ↾ 𝐴) Se 𝐴)) | ||
| Theorem | axregs 35166* | Derivation of ax-regs 35145 from the axioms of ZF set theory. (Contributed by BTernaryTau, 29-Dec-2025.) |
| ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑)))) | ||
| Theorem | gblacfnacd 35167* | If 𝐺 is a global choice function, then the Axiom of Choice (in the form of the right-hand side of dfac4 10020) holds. Note that 𝐺 must be a proper class by fndmexb 7842. This means we cannot show that the existence of a class that behaves as a global choice function is sufficient because we only have existential quantifiers for sets, not (proper) classes. However, if a class variant of exlimiv 1931 were available, then it could be used alongside the closed form of this theorem to prove that result. (Contributed by BTernaryTau, 12-Dec-2024.) |
| ⊢ (𝜑 → 𝐺 Fn V) & ⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)) ⇒ ⊢ (𝜑 → ∀𝑥∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) | ||
| Theorem | onvf1odlem1 35168* | Lemma for onvf1od 35172. (Contributed by BTernaryTau, 2-Dec-2025.) |
| ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ 𝐴) | ||
| Theorem | onvf1odlem2 35169* | Lemma for onvf1od 35172. (Contributed by BTernaryTau, 2-Dec-2025.) |
| ⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)) & ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ 𝐴} & ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ 𝐴)) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑉 → 𝑁 ∈ ((𝑅1‘𝑀) ∖ 𝐴))) | ||
| Theorem | onvf1odlem3 35170* | Lemma for onvf1od 35172. The value of 𝐹 at an ordinal 𝐴. (Contributed by BTernaryTau, 2-Dec-2025.) |
| ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤} & ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤)) & ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁)) & ⊢ 𝐵 = ∩ {𝑢 ∈ On ∣ ∃𝑣 ∈ (𝑅1‘𝑢) ¬ 𝑣 ∈ (𝐹 “ 𝐴)} & ⊢ 𝐶 = (𝐺‘((𝑅1‘𝐵) ∖ (𝐹 “ 𝐴))) ⇒ ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | onvf1odlem4 35171* | Lemma for onvf1od 35172. If the range of 𝐹 does not exist, then it must equal the universe. (Contributed by BTernaryTau, 4-Dec-2025.) |
| ⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)) & ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤} & ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤)) & ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁)) & ⊢ 𝐵 = ∩ {𝑢 ∈ On ∣ ∃𝑣 ∈ (𝑅1‘𝑢) ¬ 𝑣 ∈ (𝐹 “ 𝑡)} & ⊢ 𝐶 = (𝐺‘((𝑅1‘𝐵) ∖ (𝐹 “ 𝑡))) ⇒ ⊢ (𝜑 → (¬ ran 𝐹 ∈ V → ran 𝐹 = V)) | ||
| Theorem | onvf1od 35172* | If 𝐺 is a global choice function, then 𝐹 is a bijection from the ordinals to the universe. This is the ZFC version of (1 → 2) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 5-Dec-2025.) |
| ⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)) & ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤} & ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤)) & ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁)) ⇒ ⊢ (𝜑 → 𝐹:On–1-1-onto→V) | ||
| Theorem | vonf1owev 35173* | If 𝐹 is a bijection from the universe to the ordinals, then 𝑅 well-orders the universe. This is the ZFC version of (2 → 3) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 6-Dec-2025.) |
| ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)} ⇒ ⊢ (𝐹:V–1-1-onto→On → 𝑅 We V) | ||
| Theorem | wevgblacfn 35174* | If 𝑅 is a well-ordering of the universe, then 𝐺 is a global choice function. Here 𝐺 maps each set 𝑧 to its minimal element with respect to 𝑅 (except when 𝑧 is the empty set, in which case it is mapped to the empty set, though this is only done for convenience). This is the ZFC version of (3 → 1) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 29-Jun-2025.) |
| ⊢ 𝐺 = (𝑧 ∈ V ↦ ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦}) ⇒ ⊢ (𝑅 We V → (𝐺 Fn V ∧ ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))) | ||
| Theorem | zltp1ne 35175 | Integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1)))) | ||
| Theorem | nnltp1ne 35176 | Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1)))) | ||
| Theorem | nn0ltp1ne 35177 | Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1)))) | ||
| Theorem | 0nn0m1nnn0 35178 | A number is zero if and only if it's a nonnegative integer that becomes negative after subtracting 1. (Contributed by BTernaryTau, 30-Sep-2023.) |
| ⊢ (𝑁 = 0 ↔ (𝑁 ∈ ℕ0 ∧ ¬ (𝑁 − 1) ∈ ℕ0)) | ||
| Theorem | f1resfz0f1d 35179 | If a function with a sequence of nonnegative integers (starting at 0) as its domain is one-to-one when 0 is removed, and if the range of that restriction does not contain the function's value at the removed integer, then the function is itself one-to-one. (Contributed by BTernaryTau, 4-Oct-2023.) |
| ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐹:(0...𝐾)⟶𝑉) & ⊢ (𝜑 → (𝐹 ↾ (1...𝐾)):(1...𝐾)–1-1→𝑉) & ⊢ (𝜑 → ((𝐹 “ {0}) ∩ (𝐹 “ (1...𝐾))) = ∅) ⇒ ⊢ (𝜑 → 𝐹:(0...𝐾)–1-1→𝑉) | ||
| Theorem | fisshasheq 35180 | A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023.) |
| ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝐴 = 𝐵) | ||
| Theorem | revpfxsfxrev 35181 | The reverse of a prefix of a word is equal to the same-length suffix of the reverse of that word. (Contributed by BTernaryTau, 2-Dec-2023.) |
| ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) = ((reverse‘𝑊) substr ⟨((♯‘𝑊) − 𝐿), (♯‘𝑊)⟩)) | ||
| Theorem | swrdrevpfx 35182 | A subword expressed in terms of reverses and prefixes. (Contributed by BTernaryTau, 3-Dec-2023.) |
| ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨𝐹, 𝐿⟩) = (reverse‘((reverse‘(𝑊 prefix 𝐿)) prefix (𝐿 − 𝐹)))) | ||
| Theorem | lfuhgr 35183* | A hypergraph is loop-free if and only if every edge connects at least two vertices. (Contributed by BTernaryTau, 15-Oct-2023.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)2 ≤ (♯‘𝑥))) | ||
| Theorem | lfuhgr2 35184* | A hypergraph is loop-free if and only if every edge is not a loop. (Contributed by BTernaryTau, 15-Oct-2023.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)(♯‘𝑥) ≠ 1)) | ||
| Theorem | lfuhgr3 35185* | A hypergraph is loop-free if and only if none of its edges connect to only one vertex. (Contributed by BTernaryTau, 15-Oct-2023.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ¬ ∃𝑎{𝑎} ∈ (Edg‘𝐺))) | ||
| Theorem | cplgredgex 35186* | Any two (distinct) vertices in a complete graph are connected to each other by at least one edge. (Contributed by BTernaryTau, 2-Oct-2023.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ ComplGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒)) | ||
| Theorem | cusgredgex 35187 | Any two (distinct) vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 3-Oct-2023.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → {𝐴, 𝐵} ∈ 𝐸)) | ||
| Theorem | cusgredgex2 35188 | Any two distinct vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 4-Oct-2023.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝐸)) | ||
| Theorem | pfxwlk 35189 | A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023.) |
| ⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝐿)(Walks‘𝐺)(𝑃 prefix (𝐿 + 1))) | ||
| Theorem | revwlk 35190 | The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023.) |
| ⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃)) | ||
| Theorem | revwlkb 35191 | Two words represent a walk if and only if their reverses also represent a walk. (Contributed by BTernaryTau, 4-Dec-2023.) |
| ⊢ ((𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈) → (𝐹(Walks‘𝐺)𝑃 ↔ (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃))) | ||
| Theorem | swrdwlk 35192 | Two matching subwords of a walk also represent a walk. (Contributed by BTernaryTau, 7-Dec-2023.) |
| ⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐵 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 substr ⟨𝐵, 𝐿⟩)(Walks‘𝐺)(𝑃 substr ⟨𝐵, (𝐿 + 1)⟩)) | ||
| Theorem | pthhashvtx 35193 | A graph containing a path has at least as many vertices as there are edges in the path. (Contributed by BTernaryTau, 5-Oct-2023.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ≤ (♯‘𝑉)) | ||
| Theorem | spthcycl 35194 | A walk is a trivial path if and only if it is both a simple path and a cycle. (Contributed by BTernaryTau, 8-Oct-2023.) |
| ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 𝐹 = ∅) ↔ (𝐹(SPaths‘𝐺)𝑃 ∧ 𝐹(Cycles‘𝐺)𝑃)) | ||
| Theorem | usgrgt2cycl 35195 | A non-trivial cycle in a simple graph has a length greater than 2. (Contributed by BTernaryTau, 24-Sep-2023.) |
| ⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝐹)) | ||
| Theorem | usgrcyclgt2v 35196 | A simple graph with a non-trivial cycle must have at least 3 vertices. (Contributed by BTernaryTau, 5-Oct-2023.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝑉)) | ||
| Theorem | subgrwlk 35197 | If a walk exists in a subgraph of a graph 𝐺, then that walk also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.) |
| ⊢ (𝑆 SubGraph 𝐺 → (𝐹(Walks‘𝑆)𝑃 → 𝐹(Walks‘𝐺)𝑃)) | ||
| Theorem | subgrtrl 35198 | If a trail exists in a subgraph of a graph 𝐺, then that trail also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.) |
| ⊢ (𝑆 SubGraph 𝐺 → (𝐹(Trails‘𝑆)𝑃 → 𝐹(Trails‘𝐺)𝑃)) | ||
| Theorem | subgrpth 35199 | If a path exists in a subgraph of a graph 𝐺, then that path also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.) |
| ⊢ (𝑆 SubGraph 𝐺 → (𝐹(Paths‘𝑆)𝑃 → 𝐹(Paths‘𝐺)𝑃)) | ||
| Theorem | subgrcycl 35200 | If a cycle exists in a subgraph of a graph 𝐺, then that cycle also exists in 𝐺. (Contributed by BTernaryTau, 23-Oct-2023.) |
| ⊢ (𝑆 SubGraph 𝐺 → (𝐹(Cycles‘𝑆)𝑃 → 𝐹(Cycles‘𝐺)𝑃)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |