Home | Metamath
Proof Explorer Theorem List (p. 383 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rfcnpre1 38201 | 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 38202* | 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 38203* | 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 38204 | The product of a negative and a positive number is negative. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 · 𝐵) < 0) | ||
Theorem | rspcegf 38205 | A version of rspcev 3282 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | rabexgf 38206 | A version of rabexg 4739 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | ||
Theorem | fcnre 38207 | 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 38208* | A sum of a singleton is the term. The deduction version of sumsn 14319. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ (𝜑 → Ⅎ𝑘𝐵) & ⊢ Ⅎ𝑘𝜑 & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵) | ||
Theorem | evthf 38209* | A version of evth 22566 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑦𝐹 & ⊢ Ⅎ𝑥𝑋 & ⊢ Ⅎ𝑦𝑋 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥)) | ||
Theorem | cnfex 38210 | The class of continuous functions between two topologies is a set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V) | ||
Theorem | fnchoice 38211* | 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 38212* | 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 22481 for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | rfcnpre2 38213 | 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 38214* | 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 38215* | If F is a continuous function with respect to the standard topology, then the preimage A of the values greater or equal than a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑡𝐹 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝑇 = ∪ 𝐽 & ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ 𝐵 ≤ (𝐹‘𝑡)} & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | rfcnpre4 38216* | If F is a continuous function with respect to the standard topology, then the preimage A of the values smaller or equal than a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑡𝐹 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝑇 = ∪ 𝐽 & ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ 𝐵} & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | sumpair 38217* | 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 38218* | 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 38219* | This is the core Lemma for refsum2cn 38220: 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 38220* | 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 | elunnel2 38221 | A member of a union that is not a member of the second class, is a member of the first class. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ (𝐵 ∪ 𝐶) ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ 𝐵) | ||
Theorem | adantlllr 38222 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | 3adantlr3 38223 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜂)) ∧ 𝜃) → 𝜏) | ||
Theorem | nnxrd 38224 | A natural number is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | 3adantll2 38225 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜂 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | 3adantll3 38226 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | ssnel 38227 | If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵) → ¬ 𝐶 ∈ 𝐴) | ||
Theorem | jcn 38228 | Inference joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → 𝜒)) | ||
Theorem | elabrexg 38229* | Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | unicntop 38230 | The underlying set of the standard topology on the complex numers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ℂ = ∪ (TopOpen‘ℂfld) | ||
Theorem | ifeq123d 38231 | Equality deduction for conditional operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.) AV: This theorem already exists as ifbieq12d 4063. TODO (NM): Please replace the usage of this theorem by ifbieq12d 4063 then delete this theorem. (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐷)) | ||
Theorem | sncldre 38232 | A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → {𝐴} ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | cnopn 38233 | The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ℂ ∈ (TopOpen‘ℂfld) | ||
Theorem | n0p 38234 | 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 38235 | Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (¬ 𝜑 → 𝜓) & ⊢ (¬ 𝜑 → ¬ 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | pwssfi 38236 | Every element of the power set of 𝐴 is finite if and only if 𝐴 is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ 𝒫 𝐴 ⊆ Fin)) | ||
Theorem | iuneq2df 38237 | Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | nnfoctb 38238* | There exists a mapping from ℕ onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto→𝐴) | ||
Theorem | ssinss1d 38239 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | 0un 38240 | The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (∅ ∪ 𝐴) = 𝐴 | ||
Theorem | elpwinss 38241 | An element of the powerset of 𝐵 intersected with anything, is a subset of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵) | ||
Theorem | unidmex 38242 | If 𝐹 is a set, then ∪ dom 𝐹 is a set (common case). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ 𝑋 = ∪ dom 𝐹 ⇒ ⊢ (𝜑 → 𝑋 ∈ V) | ||
Theorem | ndisj2 38243* | A non disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (¬ Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ (𝐵 ∩ 𝐶) ≠ ∅)) | ||
Theorem | zenom 38244 | The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ℤ ≈ ω | ||
Theorem | rexsngf 38245* | Restricted existential quantification over a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | uzwo4 38246* | 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 38247 | The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ∪ {∅} = ∅ | ||
Theorem | ssin0 38248 | If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → (𝐶 ∩ 𝐷) = ∅) | ||
Theorem | inabs3 38249 | Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐶 ⊆ 𝐵 → ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ 𝐶)) | ||
Theorem | pwpwuni 38250 | Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵)) | ||
Theorem | disjiun2 38251* | In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶)) & ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐸) ⇒ ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ 𝐸) = ∅) | ||
Theorem | 0pwfi 38252 | The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin) | ||
Theorem | ssinss2d 38253 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | zct 38254 | The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ℤ ≼ ω | ||
Theorem | iunxsngf2 38255* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) | ||
Theorem | pwfin0 38256 | A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝒫 𝐴 ∩ Fin) ≠ ∅ | ||
Theorem | uzct 38257 | An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ 𝑍 ≼ ω | ||
Theorem | iunxsnf 38258* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 | ||
Theorem | fiiuncl 38259* | 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 38260* | 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 38261* | 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 38262 | Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | disjxp1 38263* | 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 | elpwd 38264 | Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | disjsnxp 38265* | The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Disj 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) | ||
Theorem | eliind 38266* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶) & ⊢ (𝜑 → 𝐾 ∈ 𝐵) & ⊢ (𝑥 = 𝐾 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐷) | ||
Theorem | rspcef 38267 | Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | inn0f 38268 | A non-empty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | ixpssmapc 38269* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐶 ↑𝑚 𝐴)) | ||
Theorem | inn0 38270* | A non-empty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | elintd 38271* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
Theorem | eqneltri 38272 | If a class is not an element of another class, an equal class is also not an element. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ 𝐴 = 𝐵 & ⊢ ¬ 𝐵 ∈ 𝐶 ⇒ ⊢ ¬ 𝐴 ∈ 𝐶 | ||
Theorem | ssdf 38273* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | brneqtrd 38274 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → ¬ 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) | ||
Theorem | ssnct 38275 | A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → ¬ 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 ≼ ω) | ||
Theorem | ssuniint 38276* | Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ∪ ∩ 𝐵) | ||
Theorem | elintdv 38277* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
Theorem | ssd 38278* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ralimralim 38279 | Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) | ||
Theorem | snelmap 38280 | Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → (𝐴 × {𝑥}) ∈ (𝐵 ↑𝑚 𝐴)) ⇒ ⊢ (𝜑 → 𝑥 ∈ 𝐵) | ||
Theorem | dfcleqf 38281 | Equality connective between classes. Same as dfcleq 2604, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | xrnmnfpnf 38282 | An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ -∞) ⇒ ⊢ (𝜑 → 𝐴 = +∞) | ||
Theorem | nelrnmpt 38283* | Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝐹) | ||
Theorem | snn0d 38284 | The singleton of a set is not empty. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → {𝐴} ≠ ∅) | ||
Theorem | rabid3 38285 | Membership in a restricted abstraction (special case). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) | ||
Theorem | iuneq1i 38286* | Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 | ||
Theorem | nssrex 38287* | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | nelpr2 38288 | If a class is not an element of an unordered pair, it is not the second listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | nelpr1 38289 | If a class is not an element of an unordered pair, it is not the first listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | iunssf 38290 | Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | elpwi2 38291 | Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝐵 ∈ 𝑉 & ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ 𝐴 ∈ 𝒫 𝐵 | ||
Theorem | ssinc 38292* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁)) | ||
Theorem | ssdec 38293* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀)) | ||
Theorem | elixpconstg 38294* | Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)) | ||
Theorem | iineq1d 38295* | Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | metpsmet 38296 | A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) | ||
Theorem | ixpssixp 38297 | Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ballss3 38298* | A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ 𝐴) | ||
Theorem | iunssd 38299* | Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | iunincfi 38300* | Given a sequence of increasing sets, the union of a finite subsequence, is its last element. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) = (𝐹‘𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |