Home | Metamath
Proof Explorer Theorem List (p. 321 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bnj1366 32001* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
⊢ (𝜓 ↔ (𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ∧ 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑})) ⇒ ⊢ (𝜓 → 𝐵 ∈ V) | ||
Theorem | bnj1379 32002* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) & ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) & ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) & ⊢ (𝜒 ↔ (𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪ 𝐴)) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) & ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) ⇒ ⊢ (𝜓 → Fun ∪ 𝐴) | ||
Theorem | bnj1383 32003* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) & ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) & ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) ⇒ ⊢ (𝜓 → Fun ∪ 𝐴) | ||
Theorem | bnj1385 32004* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) & ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) & ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) & ⊢ (𝑥 ∈ 𝐴 → ∀𝑓 𝑥 ∈ 𝐴) & ⊢ (𝜑′ ↔ ∀ℎ ∈ 𝐴 Fun ℎ) & ⊢ 𝐸 = (dom ℎ ∩ dom 𝑔) & ⊢ (𝜓′ ↔ (𝜑′ ∧ ∀ℎ ∈ 𝐴 ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸))) ⇒ ⊢ (𝜓 → Fun ∪ 𝐴) | ||
Theorem | bnj1386 32005* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) & ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) & ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) & ⊢ (𝑥 ∈ 𝐴 → ∀𝑓 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜓 → Fun ∪ 𝐴) | ||
Theorem | bnj1397 32006 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj1400 32007* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥 | ||
Theorem | bnj1405 32008* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑋 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ∈ 𝐵) | ||
Theorem | bnj1422 32009 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → Fun 𝐴) & ⊢ (𝜑 → dom 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 Fn 𝐵) | ||
Theorem | bnj1424 32010 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ (𝐷 ∈ 𝐴 → (𝐷 ∈ 𝐵 ∨ 𝐷 ∈ 𝐶)) | ||
Theorem | bnj1436 32011 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝜑) | ||
Theorem | bnj1441 32012* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Add disjoint variable condition to avoid ax-13 2383. See bnj1441g 32013 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → ∀𝑦 𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | bnj1441g 32013* | First-order logic and set theory. See bnj1441 32012 for a version with more disjoint variable conditions, but not requiring ax-13 2383. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → ∀𝑦 𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | bnj1454 32014 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐵 ∈ V → (𝐵 ∈ 𝐴 ↔ [𝐵 / 𝑥]𝜑)) | ||
Theorem | bnj1459 32015* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐴)) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜒) | ||
Theorem | bnj1464 32016* | Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | bnj1465 32017* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑉) → ∃𝑥𝜑) | ||
Theorem | bnj1468 32018* | Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | bnj1476 32019 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} & ⊢ (𝜓 → 𝐷 = ∅) ⇒ ⊢ (𝜓 → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | bnj1502 32020 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝐺 ⊆ 𝐹) & ⊢ (𝜑 → 𝐴 ∈ dom 𝐺) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴)) | ||
Theorem | bnj1503 32021 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝐺 ⊆ 𝐹) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐺) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴)) | ||
Theorem | bnj1517 32022 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∣ (𝜑 ∧ 𝜓)} ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝜓) | ||
Theorem | bnj1521 32023 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → ∃𝑥 ∈ 𝐵 𝜑) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜑)) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ (𝜒 → ∃𝑥𝜃) | ||
Theorem | bnj1533 32024 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜃 → ∀𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝐷) & ⊢ 𝐵 ⊆ 𝐴 & ⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ 𝐶 ≠ 𝐸} ⇒ ⊢ (𝜃 → ∀𝑧 ∈ 𝐵 𝐶 = 𝐸) | ||
Theorem | bnj1534 32025* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐻‘𝑥)} & ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹) ⇒ ⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ (𝐹‘𝑧) ≠ (𝐻‘𝑧)} | ||
Theorem | bnj1536 32026* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵)) | ||
Theorem | bnj1538 32027 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝜑) | ||
Theorem | bnj1541 32028 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝐴 ≠ 𝐵)) & ⊢ ¬ 𝜑 ⇒ ⊢ (𝜓 → 𝐴 = 𝐵) | ||
Theorem | bnj1542 32029* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐹 ≠ 𝐺) & ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) ≠ (𝐺‘𝑥)) | ||
Theorem | bnj110 32030* | Well-founded induction restricted to a set (𝐴 ∈ V). 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.) |
⊢ 𝐴 ∈ V & ⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | bnj157 32031* | Well-founded induction restricted to a set (𝐴 ∈ V). 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.) |
⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) & ⊢ 𝐴 ∈ V & ⊢ 𝑅 Fr 𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | bnj66 32032* | Technical lemma for bnj60 32232. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} ⇒ ⊢ (𝑔 ∈ 𝐶 → Rel 𝑔) | ||
Theorem | bnj91 32033* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ 𝑍 ∈ V ⇒ ⊢ ([𝑍 / 𝑦]𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj92 32034* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝑍 ∈ V ⇒ ⊢ ([𝑍 / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑍 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj93 32035* | Technical lemma for bnj97 32038. 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.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → pred(𝑥, 𝐴, 𝑅) ∈ V) | ||
Theorem | bnj95 32036 | Technical lemma for bnj124 32043. 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(𝑥, 𝐴, 𝑅)〉} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | bnj96 32037* | Technical lemma for bnj150 32048. 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.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.) |
⊢ 𝐹 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉} ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → dom 𝐹 = 1o) | ||
Theorem | bnj97 32038* | Technical lemma for bnj150 32048. 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(𝑥, 𝐴, 𝑅)〉} ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj98 32039 | Technical lemma for bnj150 32048. 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.) |
⊢ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)) | ||
Theorem | bnj106 32040* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐹 ∈ V ⇒ ⊢ ([𝐹 / 𝑓][1o / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj118 32041* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) ⇒ ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj121 32042* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) ⇒ ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) | ||
Theorem | bnj124 32043* | Technical lemma for bnj150 32048. 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.) |
⊢ 𝐹 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉} & ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) & ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′) & ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) ⇒ ⊢ (𝜁″ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″))) | ||
Theorem | bnj125 32044* | Technical lemma for bnj150 32048. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) & ⊢ 𝐹 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉} ⇒ ⊢ (𝜑″ ↔ (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj126 32045* | Technical lemma for bnj150 32048. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) & ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) & ⊢ 𝐹 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉} ⇒ ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj130 32046* | Technical lemma for bnj151 32049. 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.) |
⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) & ⊢ (𝜃′ ↔ [1o / 𝑛]𝜃) ⇒ ⊢ (𝜃′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) | ||
Theorem | bnj149 32047* | Technical lemma for bnj151 32049. 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.) |
⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0) & ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′) & ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′) & ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) ⇒ ⊢ 𝜃1 | ||
Theorem | bnj150 32048* | Technical lemma for bnj151 32049. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) & ⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁) & ⊢ 𝐹 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉} & ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) & ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′) ⇒ ⊢ 𝜃0 | ||
Theorem | bnj151 32049* | Technical lemma for bnj153 32052. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜏 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜃)) & ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) & ⊢ (𝜃′ ↔ [1o / 𝑛]𝜃) & ⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁) & ⊢ 𝐹 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉} & ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) & ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′) & ⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0) & ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′) & ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′) ⇒ ⊢ (𝑛 = 1o → ((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃)) | ||
Theorem | bnj154 32050* | Technical lemma for bnj153 32052. 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.) |
⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′) & ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) ⇒ ⊢ (𝜑1 ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj155 32051* | Technical lemma for bnj153 32052. 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.) |
⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ (𝜓1 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj153 32052* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜏 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜃)) ⇒ ⊢ (𝑛 = 1o → ((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃)) | ||
Theorem | bnj207 32053* | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑀 / 𝑛]𝜒) & ⊢ 𝑀 ∈ V ⇒ ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑀 ∧ 𝜑′ ∧ 𝜓′))) | ||
Theorem | bnj213 32054 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴 | ||
Theorem | bnj222 32055* | Technical lemma for bnj229 32056. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ (𝜓 ↔ ∀𝑚 ∈ ω (suc 𝑚 ∈ 𝑁 → (𝐹‘suc 𝑚) = ∪ 𝑦 ∈ (𝐹‘𝑚) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj229 32056* | Technical lemma for bnj517 32057. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ ((𝑛 ∈ 𝑁 ∧ (suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓)) → (𝐹‘𝑛) ⊆ 𝐴) | ||
Theorem | bnj517 32057* | Technical lemma for bnj518 32058. 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.) |
⊢ (𝜑 ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ ((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) → ∀𝑛 ∈ 𝑁 (𝐹‘𝑛) ⊆ 𝐴) | ||
Theorem | bnj518 32058* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏) → ∀𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V) | ||
Theorem | bnj523 32059* | Technical lemma for bnj852 32093. 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(𝑋, 𝐴, 𝑅)) & ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑) & ⊢ 𝑀 ∈ V ⇒ ⊢ (𝜑′ ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj526 32060* | Technical lemma for bnj852 32093. 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(𝑋, 𝐴, 𝑅)) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑) & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj528 32061 | Technical lemma for bnj852 32093. 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(𝑦, 𝐴, 𝑅)〉}) ⇒ ⊢ 𝐺 ∈ V | ||
Theorem | bnj535 32062* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)〉}) & ⊢ (𝜏 ↔ (𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝑛 = (𝑚 ∪ {𝑚}) ∧ 𝑓 Fn 𝑚) → 𝐺 Fn 𝑛) | ||
Theorem | bnj539 32063* | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓) & ⊢ 𝑀 ∈ V ⇒ ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑀 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj540 32064* | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓) & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj543 32065* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)〉}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜎 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) | ||
Theorem | bnj544 32066* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)〉}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) | ||
Theorem | bnj545 32067 | Technical lemma for bnj852 32093. 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 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) & ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝜑″) | ||
Theorem | bnj546 32068* | Technical lemma for bnj852 32093. 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.) |
⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V) | ||
Theorem | bnj548 32069* | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, 𝐶〉}) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) ⇒ ⊢ (((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) ∧ 𝑖 ∈ 𝑚) → 𝐵 = 𝐾) | ||
Theorem | bnj553 32070* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)〉}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, 𝐶〉}) & ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) ⇒ ⊢ (((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖) → (𝐺‘𝑚) = 𝐿) | ||
Theorem | bnj554 32071* | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖)) & ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅) ⇒ ⊢ ((𝜂 ∧ 𝜁) → ((𝐺‘𝑚) = 𝐿 ↔ (𝐺‘suc 𝑖) = 𝐾)) | ||
Theorem | bnj556 32072 | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) ⇒ ⊢ (𝜂 → 𝜎) | ||
Theorem | bnj557 32073* | Technical lemma for bnj852 32093. 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(𝑦, 𝐴, 𝑅)〉}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖)) & ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, 𝐶〉}) & ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁) → (𝐺‘𝑚) = 𝐿) | ||
Theorem | bnj558 32074* | Technical lemma for bnj852 32093. 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(𝑦, 𝐴, 𝑅)〉}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖)) & ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, 𝐶〉}) & ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁) → (𝐺‘suc 𝑖) = 𝐾) | ||
Theorem | bnj561 32075 | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛) | ||
Theorem | bnj562 32076 | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝜑″) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″) | ||
Theorem | bnj570 32077* | Technical lemma for bnj852 32093. 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.) |
⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖)) & ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, 𝐶〉}) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌) → (𝐺‘suc 𝑖) = 𝐾) | ||
Theorem | bnj571 32078* | Technical lemma for bnj852 32093. 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(𝑦, 𝐴, 𝑅)〉}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖)) & ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, 𝐶〉}) & ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) & ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖)) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛) & ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″) | ||
Theorem | bnj605 32079* | Technical lemma. 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.) |
⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒)) & ⊢ (𝜑″ ↔ [𝑓 / 𝑓]𝜑) & ⊢ (𝜓″ ↔ [𝑓 / 𝑓]𝜓) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ 𝑓 ∈ V & ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜑″ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚∃𝑝𝜂) & ⊢ ((𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛) → 𝜒′) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝑓 Fn 𝑛) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″) ⇒ ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) | ||
Theorem | bnj581 32080* | Technical lemma for bnj580 32085. 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.) Remove unnecessary distinct variable conditions. (Revised by Andrew Salmon, 9-Jul-2011.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑) & ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓) & ⊢ (𝜒′ ↔ [𝑔 / 𝑓]𝜒) ⇒ ⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) | ||
Theorem | bnj589 32081* | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑓‘suc 𝑘) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj590 32082 | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ ((𝐵 = suc 𝑖 ∧ 𝜓) → (𝑖 ∈ ω → (𝐵 ∈ 𝑛 → (𝑓‘𝐵) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) | ||
Theorem | bnj591 32083* | Technical lemma for bnj852 32093. 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 | bnj594 32084* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) & ⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))) & ⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)) ⇒ ⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃) | ||
Theorem | bnj580 32085* | Technical lemma for bnj579 32086. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑) & ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓) & ⊢ (𝜒′ ↔ [𝑔 / 𝑓]𝜒) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) & ⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)) ⇒ ⊢ (𝑛 ∈ 𝐷 → ∃*𝑓𝜒) | ||
Theorem | bnj579 32086* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑛 ∈ 𝐷 → ∃*𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) | ||
Theorem | bnj602 32087 | Equality theorem for the pred function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑋 = 𝑌 → pred(𝑋, 𝐴, 𝑅) = pred(𝑌, 𝐴, 𝑅)) | ||
Theorem | bnj607 32088* | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒)) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ 𝐺 ∈ V & ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚∃𝑝𝜂) & ⊢ ((𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛) → 𝜒′) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″) & ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″) & ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜑0 ↔ [ℎ / 𝑓]𝜑) & ⊢ (𝜓0 ↔ [ℎ / 𝑓]𝜓) & ⊢ (𝜑1 ↔ [𝐺 / ℎ]𝜑0) & ⊢ (𝜓1 ↔ [𝐺 / ℎ]𝜓0) ⇒ ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) | ||
Theorem | bnj609 32089* | Technical lemma for bnj852 32093. 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(𝑋, 𝐴, 𝑅)) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑) & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj611 32090* | Technical lemma for bnj852 32093. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓) & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj600 32091* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒)) & ⊢ (𝜑′ ↔ [𝑚 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑚 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑚 / 𝑛]𝜒) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)〉}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) & ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖)) & ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖)) & ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, 𝐶〉}) ⇒ ⊢ (𝑛 ≠ 1o → ((𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒)) | ||
Theorem | bnj601 32092* | Technical lemma for bnj852 32093. 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(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒)) ⇒ ⊢ (𝑛 ≠ 1o → ((𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒)) | ||
Theorem | bnj852 32093* | Technical lemma for bnj69 32180. 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(𝑋, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) | ||
Theorem | bnj864 32094* | Technical lemma for bnj69 32180. 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(𝑋, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷)) & ⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ⇒ ⊢ (𝜒 → ∃!𝑓𝜃) | ||
Theorem | bnj865 32095* | Technical lemma for bnj69 32180. 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(𝑋, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷)) & ⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ⇒ ⊢ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) | ||
Theorem | bnj873 32096* | Technical lemma for bnj69 32180. 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.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑) & ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓) ⇒ ⊢ 𝐵 = {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)} | ||
Theorem | bnj849 32097* | Technical lemma for bnj69 32180. 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.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷)) & ⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑) & ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓) & ⊢ (𝜃′ ↔ [𝑔 / 𝑓]𝜃) & ⊢ (𝜏 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V) | ||
Theorem | bnj882 32098* | Definition (using hypotheses for readability) of the function giving the transitive closure of 𝑋 in 𝐴 by 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} ⇒ ⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) | ||
Theorem | bnj18eq1 32099 | Equality theorem for transitive closure. (Contributed by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
⊢ (𝑋 = 𝑌 → trCl(𝑋, 𝐴, 𝑅) = trCl(𝑌, 𝐴, 𝑅)) | ||
Theorem | bnj893 32100 | Property of trCl. Under certain conditions, the transitive closure of 𝑋 in 𝐴 by 𝑅 is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) ∈ V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |