![]() |
Metamath
Proof Explorer Theorem List (p. 350 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bnj589 34901* | Technical lemma for bnj852 34913. 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 34902 | Technical lemma for bnj852 34913. 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 34903* | Technical lemma for bnj852 34913. 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 34904* | Technical lemma for bnj852 34913. 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 34905* | Technical lemma for bnj579 34906. 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 34906* | Technical lemma for bnj852 34913. 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 34907 | Equality theorem for the pred function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑋 = 𝑌 → pred(𝑋, 𝐴, 𝑅) = pred(𝑌, 𝐴, 𝑅)) | ||
Theorem | bnj607 34908* | Technical lemma for bnj852 34913. 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 34909* | Technical lemma for bnj852 34913. 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 34910* | Technical lemma for bnj852 34913. 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 34911* | Technical lemma for bnj852 34913. 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 34912* | Technical lemma for bnj852 34913. 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 34913* | Technical lemma for bnj69 35002. 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 34914* | Technical lemma for bnj69 35002. 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 34915* | Technical lemma for bnj69 35002. 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 34916* | Technical lemma for bnj69 35002. 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 34917* | Technical lemma for bnj69 35002. 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 34918* | 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 34919 | Equality theorem for transitive closure. (Contributed by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
⊢ (𝑋 = 𝑌 → trCl(𝑋, 𝐴, 𝑅) = trCl(𝑌, 𝐴, 𝑅)) | ||
Theorem | bnj893 34920 | 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) | ||
Theorem | bnj900 34921* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)} ⇒ ⊢ (𝑓 ∈ 𝐵 → ∅ ∈ dom 𝑓) | ||
Theorem | bnj906 34922 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj908 34923* | Technical lemma for bnj69 35002. 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(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑚, 𝐶〉}) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → ∃𝑓(𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″)) | ||
Theorem | bnj911 34924* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑖(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) | ||
Theorem | bnj916 34925* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ⇒ ⊢ (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) | ||
Theorem | bnj917 34926* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ⇒ ⊢ (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) | ||
Theorem | bnj934 34927* | Technical lemma for bnj69 35002. 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 | bnj929 34928* | Technical lemma for bnj69 35002. 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 ⇒ ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑) → 𝜑″) | ||
Theorem | bnj938 34929* | Technical lemma for bnj69 35002. 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 | bnj944 34930* | Technical lemma for bnj69 35002. 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(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜎 ↔ (𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛)) ⇒ ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝜑″) | ||
Theorem | bnj953 34931 | Technical lemma for bnj69 35002. 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 𝑖) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛) ∧ 𝜓) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) | ||
Theorem | bnj958 34932* | Technical lemma for bnj69 35002. 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(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ ((𝐺‘𝑖) = (𝑓‘𝑖) → ∀𝑦(𝐺‘𝑖) = (𝑓‘𝑖)) | ||
Theorem | bnj1000 34933* | Technical lemma for bnj852 34913. 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 & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj965 34934* | Technical lemma for bnj852 34913. 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(𝑦, 𝐴, 𝑅))) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓) & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj964 34935* | Technical lemma for bnj69 35002. 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(𝑦, 𝐴, 𝑅))) & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) & ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) ⇒ ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝜓″) | ||
Theorem | bnj966 34936* | Technical lemma for bnj69 35002. 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(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐶 ∈ V) & ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐺 Fn 𝑝) ⇒ ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) | ||
Theorem | bnj967 34937* | Technical lemma for bnj69 35002. 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(𝑦, 𝐴, 𝑅))) & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐶 ∈ V) ⇒ ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) | ||
Theorem | bnj969 34938* | Technical lemma for bnj69 35002. 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(𝑦, 𝐴, 𝑅) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜎 ↔ (𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛)) ⇒ ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐶 ∈ V) | ||
Theorem | bnj970 34939 | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝑝 ∈ 𝐷) | ||
Theorem | bnj910 34940* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ (𝜏 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜎 ↔ (𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛)) ⇒ ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝜒″) | ||
Theorem | bnj978 34941* | Technical lemma for bnj69 35002. 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 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜃 → 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo( trCl(𝑋, 𝐴, 𝑅), 𝐴, 𝑅)) | ||
Theorem | bnj981 34942* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ⇒ ⊢ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖))) | ||
Theorem | bnj983 34943* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ⇒ ⊢ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) ↔ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖))) | ||
Theorem | bnj984 34944 | Technical lemma for bnj69 35002. 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 | bnj985v 34945* | Version of bnj985 34946 with an additional disjoint variable condition, not requiring ax-13 2374. (Contributed by GG, 27-Mar-2024.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ (𝐺 ∈ 𝐵 ↔ ∃𝑝𝜒″) | ||
Theorem | bnj985 34946* | Technical lemma for bnj69 35002. 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). See bnj985v 34945 for a version with more disjoint variable conditions, not requiring ax-13 2374. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ (𝐺 ∈ 𝐵 ↔ ∃𝑝𝜒″) | ||
Theorem | bnj986 34947* | Technical lemma for bnj69 35002. 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 𝑛)) ⇒ ⊢ (𝜒 → ∃𝑚∃𝑝𝜏) | ||
Theorem | bnj996 34948* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) & ⊢ (𝜂 ↔ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} ⇒ ⊢ ∃𝑓∃𝑛∃𝑖∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) | ||
Theorem | bnj998 34949* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) & ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → 𝜒″) | ||
Theorem | bnj999 34950* | Technical lemma for bnj69 35002. 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 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → pred(𝑦, 𝐴, 𝑅) ⊆ (𝐺‘suc 𝑖)) | ||
Theorem | bnj1001 34951 | Technical lemma for bnj69 35002. 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 𝑖 ∈ 𝑝)) | ||
Theorem | bnj1006 34952* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) & ⊢ (𝜂 ↔ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) & ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → (𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝)) ⇒ ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → pred(𝑦, 𝐴, 𝑅) ⊆ (𝐺‘suc 𝑖)) | ||
Theorem | bnj1014 34953* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj1015 34954* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ 𝐺 ∈ 𝑉 & ⊢ 𝐽 ∈ 𝑉 ⇒ ⊢ ((𝐺 ∈ 𝐵 ∧ 𝐽 ∈ dom 𝐺) → (𝐺‘𝐽) ⊆ trCl(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj1018g 34955* | Version of bnj1018 34956 with less disjoint variable conditions, but requiring ax-13 2374. (Contributed by GG, 27-Mar-2024.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) & ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ (𝜒″ ↔ (𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″)) & ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → 𝜒″) & ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → (𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝)) ⇒ ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏) → (𝐺‘suc 𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj1018 34956* | Technical lemma for bnj69 35002. 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). See bnj1018g 34955 for a less restrictive version requiring ax-13 2374. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) & ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ (𝜒″ ↔ (𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″)) & ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → 𝜒″) & ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → (𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝)) ⇒ ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏) → (𝐺‘suc 𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj1020 34957* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) & ⊢ (𝜂 ↔ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) & ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ (𝜒″ ↔ (𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″)) ⇒ ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏) → pred(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj1021 34958* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) & ⊢ (𝜂 ↔ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} ⇒ ⊢ ∃𝑓∃𝑛∃𝑖∃𝑚(𝜃 → (𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏)) | ||
Theorem | bnj907 34959* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) & ⊢ (𝜂 ↔ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) & ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) & ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) & ⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo( trCl(𝑋, 𝐴, 𝑅), 𝐴, 𝑅)) | ||
Theorem | bnj1029 34960 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo( trCl(𝑋, 𝐴, 𝑅), 𝐴, 𝑅)) | ||
Theorem | bnj1033 34961* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) & ⊢ (𝜂 ↔ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) & ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) ⇒ ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj1034 34962* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) & ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) ⇒ ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj1039 34963 | Technical lemma for bnj69 35002. 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 | bnj1040 34964* | Technical lemma for bnj69 35002. 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 | bnj1047 34965 | Technical lemma for bnj69 35002. 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 𝑖 → [𝑗 / 𝑖]𝜂)) & ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂) ⇒ ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → 𝜂′)) | ||
Theorem | bnj1049 34966 | Technical lemma for bnj69 35002. 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 | bnj1052 34967* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) & ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)) & ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂)) & ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ( E Fr 𝑛 ∧ ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂))) ⇒ ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj1053 34968* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) & ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)) & ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂)) & ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂)) ⇒ ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj1071 34969 | Technical lemma for bnj69 35002. 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 Fr 𝑛) | ||
Theorem | bnj1083 34970 | Technical lemma for bnj69 35002. 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 | bnj1090 34971* | Technical lemma for bnj69 35002. 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.) |
⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) & ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂)) & ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂) & ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) & ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) & ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) ⇒ ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂)) | ||
Theorem | bnj1093 34972* | Technical lemma for bnj69 35002. 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.) |
⊢ ∃𝑗(((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0) → (𝑓‘𝑖) ⊆ 𝐵) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ⇒ ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) | ||
Theorem | bnj1097 34973 | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) ⇒ ⊢ ((𝑖 = ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓‘𝑖) ⊆ 𝐵) | ||
Theorem | bnj1110 34974* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) & ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) & ⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) ⇒ ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ (𝑓‘𝑗) ⊆ 𝐵)) | ||
Theorem | bnj1112 34975* | Technical lemma for bnj69 35002. 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 | bnj1118 34976* | Technical lemma for bnj69 35002. 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(𝑦, 𝐴, 𝑅))) & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) & ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) & ⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) ⇒ ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓‘𝑖) ⊆ 𝐵) | ||
Theorem | bnj1121 34977 | Technical lemma for bnj69 35002. 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 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) & ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) & ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 𝜂) & ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} ⇒ ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) | ||
Theorem | bnj1123 34978* | Technical lemma for bnj69 35002. 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(𝑦, 𝐴, 𝑅))) & ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) & ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂) ⇒ ⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) | ||
Theorem | bnj1030 34979* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) & ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) & ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂)) & ⊢ (𝜑′ ↔ [𝑗 / 𝑖]𝜑) & ⊢ (𝜓′ ↔ [𝑗 / 𝑖]𝜓) & ⊢ (𝜒′ ↔ [𝑗 / 𝑖]𝜒) & ⊢ (𝜃′ ↔ [𝑗 / 𝑖]𝜃) & ⊢ (𝜏′ ↔ [𝑗 / 𝑖]𝜏) & ⊢ (𝜁′ ↔ [𝑗 / 𝑖]𝜁) & ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂) & ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) & ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) ⇒ ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj1124 34980 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) ⇒ ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj1133 34981* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜏 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜃)) & ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜏) → 𝜃) ⇒ ⊢ (𝜒 → ∀𝑖 ∈ 𝑛 𝜃) | ||
Theorem | bnj1128 34982* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ (𝜒 → (𝑓‘𝑖) ⊆ 𝐴)) & ⊢ (𝜏 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜃)) & ⊢ (𝜑′ ↔ [𝑗 / 𝑖]𝜑) & ⊢ (𝜓′ ↔ [𝑗 / 𝑖]𝜓) & ⊢ (𝜒′ ↔ [𝑗 / 𝑖]𝜒) & ⊢ (𝜃′ ↔ [𝑗 / 𝑖]𝜃) ⇒ ⊢ (𝑌 ∈ trCl(𝑋, 𝐴, 𝑅) → 𝑌 ∈ 𝐴) | ||
Theorem | bnj1127 34983 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑌 ∈ trCl(𝑋, 𝐴, 𝑅) → 𝑌 ∈ 𝐴) | ||
Theorem | bnj1125 34984 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl(𝑋, 𝐴, 𝑅)) → trCl(𝑌, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj1145 34985* | Technical lemma for bnj69 35002. 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 𝑛 ∧ 𝜑 ∧ 𝜓)} & ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))) ⇒ ⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴 | ||
Theorem | bnj1147 34986 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴 | ||
Theorem | bnj1137 34987* | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo(𝐵, 𝐴, 𝑅)) | ||
Theorem | bnj1148 34988 | Property of pred. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ∈ V) | ||
Theorem | bnj1136 34989* | Technical lemma for bnj69 35002. 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(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) & ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵) | ||
Theorem | bnj1152 34990 | Technical lemma for bnj69 35002. 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(𝑋, 𝐴, 𝑅) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋)) | ||
Theorem | bnj1154 34991* | Property of Fr. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ∈ V) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | bnj1171 34992 | Technical lemma for bnj69 35002. 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 | bnj1172 34993 | Technical lemma for bnj69 35002. 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.) |
⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵) & ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵)))) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (𝜃 ↔ 𝑤 ∈ 𝐴)) ⇒ ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐴 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵)))) | ||
Theorem | bnj1173 34994 | Technical lemma for bnj69 35002. 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.) |
⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵) & ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑅 FrSe 𝐴) & ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (𝜃 ↔ 𝑤 ∈ 𝐴)) | ||
Theorem | bnj1174 34995 | Technical lemma for bnj69 35002. 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.) |
⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵) & ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))) & ⊢ (𝜃 → (𝑤𝑅𝑧 → 𝑤 ∈ trCl(𝑋, 𝐴, 𝑅))) ⇒ ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵)))) | ||
Theorem | bnj1175 34996 | Technical lemma for bnj69 35002. 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.) |
⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵) & ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧))) & ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴)) ⇒ ⊢ (𝜃 → (𝑤𝑅𝑧 → 𝑤 ∈ trCl(𝑋, 𝐴, 𝑅))) | ||
Theorem | bnj1176 34997* | Technical lemma for bnj69 35002. 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.) |
⊢ ((𝜑 ∧ 𝜓) → (𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V)) & ⊢ ((𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V) → ∃𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧) ⇒ ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))) | ||
Theorem | bnj1177 34998 | Technical lemma for bnj69 35002. 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.) |
⊢ (𝜓 ↔ (𝑋 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑋)) & ⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵) & ⊢ ((𝜑 ∧ 𝜓) → 𝑅 FrSe 𝐴) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V)) | ||
Theorem | bnj1186 34999* | Technical lemma for bnj69 35002. 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 | bnj1190 35000* | Technical lemma for bnj69 35002. 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 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) & ⊢ (𝜓 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∃𝑤 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝑤) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |