Home | Metamath
Proof Explorer Theorem List (p. 324 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bnj1321 32301* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ ∃𝑓𝜏) → ∃!𝑓𝜏) | ||
Theorem | bnj1364 32302 | Property of FrSe. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑅 FrSe 𝐴 → 𝑅 Se 𝐴) | ||
Theorem | bnj1371 32303* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ (𝜏′ ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))) ⇒ ⊢ (𝑓 ∈ 𝐻 → Fun 𝑓) | ||
Theorem | bnj1373 32304* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) ⇒ ⊢ (𝜏′ ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))) | ||
Theorem | bnj1374 32305* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} ⇒ ⊢ (𝑓 ∈ 𝐻 → 𝑓 ∈ 𝐶) | ||
Theorem | bnj1384 32306* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 ⇒ ⊢ (𝑅 FrSe 𝐴 → Fun 𝑃) | ||
Theorem | bnj1388 32307* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) ⇒ ⊢ (𝜒 → ∀𝑦 ∈ pred (𝑥, 𝐴, 𝑅)∃𝑓𝜏′) | ||
Theorem | bnj1398 32308* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑥, 𝐴, 𝑅)({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))) & ⊢ (𝜂 ↔ (𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑧 ∈ ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))) ⇒ ⊢ (𝜒 → ∪ 𝑦 ∈ pred (𝑥, 𝐴, 𝑅)({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)) = dom 𝑃) | ||
Theorem | bnj1413 32309* | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V) | ||
Theorem | bnj1408 32310* | Technical lemma for bnj1414 32311. 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 (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) & ⊢ 𝐶 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵) | ||
Theorem | bnj1414 32311* | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵) | ||
Theorem | bnj1415 32312* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 ⇒ ⊢ (𝜒 → dom 𝑃 = trCl(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj1416 32313 | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ (𝜒 → dom 𝑃 = trCl(𝑥, 𝐴, 𝑅)) ⇒ ⊢ (𝜒 → dom 𝑄 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) | ||
Theorem | bnj1418 32314 | Property of pred. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → 𝑦𝑅𝑥) | ||
Theorem | bnj1417 32315* | Technical lemma for bnj60 32336. 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.) |
⊢ (𝜑 ↔ 𝑅 FrSe 𝐴) & ⊢ (𝜓 ↔ ¬ 𝑥 ∈ trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜓)) & ⊢ (𝜃 ↔ (𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒)) & ⊢ 𝐵 = ( pred(𝑥, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ trCl(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj1421 32316* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ (𝜒 → Fun 𝑃) & ⊢ (𝜒 → dom 𝑄 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) & ⊢ (𝜒 → dom 𝑃 = trCl(𝑥, 𝐴, 𝑅)) ⇒ ⊢ (𝜒 → Fun 𝑄) | ||
Theorem | bnj1444 32317* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 & ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸)) & ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥})) & ⊢ (𝜁 ↔ (𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))) & ⊢ (𝜌 ↔ (𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓)) ⇒ ⊢ (𝜌 → ∀𝑦𝜌) | ||
Theorem | bnj1445 32318* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 & ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸)) & ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥})) & ⊢ (𝜁 ↔ (𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))) & ⊢ (𝜌 ↔ (𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓)) & ⊢ (𝜎 ↔ (𝜌 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))) & ⊢ (𝜑 ↔ (𝜎 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) & ⊢ 𝑋 = 〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉 ⇒ ⊢ (𝜎 → ∀𝑑𝜎) | ||
Theorem | bnj1446 32319* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 ⇒ ⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑑(𝑄‘𝑧) = (𝐺‘𝑊)) | ||
Theorem | bnj1447 32320* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 ⇒ ⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑦(𝑄‘𝑧) = (𝐺‘𝑊)) | ||
Theorem | bnj1448 32321* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 ⇒ ⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑓(𝑄‘𝑧) = (𝐺‘𝑊)) | ||
Theorem | bnj1449 32322* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 & ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸)) & ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥})) & ⊢ (𝜁 ↔ (𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))) ⇒ ⊢ (𝜁 → ∀𝑓𝜁) | ||
Theorem | bnj1442 32323* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 & ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸)) & ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥})) ⇒ ⊢ (𝜂 → (𝑄‘𝑧) = (𝐺‘𝑊)) | ||
Theorem | bnj1450 32324* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 & ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸)) & ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥})) & ⊢ (𝜁 ↔ (𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))) & ⊢ (𝜌 ↔ (𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓)) & ⊢ (𝜎 ↔ (𝜌 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))) & ⊢ (𝜑 ↔ (𝜎 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) & ⊢ 𝑋 = 〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉 ⇒ ⊢ (𝜁 → (𝑄‘𝑧) = (𝐺‘𝑊)) | ||
Theorem | bnj1423 32325* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 & ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) ⇒ ⊢ (𝜒 → ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊)) | ||
Theorem | bnj1452 32326* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 & ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) ⇒ ⊢ (𝜒 → 𝐸 ∈ 𝐵) | ||
Theorem | bnj1466 32327* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) ⇒ ⊢ (𝑤 ∈ 𝑄 → ∀𝑓 𝑤 ∈ 𝑄) | ||
Theorem | bnj1467 32328* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) ⇒ ⊢ (𝑤 ∈ 𝑄 → ∀𝑑 𝑤 ∈ 𝑄) | ||
Theorem | bnj1463 32329* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 & ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) & ⊢ (𝜒 → 𝑄 ∈ V) & ⊢ (𝜒 → ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊)) & ⊢ (𝜒 → 𝑄 Fn 𝐸) & ⊢ (𝜒 → 𝐸 ∈ 𝐵) ⇒ ⊢ (𝜒 → 𝑄 ∈ 𝐶) | ||
Theorem | bnj1489 32330* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) ⇒ ⊢ (𝜒 → 𝑄 ∈ V) | ||
Theorem | bnj1491 32331* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ (𝜒 → (𝑄 ∈ 𝐶 ∧ dom 𝑄 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) ⇒ ⊢ ((𝜒 ∧ 𝑄 ∈ V) → ∃𝑓(𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) | ||
Theorem | bnj1312 32332* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} & ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) & ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} & ⊢ 𝑃 = ∪ 𝐻 & ⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) & ⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 & ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) ⇒ ⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) | ||
Theorem | bnj1493 32333* | Technical lemma for bnj60 32336. 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 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) | ||
Theorem | bnj1497 32334* | Technical lemma for bnj60 32336. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} ⇒ ⊢ ∀𝑔 ∈ 𝐶 Fun 𝑔 | ||
Theorem | bnj1498 32335* | Technical lemma for bnj60 32336. 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 𝐴 → dom 𝐹 = 𝐴) | ||
Theorem | bnj60 32336* | 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.) |
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} & ⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ 𝐹 = ∪ 𝐶 ⇒ ⊢ (𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴) | ||
Theorem | bnj1514 32337* | Technical lemma for bnj1500 32342. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} ⇒ ⊢ (𝑓 ∈ 𝐶 → ∀𝑥 ∈ dom 𝑓(𝑓‘𝑥) = (𝐺‘𝑌)) | ||
Theorem | bnj1518 32338* | Technical lemma for bnj1500 32342. 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 𝐴 ∧ 𝑥 ∈ 𝐴)) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓)) ⇒ ⊢ (𝜓 → ∀𝑑𝜓) | ||
Theorem | bnj1519 32339* | Technical lemma for bnj1500 32342. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ 𝐹 = ∪ 𝐶 ⇒ ⊢ ((𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) → ∀𝑑(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) | ||
Theorem | bnj1520 32340* | Technical lemma for bnj1500 32342. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ 𝐹 = ∪ 𝐶 ⇒ ⊢ ((𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) → ∀𝑓(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) | ||
Theorem | bnj1501 32341* | Technical lemma for bnj1500 32342. 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 𝐴 ∧ 𝑥 ∈ 𝐴)) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓)) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑)) ⇒ ⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) | ||
Theorem | bnj1500 32342* | 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 32343* | Technical lemma for bnj1522 32346. 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 32344* | Technical lemma for bnj1522 32346. 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 32345* | Technical lemma for bnj1522 32346. 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 32346* | 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 | exdifsn 32347 | 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 32348 | 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 32349 | 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 | zltp1ne 32350 | Integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1)))) | ||
Theorem | nnltp1ne 32351 | Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1)))) | ||
Theorem | nn0ltp1ne 32352 | Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1)))) | ||
Theorem | 0nn0m1nnn0 32353 | 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 | fisshasheq 32354 | A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝐴 = 𝐵) | ||
Theorem | dff15 32355* | 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 | hashfundm 32356 | The size of a set function is equal to the size of its domain. (Contributed by BTernaryTau, 30-Sep-2023.) |
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (♯‘𝐹) = (♯‘dom 𝐹)) | ||
Theorem | hashf1dmrn 32357 | The size of the domain of a one-to-one set function is equal to the size of its range. (Contributed by BTernaryTau, 1-Oct-2023.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (♯‘𝐴) = (♯‘ran 𝐹)) | ||
Theorem | hashf1dmcdm 32358 | The size of the domain of a one-to-one set function is less than or equal to the size of its codomain, if it exists. (Contributed by BTernaryTau, 1-Oct-2023.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)) | ||
Theorem | funen1cnv 32359 | 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 | f1resveqaeq 32360 | 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 32361 | Lemma for f1resrcmplf1d 32362. (Contributed by BTernaryTau, 27-Sep-2023.) |
⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ((𝐹 “ 𝐶) ∩ (𝐹 “ 𝐷)) = ∅) ⇒ ⊢ (𝜑 → ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐷) → ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑋 = 𝑌))) | ||
Theorem | f1resrcmplf1d 32362 | 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 | f1resfz0f1d 32363 | 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 | revpfxsfxrev 32364 | 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 32365 | 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 32366* | 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 32367* | 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 32368* | 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 32369* | 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 32370 | 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 32371 | 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 32372 | A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝐿)(Walks‘𝐺)(𝑃 prefix (𝐿 + 1))) | ||
Theorem | revwlk 32373 | The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023.) |
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃)) | ||
Theorem | revwlkb 32374 | 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 32375 | 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 32376 | 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 | pthisspthorcycl 32377 | A path is either a simple path or a cycle (or both). (Contributed by BTernaryTau, 20-Oct-2023.) |
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝐹(SPaths‘𝐺)𝑃 ∨ 𝐹(Cycles‘𝐺)𝑃)) | ||
Theorem | spthcycl 32378 | 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 32379 | 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 32380 | 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 32381 | 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 32382 | 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 32383 | 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 32384 | 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‘𝐺)𝑃)) | ||
Theorem | cusgr3cyclex 32385* | Every complete simple graph with more than two vertices has a 3-cycle. (Contributed by BTernaryTau, 4-Oct-2023.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 2 < (♯‘𝑉)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3)) | ||
Theorem | loop1cycl 32386* | A hypergraph has a cycle of length one if and only if it has a loop. (Contributed by BTernaryTau, 13-Oct-2023.) |
⊢ (𝐺 ∈ UHGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ {𝐴} ∈ (Edg‘𝐺))) | ||
Theorem | 2cycld 32387 | Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐽 ≠ 𝐾) & ⊢ (𝜑 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃) | ||
Theorem | 2cycl2d 32388 | Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐴”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐴, 𝐵} ⊆ (𝐼‘𝐾))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐽 ≠ 𝐾) ⇒ ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃) | ||
Theorem | umgr2cycllem 32389* | Lemma for umgr2cycl 32390. (Contributed by BTernaryTau, 17-Oct-2023.) |
⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ UMGraph) & ⊢ (𝜑 → 𝐽 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐽 ≠ 𝐾) & ⊢ (𝜑 → (𝐼‘𝐽) = (𝐼‘𝐾)) ⇒ ⊢ (𝜑 → ∃𝑝 𝐹(Cycles‘𝐺)𝑝) | ||
Theorem | umgr2cycl 32390* | A multigraph with two distinct edges that connect the same vertices has a 2-cycle. (Contributed by BTernaryTau, 17-Oct-2023.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ ∃𝑗 ∈ dom 𝐼∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) | ||
Syntax | cacycgr 32391 | Extend class notation with acyclic graphs. |
class AcyclicGraph | ||
Definition | df-acycgr 32392* | Define the class of all acyclic graphs. A graph is called acyclic if it has no (non-trivial) cycles. (Contributed by BTernaryTau, 11-Oct-2023.) |
⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)} | ||
Theorem | dfacycgr1 32393* | An alternate definition of the class of all acyclic graphs that requires all cycles to be trivial. (Contributed by BTernaryTau, 11-Oct-2023.) |
⊢ AcyclicGraph = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)} | ||
Theorem | isacycgr 32394* | The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.) |
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅))) | ||
Theorem | isacycgr1 32395* | The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.) |
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝐺)𝑝 → 𝑓 = ∅))) | ||
Theorem | acycgrcycl 32396 | Any cycle in an acyclic graph is trivial (i.e. has one vertex and no edges). (Contributed by BTernaryTau, 12-Oct-2023.) |
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → 𝐹 = ∅) | ||
Theorem | acycgr0v 32397 | A null graph (with no vertices) is an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅) → 𝐺 ∈ AcyclicGraph) | ||
Theorem | acycgr1v 32398 | A multigraph with one vertex is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ (♯‘𝑉) = 1) → 𝐺 ∈ AcyclicGraph) | ||
Theorem | acycgr2v 32399 | A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 2) → 𝐺 ∈ AcyclicGraph) | ||
Theorem | prclisacycgr 32400* | A proper class (representing a null graph, see vtxvalprc 26832) has the property of an acyclic graph (see also acycgr0v 32397). (Contributed by BTernaryTau, 11-Oct-2023.) (New usage is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (¬ 𝐺 ∈ V → ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |