![]() |
Metamath
Proof Explorer Theorem List (p. 320 of 443) | < 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-28474) |
![]() (28475-29999) |
![]() (30000-44279) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bnj1083 31901 | Technical lemma for bnj69 31933. 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 31902* | Technical lemma for bnj69 31933. 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 31903* | Technical lemma for bnj69 31933. 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 31904 | Technical lemma for bnj69 31933. 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 31905* | Technical lemma for bnj69 31933. 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 31906* | Technical lemma for bnj69 31933. 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 31907* | Technical lemma for bnj69 31933. 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 31908 | Technical lemma for bnj69 31933. 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 31909* | Technical lemma for bnj69 31933. 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 31910* | Technical lemma for bnj69 31933. 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 31911 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) & ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) ⇒ ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj1133 31912* | Technical lemma for bnj69 31933. 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 31913* | Technical lemma for bnj69 31933. 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 31914 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑌 ∈ trCl(𝑋, 𝐴, 𝑅) → 𝑌 ∈ 𝐴) | ||
Theorem | bnj1125 31915 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl(𝑋, 𝐴, 𝑅)) → trCl(𝑌, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj1145 31916* | Technical lemma for bnj69 31933. 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 31917 | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴 | ||
Theorem | bnj1137 31918* | 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 31919 | Property of pred. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ∈ V) | ||
Theorem | bnj1136 31920* | Technical lemma for bnj69 31933. 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 31921 | Technical lemma for bnj69 31933. 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 31922* | Property of Fr. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ∈ V) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | bnj1171 31923 | Technical lemma for bnj69 31933. 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 31924 | Technical lemma for bnj69 31933. 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 31925 | Technical lemma for bnj69 31933. 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 31926 | Technical lemma for bnj69 31933. 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 31927 | Technical lemma for bnj69 31933. 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 31928* | Technical lemma for bnj69 31933. 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 31929 | Technical lemma for bnj69 31933. 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 31930* | Technical lemma for bnj69 31933. 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 31931* | Technical lemma for bnj69 31933. 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 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) & ⊢ (𝜓 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∃𝑤 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝑤) | ||
Theorem | bnj1189 31932* | Technical lemma for bnj69 31933. 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 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) & ⊢ (𝜓 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) & ⊢ (𝜒 ↔ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | bnj69 31933* | Existence of a minimal element in certain classes: if 𝑅 is well-founded and set-like on 𝐴, then every nonempty subclass of 𝐴 has a minimal element. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | bnj1228 31934* | Existence of a minimal element in certain classes: if 𝑅 is well-founded and set-like on 𝐴, then every nonempty subclass of 𝐴 has a minimal element. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑤 ∈ 𝐵 → ∀𝑥 𝑤 ∈ 𝐵) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | bnj1204 31935* | Well-founded induction. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | bnj1234 31936* | Technical lemma for bnj60 31985. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ 𝑍 = 〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝐷 = {𝑔 ∣ ∃𝑑 ∈ 𝐵 (𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘𝑍))} ⇒ ⊢ 𝐶 = 𝐷 | ||
Theorem | bnj1245 31937* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) & ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥)) & ⊢ 𝑍 = 〈𝑥, (ℎ ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝐾 = {ℎ ∣ ∃𝑑 ∈ 𝐵 (ℎ Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (ℎ‘𝑥) = (𝐺‘𝑍))} ⇒ ⊢ (𝜑 → dom ℎ ⊆ 𝐴) | ||
Theorem | bnj1256 31938* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) & ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 𝑔 Fn 𝑑) | ||
Theorem | bnj1259 31939* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) & ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 ℎ Fn 𝑑) | ||
Theorem | bnj1253 31940* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) & ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → 𝐸 ≠ ∅) | ||
Theorem | bnj1279 31941* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) & ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥)) ⇒ ⊢ ((𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥) → ( pred(𝑥, 𝐴, 𝑅) ∩ 𝐸) = ∅) | ||
Theorem | bnj1286 31942* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) & ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥)) ⇒ ⊢ (𝜓 → pred(𝑥, 𝐴, 𝑅) ⊆ 𝐷) | ||
Theorem | bnj1280 31943* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) & ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜓 → ( pred(𝑥, 𝐴, 𝑅) ∩ 𝐸) = ∅) ⇒ ⊢ (𝜓 → (𝑔 ↾ pred(𝑥, 𝐴, 𝑅)) = (ℎ ↾ pred(𝑥, 𝐴, 𝑅))) | ||
Theorem | bnj1296 31944* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) & ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} & ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))) & ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥)) & ⊢ (𝜓 → (𝑔 ↾ pred(𝑥, 𝐴, 𝑅)) = (ℎ ↾ pred(𝑥, 𝐴, 𝑅))) & ⊢ 𝑍 = 〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝐾 = {𝑔 ∣ ∃𝑑 ∈ 𝐵 (𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘𝑍))} & ⊢ 𝑊 = 〈𝑥, (ℎ ↾ pred(𝑥, 𝐴, 𝑅))〉 & ⊢ 𝐿 = {ℎ ∣ ∃𝑑 ∈ 𝐵 (ℎ Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (ℎ‘𝑥) = (𝐺‘𝑊))} ⇒ ⊢ (𝜓 → (𝑔‘𝑥) = (ℎ‘𝑥)) | ||
Theorem | bnj1309 31945* | Technical lemma for bnj60 31985. 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 | bnj1307 31946* | Technical lemma for bnj60 31985. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} & ⊢ (𝑤 ∈ 𝐵 → ∀𝑥 𝑤 ∈ 𝐵) ⇒ ⊢ (𝑤 ∈ 𝐶 → ∀𝑥 𝑤 ∈ 𝐶) | ||
Theorem | bnj1311 31947* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶) → (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷)) | ||
Theorem | bnj1318 31948 | Technical lemma for bnj60 31985. 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 | bnj1326 31949* | Technical lemma for bnj60 31985. 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 𝑔 ∩ dom ℎ) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶) → (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷)) | ||
Theorem | bnj1321 31950* | Technical lemma for bnj60 31985. 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 31951 | Property of FrSe. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑅 FrSe 𝐴 → 𝑅 Se 𝐴) | ||
Theorem | bnj1371 31952* | Technical lemma for bnj60 31985. 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 31953* | Technical lemma for bnj60 31985. 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 31954* | Technical lemma for bnj60 31985. 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 31955* | Technical lemma for bnj60 31985. 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 31956* | Technical lemma for bnj60 31985. 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 31957* | Technical lemma for bnj60 31985. 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 31958* | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V) | ||
Theorem | bnj1408 31959* | Technical lemma for bnj1414 31960. 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 31960* | Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵) | ||
Theorem | bnj1415 31961* | Technical lemma for bnj60 31985. 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 31962 | Technical lemma for bnj60 31985. 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 31963 | Property of pred. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → 𝑦𝑅𝑥) | ||
Theorem | bnj1417 31964* | Technical lemma for bnj60 31985. 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 31965* | Technical lemma for bnj60 31985. 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 31966* | Technical lemma for bnj60 31985. 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 31967* | Technical lemma for bnj60 31985. 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 31968* | Technical lemma for bnj60 31985. 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 31969* | Technical lemma for bnj60 31985. 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 31970* | Technical lemma for bnj60 31985. 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 31971* | Technical lemma for bnj60 31985. 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 31972* | Technical lemma for bnj60 31985. 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 31973* | Technical lemma for bnj60 31985. 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 31974* | Technical lemma for bnj60 31985. 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 31975* | Technical lemma for bnj60 31985. 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 31976* | Technical lemma for bnj60 31985. 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 31977* | Technical lemma for bnj60 31985. 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 31978* | Technical lemma for bnj60 31985. 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 31979* | Technical lemma for bnj60 31985. 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 31980* | Technical lemma for bnj60 31985. 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 31981* | Technical lemma for bnj60 31985. 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 31982* | Technical lemma for bnj60 31985. 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 31983* | Technical lemma for bnj60 31985. 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 31984* | Technical lemma for bnj60 31985. 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 31985* | 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 31986* | Technical lemma for bnj1500 31991. 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 31987* | Technical lemma for bnj1500 31991. 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 31988* | Technical lemma for bnj1500 31991. 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 31989* | Technical lemma for bnj1500 31991. 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 31990* | Technical lemma for bnj1500 31991. 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 31991* | 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 31992* | Technical lemma for bnj1522 31995. 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 31993* | Technical lemma for bnj1522 31995. 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 31994* | Technical lemma for bnj1522 31995. 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 31995* | 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 31996 | 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.) |
⊢ (∃𝑥 𝑥 ∈ (𝐴 ∖ {𝐵}) ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 𝐵) | ||
Axiom | ax-7d 31997* | Distinct variable version of ax-11 2093. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Axiom | ax-8d 31998* | Distinct variable version of ax-7 1965. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Axiom | ax-9d1 31999 | Distinct variable version of ax-6 1928, equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑥 | ||
Axiom | ax-9d2 32000* | Distinct variable version of ax-6 1928, distinct variables case. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |