Home | Metamath
Proof Explorer Theorem List (p. 414 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28698) |
Hilbert Space Explorer
(28699-30221) |
Users' Mathboxes
(30222-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | refsum2cn 41301* | 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 41302 | 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 41303 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | 3adantlr3 41304 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜂)) ∧ 𝜃) → 𝜏) | ||
Theorem | nnxrd 41305 | A natural number is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | 3adantll2 41306 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜂 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | 3adantll3 41307 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | ssnel 41308 | If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵) → ¬ 𝐶 ∈ 𝐴) | ||
Theorem | elabrexg 41309* | Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | sncldre 41310 | 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 41311 | 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 41312 | Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (¬ 𝜑 → 𝜓) & ⊢ (¬ 𝜑 → ¬ 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | pwssfi 41313 | 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 41314 | Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | nnfoctb 41315* | There exists a mapping from ℕ onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto→𝐴) | ||
Theorem | ssinss1d 41316 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | elpwinss 41317 | An element of the powerset of 𝐵 intersected with anything, is a subset of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵) | ||
Theorem | unidmex 41318 | If 𝐹 is a set, then ∪ dom 𝐹 is a set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ 𝑋 = ∪ dom 𝐹 ⇒ ⊢ (𝜑 → 𝑋 ∈ V) | ||
Theorem | ndisj2 41319* | A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (¬ Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ (𝐵 ∩ 𝐶) ≠ ∅)) | ||
Theorem | zenom 41320 | The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ℤ ≈ ω | ||
Theorem | uzwo4 41321* | 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 41322 | The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ∪ {∅} = ∅ | ||
Theorem | ssin0 41323 | If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → (𝐶 ∩ 𝐷) = ∅) | ||
Theorem | inabs3 41324 | Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐶 ⊆ 𝐵 → ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ 𝐶)) | ||
Theorem | pwpwuni 41325 | Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵)) | ||
Theorem | disjiun2 41326* | In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶)) & ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐸) ⇒ ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ 𝐸) = ∅) | ||
Theorem | 0pwfi 41327 | The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin) | ||
Theorem | ssinss2d 41328 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | zct 41329 | The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ℤ ≼ ω | ||
Theorem | pwfin0 41330 | A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝒫 𝐴 ∩ Fin) ≠ ∅ | ||
Theorem | uzct 41331 | An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ 𝑍 ≼ ω | ||
Theorem | iunxsnf 41332* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 | ||
Theorem | fiiuncl 41333* | 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 41334* | 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 41335* | 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 41336 | Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | disjxp1 41337* | 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 41338* | The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Disj 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) | ||
Theorem | eliind 41339* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶) & ⊢ (𝜑 → 𝐾 ∈ 𝐵) & ⊢ (𝑥 = 𝐾 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐷) | ||
Theorem | rspcef 41340 | Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | inn0f 41341 | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | ixpssmapc 41342* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐶 ↑m 𝐴)) | ||
Theorem | inn0 41343* | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | elintd 41344* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
Theorem | ssdf 41345* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | brneqtrd 41346 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → ¬ 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) | ||
Theorem | ssnct 41347 | A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → ¬ 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 ≼ ω) | ||
Theorem | ssuniint 41348* | Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ∪ ∩ 𝐵) | ||
Theorem | elintdv 41349* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
Theorem | ssd 41350* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ralimralim 41351 | Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) | ||
Theorem | snelmap 41352 | Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → (𝐴 × {𝑥}) ∈ (𝐵 ↑m 𝐴)) ⇒ ⊢ (𝜑 → 𝑥 ∈ 𝐵) | ||
Theorem | xrnmnfpnf 41353 | An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ -∞) ⇒ ⊢ (𝜑 → 𝐴 = +∞) | ||
Theorem | nelrnmpt 41354* | Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝐹) | ||
Theorem | snn0d 41355 | The singleton of a set is not empty. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → {𝐴} ≠ ∅) | ||
Theorem | iuneq1i 41356* | Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 | ||
Theorem | nssrex 41357* | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | iunssf 41358 | Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | ssinc 41359* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁)) | ||
Theorem | ssdec 41360* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀)) | ||
Theorem | elixpconstg 41361* | Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)) | ||
Theorem | iineq1d 41362* | Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | metpsmet 41363 | A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) | ||
Theorem | ixpssixp 41364 | Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ballss3 41365* | A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ 𝐴) | ||
Theorem | iunincfi 41366* | 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 41367 | If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((¬ 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐶) | ||
Theorem | rexanuz3 41368* | Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜒) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) & ⊢ (𝑘 = 𝑗 → (𝜒 ↔ 𝜃)) & ⊢ (𝑘 = 𝑗 → (𝜓 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝜃 ∧ 𝜏)) | ||
Theorem | cbvmpo2 41369* | Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑤𝐴 & ⊢ Ⅎ𝑤𝐶 & ⊢ Ⅎ𝑦𝐸 & ⊢ (𝑦 = 𝑤 → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | cbvmpo1 41370* | Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑧𝐵 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑥𝐸 & ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | eliuniin 41371* | Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ⇒ ⊢ (𝑍 ∈ 𝑉 → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) | ||
Theorem | ssabf 41372 | Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | pssnssi 41373 | A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 ⊊ 𝐵 ⇒ ⊢ ¬ 𝐵 ⊆ 𝐴 | ||
Theorem | rabidim2 41374 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝜑) | ||
Theorem | eluni2f 41375* | Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) | ||
Theorem | eliin2f 41376* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) | ||
Theorem | nssd 41377 | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 ⊆ 𝐵) | ||
Theorem | iineq12dv 41378* | Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | supxrcld 41379 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | elrestd 41380 | A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐽 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ 𝐴 = (𝑋 ∩ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐵)) | ||
Theorem | eliuniincex 41381* | Counterexample to show that the additional conditions in eliuniin 41371 and eliuniin2 41392 are actually needed. Notice that the definition of 𝐴 is not even needed (it can be any class). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐵 = {∅} & ⊢ 𝐶 = ∅ & ⊢ 𝐷 = ∅ & ⊢ 𝑍 = V ⇒ ⊢ ¬ (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) | ||
Theorem | eliincex 41382* | Counterexample to show that the additional conditions in eliin 4927 and eliin2 41388 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = V & ⊢ 𝐵 = ∅ ⇒ ⊢ ¬ (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) | ||
Theorem | eliinid 41383* | Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶) | ||
Theorem | abssf 41384 | Class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) | ||
Theorem | fexd 41385 | If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | supxrubd 41386 | A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ 𝑆 = sup(𝐴, ℝ*, < ) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝑆) | ||
Theorem | ssrabf 41387 | Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | eliin2 41388* | Membership in indexed intersection. See eliincex 41382 for a counterexample showing that the precondition 𝐵 ≠ ∅ cannot be simply dropped. eliin 4927 uses an alternative precondition (and it doesn't have a disjoint var constraint between 𝐵 and 𝑥; see eliin2f 41376). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) | ||
Theorem | ssrab2f 41389 | Subclass relation for a restricted class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | restuni3 41390 | The underlying set of a subspace induced by the subspace operator ↾t. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = (∪ 𝐴 ∩ 𝐵)) | ||
Theorem | rabssf 41391 | Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) | ||
Theorem | eliuniin2 41392* | Indexed union of indexed intersections. See eliincex 41382 for a counterexample showing that the precondition 𝐶 ≠ ∅ cannot be simply dropped. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ⇒ ⊢ (𝐶 ≠ ∅ → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) | ||
Theorem | restuni4 41393 | The underlying set of a subspace induced by the ↾t operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝐴) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = 𝐵) | ||
Theorem | restuni6 41394 | The underlying set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = (∪ 𝐴 ∩ 𝐵)) | ||
Theorem | restuni5 41395 | The underlying set of a subspace induced by the ↾t operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | ||
Theorem | unirestss 41396 | The union of an elementwise intersection is a subset of the underlying set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) ⊆ ∪ 𝐴) | ||
Theorem | iniin1 41397* | Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ≠ ∅ → (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵) = ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵)) | ||
Theorem | iniin2 41398* | Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ≠ ∅ → (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶) = ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶)) | ||
Theorem | cbvrabv2 41399* | A more general version of cbvrabv 3494. Usage of this theorem is discouraged because it depends on ax-13 2389. Use of cbvrabv2w 41400 is preferred. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvrabv2w 41400* | A more general version of cbvrabv 3494. Version of cbvrabv2 41399 with a disjoint variable condition, which does not require ax-13 2389. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Revised by Gino Giotto, 16-Apr-2024.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |