Home | Metamath
Proof Explorer Theorem List (p. 413 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 0pwfi 41201 | The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin) | ||
Theorem | ssinss2d 41202 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | zct 41203 | The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ℤ ≼ ω | ||
Theorem | pwfin0 41204 | A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝒫 𝐴 ∩ Fin) ≠ ∅ | ||
Theorem | uzct 41205 | An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ 𝑍 ≼ ω | ||
Theorem | iunxsnf 41206* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 | ||
Theorem | fiiuncl 41207* | 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 41208* | 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 41209* | 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 41210 | Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | disjxp1 41211* | 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 41212* | The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Disj 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) | ||
Theorem | eliind 41213* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶) & ⊢ (𝜑 → 𝐾 ∈ 𝐵) & ⊢ (𝑥 = 𝐾 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐷) | ||
Theorem | rspcef 41214 | Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | inn0f 41215 | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | ixpssmapc 41216* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐶 ↑m 𝐴)) | ||
Theorem | inn0 41217* | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | elintd 41218* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
Theorem | ssdf 41219* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | brneqtrd 41220 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → ¬ 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) | ||
Theorem | ssnct 41221 | A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → ¬ 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 ≼ ω) | ||
Theorem | ssuniint 41222* | Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ∪ ∩ 𝐵) | ||
Theorem | elintdv 41223* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
Theorem | ssd 41224* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ralimralim 41225 | Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) | ||
Theorem | snelmap 41226 | Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → (𝐴 × {𝑥}) ∈ (𝐵 ↑m 𝐴)) ⇒ ⊢ (𝜑 → 𝑥 ∈ 𝐵) | ||
Theorem | xrnmnfpnf 41227 | An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ -∞) ⇒ ⊢ (𝜑 → 𝐴 = +∞) | ||
Theorem | nelrnmpt 41228* | Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝐹) | ||
Theorem | snn0d 41229 | The singleton of a set is not empty. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → {𝐴} ≠ ∅) | ||
Theorem | iuneq1i 41230* | Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 | ||
Theorem | nssrex 41231* | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | iunssf 41232 | Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | ssinc 41233* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁)) | ||
Theorem | ssdec 41234* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀)) | ||
Theorem | elixpconstg 41235* | Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)) | ||
Theorem | iineq1d 41236* | Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | metpsmet 41237 | A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) | ||
Theorem | ixpssixp 41238 | Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ballss3 41239* | A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ 𝐴) | ||
Theorem | iunincfi 41240* | 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 41241 | If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((¬ 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐶) | ||
Theorem | rexanuz3 41242* | Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜒) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) & ⊢ (𝑘 = 𝑗 → (𝜒 ↔ 𝜃)) & ⊢ (𝑘 = 𝑗 → (𝜓 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝜃 ∧ 𝜏)) | ||
Theorem | cbvmpo2 41243* | Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑤𝐴 & ⊢ Ⅎ𝑤𝐶 & ⊢ Ⅎ𝑦𝐸 & ⊢ (𝑦 = 𝑤 → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | cbvmpo1 41244* | Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑧𝐵 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑥𝐸 & ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | eliuniin 41245* | Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ⇒ ⊢ (𝑍 ∈ 𝑉 → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) | ||
Theorem | ssabf 41246 | Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | uniexd 41247 | Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ V) | ||
Theorem | pssnssi 41248 | A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 ⊊ 𝐵 ⇒ ⊢ ¬ 𝐵 ⊆ 𝐴 | ||
Theorem | rabidim2 41249 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝜑) | ||
Theorem | eluni2f 41250* | Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) | ||
Theorem | eliin2f 41251* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) | ||
Theorem | nssd 41252 | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 ⊆ 𝐵) | ||
Theorem | iineq12dv 41253* | Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | supxrcld 41254 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | elrestd 41255 | A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐽 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ 𝐴 = (𝑋 ∩ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐵)) | ||
Theorem | eliuniincex 41256* | Counterexample to show that the additional conditions in eliuniin 41245 and eliuniin2 41267 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 41257* | Counterexample to show that the additional conditions in eliin 4917 and eliin2 41263 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = V & ⊢ 𝐵 = ∅ ⇒ ⊢ ¬ (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) | ||
Theorem | eliinid 41258* | Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶) | ||
Theorem | abssf 41259 | Class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) | ||
Theorem | fexd 41260 | If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | supxrubd 41261 | 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 41262 | Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | eliin2 41263* | Membership in indexed intersection. See eliincex 41257 for a counterexample showing that the precondition 𝐵 ≠ ∅ cannot be simply dropped. eliin 4917 uses an alternative precondition (and it doesn't have a disjoint var constraint between 𝐵 and 𝑥; see eliin2f 41251). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) | ||
Theorem | ssrab2f 41264 | Subclass relation for a restricted class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | restuni3 41265 | 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 41266 | Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) | ||
Theorem | eliuniin2 41267* | Indexed union of indexed intersections. See eliincex 41257 for a counterexample showing that the precondition 𝐶 ≠ ∅ cannot be simply dropped. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ⇒ ⊢ (𝐶 ≠ ∅ → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) | ||
Theorem | restuni4 41268 | 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 41269 | The underlying set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = (∪ 𝐴 ∩ 𝐵)) | ||
Theorem | restuni5 41270 | 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 41271 | The union of an elementwise intersection is a subset of the underlying set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) ⊆ ∪ 𝐴) | ||
Theorem | iniin1 41272* | Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ≠ ∅ → (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵) = ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵)) | ||
Theorem | iniin2 41273* | Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ≠ ∅ → (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶) = ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶)) | ||
Theorem | cbvrabv2 41274* | A more general version of cbvrabv 3492. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | iinssiin 41275 | Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | eliind2 41276* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | iinssd 41277* | Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | ralrimia 41278 | Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rabbida2 41279 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | iinexd 41280* | The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵, which should be read 𝐵(𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V) | ||
Theorem | rabexf 41281 | Separation Scheme in terms of a restricted class abstraction. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V | ||
Theorem | rabbida3 41282 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | resexd 41283 | The restriction of a set is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ V) | ||
Theorem | r19.36vf 41284 | Restricted quantifier version of one direction of 19.36 2223. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | raleqd 41285 | Equality deduction for restricted universal quantifier. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | ralimda 41286 | Deduction quantifying both antecedent and consequent. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | iinssf 41287 | Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | iinssdf 41288 | Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑋 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | resabs2i 41289 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵) | ||
Theorem | ssdf2 41290 | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | rabssd 41291 | Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜒} ⊆ 𝐵) | ||
Theorem | rexnegd 41292 | Minus a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → -𝑒𝐴 = -𝐴) | ||
Theorem | rexlimd3 41293 | * Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | resabs1i 41294 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵) | ||
Theorem | nel1nelin 41295 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (¬ 𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)) | ||
Theorem | nel2nelin 41296 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (¬ 𝐴 ∈ 𝐶 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)) | ||
Theorem | nel1nelini 41297 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
Theorem | nel2nelini 41298 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ¬ 𝐴 ∈ 𝐶 ⇒ ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
Theorem | eliunid 41299* | Membership in indexed union. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | reximddv3 41300* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |