| Metamath
Proof Explorer Theorem List (p. 451 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pwclaxpow 45001* | Suppose 𝑀 is a transitive class that is closed under power sets intersected with 𝑀. Then, 𝑀 models the Axiom of Power Sets ax-pow 5365. One direction of Lemma II.2.8 of [Kunen2] p. 113. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ ((Tr 𝑀 ∧ ∀𝑥 ∈ 𝑀 (𝒫 𝑥 ∩ 𝑀) ∈ 𝑀) → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | ||
| Theorem | prclaxpr 45002* | A class that is closed under the pairing operation models the Axiom of Pairing ax-pr 5432. Lemma II.2.4(4) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 29-Sep-2025.) |
| ⊢ (∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 {𝑥, 𝑦} ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∃𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)) | ||
| Theorem | uniclaxun 45003* | A class that is closed under the union operation models the Axiom of Union ax-un 7755. Lemma II.2.4(5) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 1-Oct-2025.) |
| ⊢ (∀𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | ||
| Theorem | sswfaxreg 45004* | A subclass of the class of well-founded sets models the Axiom of Regularity ax-reg 9632. Lemma II.2.4(2) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ (𝑀 ⊆ ∪ (𝑅1 “ On) → ∀𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 𝑦 ∈ 𝑥 → ∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))) | ||
| Theorem | omssaxinf2 45005* | A class that contains all ordinals up to and including ω models the Axiom of Infinity ax-inf2 9681. The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf 9678. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ ((ω ⊆ 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))) | ||
| Theorem | omelaxinf2 45006* |
A transitive class that contains ω models the
Axiom of Infinity
ax-inf2 9681. Lemma II.2.11(7) of [Kunen2] p. 114. Kunen has the
additional hypotheses that the Extensionality, Separation, Pairing, and
Union axioms are true in 𝑀. This, apparently, is because
Kunen's
statement of the Axiom of Infinity uses the defined notions ∅ and
suc, and these axioms guarantee that these
notions are
well-defined. When we state the axiom using primitives only, the need
for these hypotheses disappears.
The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf 9678. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ ((Tr 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))) | ||
| Theorem | dfac5prim 45007* | dfac5 10169 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ (CHOICE ↔ ∀𝑥((∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤 𝑤 ∈ 𝑧) ∧ ∀𝑧∀𝑤((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤∀𝑣((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))) | ||
| Theorem | ac8prim 45008* | ac8 10532 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ ((∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤 𝑤 ∈ 𝑧) ∧ ∀𝑧∀𝑤((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤∀𝑣((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))) | ||
| Theorem | modelac8prim 45009* |
If 𝑀 is a transitive class, then the
following are equivalent. (1)
Every nonempty set 𝑥 ∈ 𝑀 of pairwise disjoint nonempty sets
has a
choice set in 𝑀. (2) The class 𝑀 models
the Axiom of Choice,
in the form ac8prim 45008.
Lemma II.2.11(7) of [Kunen2] p. 114. Kunen has the additional hypotheses that the Extensionality, Separation, Pairing, and Union axioms are true in 𝑀. This, apparently, is because Kunen's statement of the Axiom of Choice uses defined notions, including ∅ and ∩, and these axioms guarantee that these notions are well-defined. When we state the axiom using primitives only, the need for these hypotheses disappears. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ (Tr 𝑀 → (∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))) | ||
| Theorem | wfaxext 45010* |
The class of well-founded sets models the Axiom of Extensionality
ax-ext 2708. Part of Corollary II.2.5 of [Kunen2] p. 112.
This is the first of a series of theorems showing that all the axioms of ZFC hold in the class of well-founded sets, which we here denote by 𝑊. More precisely, for each axiom of ZFC, we obtain a provable statement if we restrict all quantifiers to 𝑊 (including implicit universal quantifiers on free variables). None of these proofs use the Axiom of Regularity. In particular, the Axiom of Regularity itself is proved to hold in 𝑊 without using Regularity. Further, the Axiom of Choice is used only in the proof that Choice holds in 𝑊. This has the consequence that any theorem of ZF (possibly proved using Regularity) can be proved, without using Regularity, to hold in 𝑊. This gives us a relative consistency result: If ZF without Regularity is consistent, so is ZF itself. Similarly, if ZFC without Regularity is consistent, so is ZFC itself. These consistency results are metatheorems and are part of Theorem II.2.13 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 11-Sep-2025.) (Revised by Eric Schmidt, 29-Sep-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 (∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) | ||
| Theorem | wfaxrep 45011* | The class of well-founded sets models the Axiom of Replacement ax-rep 5279. Actually, our statement is stronger, since it is an instance of Replacement only when all quantifiers in ∀𝑦𝜑 are relativized to 𝑊. Essentially part of Corollary II.2.5 of [Kunen2] p. 112, but note that our Replacement is different from Kunen's. (Contributed by Eric Schmidt, 29-Sep-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∀𝑥 ∈ 𝑊 (∀𝑤 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑊 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) | ||
| Theorem | wfaxsep 45012* | The class of well-founded sets models the Axiom of Separation ax-sep 5296. Actually, our statement is stronger, since it is an instance of Separation only when all quantifiers in 𝜑 are relativized to 𝑊. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 29-Sep-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∀𝑧 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑥 ∈ 𝑊 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) | ||
| Theorem | wfaxnul 45013* | The class of well-founded sets models the Null Set Axiom ax-nul 5306. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∃𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ¬ 𝑦 ∈ 𝑥 | ||
| Theorem | wfaxpow 45014* | The class of well-founded sets models the Axioms of Power Sets. Part of Corollary II.2.9 of [Kunen2] p. 113. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
| Theorem | wfaxpr 45015* | The class of well-founded sets models the Axiom of Pairing ax-pr 5432. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 29-Sep-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ∃𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
| Theorem | wfaxun 45016* | The class of well-founded sets models the Axiom of Union ax-un 7755. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∃𝑤 ∈ 𝑊 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
| Theorem | wfaxreg 45017* | The class of well-founded sets models the Axiom of Regularity ax-reg 9632. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∀𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 𝑦 ∈ 𝑥 → ∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) | ||
| Theorem | wfaxinf2 45018* | The class of well-founded sets models the Axiom of Infinity ax-inf2 9681. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∃𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))) | ||
| Theorem | wfac8prim 45019* | The class of well-founded sets 𝑊 models the Axiom of Choice. Since the previous theorems show that all the ZF axioms hold in 𝑊, we may use any statement that ZF proves is equivalent to Choice to prove this. We use ac8prim 45008. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.) |
| ⊢ 𝑊 = ∪ (𝑅1 “ On) ⇒ ⊢ ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 ∀𝑣 ∈ 𝑊 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))) | ||
| Theorem | evth2f 45020* | A version of evth2 24992 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑦𝐹 & ⊢ Ⅎ𝑥𝑋 & ⊢ Ⅎ𝑦𝑋 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑥) ≤ (𝐹‘𝑦)) | ||
| Theorem | elunif 45021* | A version of eluni 4910 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) | ||
| Theorem | rzalf 45022 | A version of rzal 4509 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥 𝐴 = ∅ ⇒ ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) | ||
| Theorem | fvelrnbf 45023 | A version of fvelrnb 6969 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) | ||
| Theorem | rfcnpre1 45024 | If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than a given extended real B is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐴 = {𝑥 ∈ 𝑋 ∣ 𝐵 < (𝐹‘𝑥)} & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐽) | ||
| Theorem | ubelsupr 45025* | If U belongs to A and U is an upper bound, then U is the sup of A. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝑈 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑈) → 𝑈 = sup(𝐴, ℝ, < )) | ||
| Theorem | fsumcnf 45026* | A finite sum of functions to complex numbers from a common topological space is continuous, without disjoint var constraint x ph. The class expression for B normally contains free variables k and x to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | mulltgt0 45027 | The product of a negative and a positive number is negative. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 · 𝐵) < 0) | ||
| Theorem | rspcegf 45028 | A version of rspcev 3622 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
| Theorem | rabexgf 45029 | A version of rabexg 5337 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | ||
| Theorem | fcnre 45030 | A function continuous with respect to the standard topology, is a real mapping. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝑇 = ∪ 𝐽 & ⊢ 𝐶 = (𝐽 Cn 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝑇⟶ℝ) | ||
| Theorem | sumsnd 45031* | A sum of a singleton is the term. The deduction version of sumsn 15782. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ (𝜑 → Ⅎ𝑘𝐵) & ⊢ Ⅎ𝑘𝜑 & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵) | ||
| Theorem | evthf 45032* | A version of evth 24991 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑦𝐹 & ⊢ Ⅎ𝑥𝑋 & ⊢ Ⅎ𝑦𝑋 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥)) | ||
| Theorem | cnfex 45033 | The class of continuous functions between two topologies is a set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V) | ||
| Theorem | fnchoice 45034* | For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) | ||
| Theorem | refsumcn 45035* | A finite sum of continuous real functions, from a common topological space, is continuous. The class expression for B normally contains free variables k and x to index it. See fsumcn 24894 for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | rfcnpre2 45036 | If 𝐹 is a continuous function with respect to the standard topology, then the preimage A of the values smaller than a given extended real 𝐵, is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐴 = {𝑥 ∈ 𝑋 ∣ (𝐹‘𝑥) < 𝐵} & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐽) | ||
| Theorem | cncmpmax 45037* | When the hypothesis for the extreme value theorem hold, then the sup of the range of the function belongs to the range, it is real and it an upper bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ 𝑇 = ∪ 𝐽 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑇 ≠ ∅) ⇒ ⊢ (𝜑 → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ∧ sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ sup(ran 𝐹, ℝ, < ))) | ||
| Theorem | rfcnpre3 45038* | If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑡𝐹 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝑇 = ∪ 𝐽 & ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ 𝐵 ≤ (𝐹‘𝑡)} & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) | ||
| Theorem | rfcnpre4 45039* | If F is a continuous function with respect to the standard topology, then the preimage A of the values less than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑡𝐹 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝑇 = ∪ 𝐽 & ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ 𝐵} & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) | ||
| Theorem | sumpair 45040* | Sum of two distinct complex values. The class expression for 𝐴 and 𝐵 normally contain free variable 𝑘 to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ (𝜑 → Ⅎ𝑘𝐷) & ⊢ (𝜑 → Ⅎ𝑘𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 + 𝐸)) | ||
| Theorem | rfcnnnub 45041* | Given a real continuous function 𝐹 defined on a compact topological space, there is always a positive integer that is a strict upper bound of its range. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑡𝐹 & ⊢ Ⅎ𝑡𝜑 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ 𝑇 = ∪ 𝐽 & ⊢ (𝜑 → 𝑇 ≠ ∅) & ⊢ 𝐶 = (𝐽 Cn 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐶) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛) | ||
| Theorem | refsum2cnlem1 45042* | This is the core Lemma for refsum2cn 45043: the sum of two continuous real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐺 & ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐴 = (𝑘 ∈ {1, 2} ↦ if(𝑘 = 1, 𝐹, 𝐺)) & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | refsum2cn 45043* | The sum of two continuus real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐺 & ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | adantlllr 45044 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
| Theorem | 3adantlr3 45045 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜂)) ∧ 𝜃) → 𝜏) | ||
| Theorem | 3adantll2 45046 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜂 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
| Theorem | 3adantll3 45047 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
| Theorem | ssnel 45048 | If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵) → ¬ 𝐶 ∈ 𝐴) | ||
| Theorem | sncldre 45049 | A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝐴 ∈ ℝ → {𝐴} ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | n0p 45050 | A polynomial with a nonzero coefficient is not the zero polynomial. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| ⊢ ((𝑃 ∈ (Poly‘ℤ) ∧ 𝑁 ∈ ℕ0 ∧ ((coeff‘𝑃)‘𝑁) ≠ 0) → 𝑃 ≠ 0𝑝) | ||
| Theorem | pm2.65ni 45051 | Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| ⊢ (¬ 𝜑 → 𝜓) & ⊢ (¬ 𝜑 → ¬ 𝜓) ⇒ ⊢ 𝜑 | ||
| Theorem | iuneq2df 45052 | Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | ||
| Theorem | nnfoctb 45053* | There exists a mapping from ℕ onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto→𝐴) | ||
| Theorem | elpwinss 45054 | An element of the powerset of 𝐵 intersected with anything, is a subset of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵) | ||
| Theorem | unidmex 45055 | If 𝐹 is a set, then ∪ dom 𝐹 is a set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ 𝑋 = ∪ dom 𝐹 ⇒ ⊢ (𝜑 → 𝑋 ∈ V) | ||
| Theorem | ndisj2 45056* | A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (¬ Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ (𝐵 ∩ 𝐶) ≠ ∅)) | ||
| Theorem | zenom 45057 | The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ℤ ≈ ω | ||
| Theorem | uzwo4 45058* | Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑗𝜓 & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ ∃𝑗 ∈ 𝑆 𝜑) → ∃𝑗 ∈ 𝑆 (𝜑 ∧ ∀𝑘 ∈ 𝑆 (𝑘 < 𝑗 → ¬ 𝜓))) | ||
| Theorem | unisn0 45059 | The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ∪ {∅} = ∅ | ||
| Theorem | ssin0 45060 | If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → (𝐶 ∩ 𝐷) = ∅) | ||
| Theorem | inabs3 45061 | Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝐶 ⊆ 𝐵 → ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ 𝐶)) | ||
| Theorem | pwpwuni 45062 | Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵)) | ||
| Theorem | disjiun2 45063* | In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶)) & ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐸) ⇒ ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ 𝐸) = ∅) | ||
| Theorem | 0pwfi 45064 | The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin) | ||
| Theorem | ssinss2d 45065 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
| Theorem | zct 45066 | The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ℤ ≼ ω | ||
| Theorem | pwfin0 45067 | A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝒫 𝐴 ∩ Fin) ≠ ∅ | ||
| Theorem | uzct 45068 | An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ 𝑍 ≼ ω | ||
| Theorem | iunxsnf 45069* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 | ||
| Theorem | fiiuncl 45070* | If a set is closed under the union of two sets, then it is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (𝑦 ∪ 𝑧) ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷) | ||
| Theorem | iunp1 45071* | The addition of the next set to a union indexed by a finite set of sequential integers. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑘𝐵 & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 = (∪ 𝑘 ∈ (𝑀...𝑁)𝐴 ∪ 𝐵)) | ||
| Theorem | fiunicl 45072* | If a set is closed under the union of two sets, then it is closed under finite union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∪ 𝑦) ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴) | ||
| Theorem | ixpeq2d 45073 | Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
| Theorem | disjxp1 45074* | The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 (𝐵 × 𝐶)) | ||
| Theorem | disjsnxp 45075* | The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ Disj 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) | ||
| Theorem | eliind 45076* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶) & ⊢ (𝜑 → 𝐾 ∈ 𝐵) & ⊢ (𝑥 = 𝐾 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐷) | ||
| Theorem | rspcef 45077 | Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
| Theorem | ixpssmapc 45078* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐶 ↑m 𝐴)) | ||
| Theorem | elintd 45079* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
| Theorem | ssdf 45080* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
| Theorem | brneqtrd 45081 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ (𝜑 → ¬ 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) | ||
| Theorem | ssnct 45082 | A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ (𝜑 → ¬ 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 ≼ ω) | ||
| Theorem | ssuniint 45083* | Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ∪ ∩ 𝐵) | ||
| Theorem | elintdv 45084* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
| Theorem | ssd 45085* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
| Theorem | ralimralim 45086 | Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) | ||
| Theorem | snelmap 45087 | Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → (𝐴 × {𝑥}) ∈ (𝐵 ↑m 𝐴)) ⇒ ⊢ (𝜑 → 𝑥 ∈ 𝐵) | ||
| Theorem | xrnmnfpnf 45088 | An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ -∞) ⇒ ⊢ (𝜑 → 𝐴 = +∞) | ||
| Theorem | nelrnmpt 45089* | Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝐹) | ||
| Theorem | iuneq1i 45090 | Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) Remove DV conditions. (Revised by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 | ||
| Theorem | nssrex 45091* | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
| Theorem | ssinc 45092* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁)) | ||
| Theorem | ssdec 45093* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀)) | ||
| Theorem | elixpconstg 45094* | Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)) | ||
| Theorem | iineq1d 45095* | Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶) | ||
| Theorem | metpsmet 45096 | A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) | ||
| Theorem | ixpssixp 45097 | Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) | ||
| Theorem | ballss3 45098* | A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ 𝐴) | ||
| Theorem | iunincfi 45099* | Given a sequence of increasing sets, the union of a finite subsequence, is its last element. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) = (𝐹‘𝑁)) | ||
| Theorem | nsstr 45100 | If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ ((¬ 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐶) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |