Home | Metamath
Proof Explorer Theorem List (p. 384 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 | nsstr 38301 | If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((¬ 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐶) | ||
Theorem | rabbida 38302 | Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rexanuz3 38303* | Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜒) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) & ⊢ (𝑘 = 𝑗 → (𝜒 ↔ 𝜃)) & ⊢ (𝑘 = 𝑗 → (𝜓 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝜃 ∧ 𝜏)) | ||
Theorem | rabeqd 38304* | Equality theorem for restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜒} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | cbvmpt22 38305* | Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑤𝐴 & ⊢ Ⅎ𝑤𝐶 & ⊢ Ⅎ𝑦𝐸 & ⊢ (𝑦 = 𝑤 → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | cbvmpt21 38306* | Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑧𝐵 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑥𝐸 & ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | eliuniin 38307* | Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ⇒ ⊢ (𝑍 ∈ 𝑉 → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) | ||
Theorem | ssabf 38308 | Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | rabbia2 38309 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒} | ||
Theorem | uniexd 38310 | Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ V) | ||
Theorem | pwexd 38311 | Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ∈ V) | ||
Theorem | pssnssi 38312 | A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 ⊊ 𝐵 ⇒ ⊢ ¬ 𝐵 ⊆ 𝐴 | ||
Theorem | rabidim2 38313 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝜑) | ||
Theorem | xpexd 38314 | The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) | ||
Theorem | eluni2f 38315* | Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) | ||
Theorem | eliin2f 38316* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) | ||
Theorem | nssd 38317 | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 ⊆ 𝐵) | ||
Theorem | rabidim1 38318 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) | ||
Theorem | iineq12dv 38319* | Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | rabeqif 38320 | Equality theorem for restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | supxrcld 38321 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | elrestd 38322 | A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐽 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ 𝐴 = (𝑋 ∩ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐵)) | ||
Theorem | eliuniincex 38323* | Counterexample to show that the additional conditions in eliuniin 38307 and eliuniin2 38335 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 38324* | Counterexample to show that the additional conditions in eliin 4461 and eliin2 38330 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = V & ⊢ 𝐵 = ∅ ⇒ ⊢ ¬ (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) | ||
Theorem | eliinid 38325* | Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶) | ||
Theorem | abssf 38326 | Class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) | ||
Theorem | fexd 38327 | If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | supxrubd 38328 | 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 38329 | Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | eliin2 38330* | Membership in indexed intersection. See eliincex 38324 for a counterexample showing that the precondition 𝐵 ≠ ∅ cannot be simply dropped. eliin 4461 uses an alternative precondition (and it doesn't have a disjoint var constraint between 𝐵 and 𝑥; see eliin2f 38316). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) | ||
Theorem | ssrab2f 38331 | Subclass relation for a restricted class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | rabeqi 38332* | Equality theorem for restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | restuni3 38333 | 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 38334 | Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) | ||
Theorem | eliuniin2 38335* | Indexed union of indexed intersections. See eliincex 38324 for a counterexample showing that the precondition 𝐶 ≠ ∅ cannot be simply dropped. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ⇒ ⊢ (𝐶 ≠ ∅ → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) | ||
Theorem | restuni4 38336 | 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 38337 | The underlying set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = (∪ 𝐴 ∩ 𝐵)) | ||
Theorem | restuni5 38338 | 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 38339 | The union of an elementwise intersection is a subset of the underlying set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) ⊆ ∪ 𝐴) | ||
Theorem | unima 38340 | Image of a union. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 “ (𝐵 ∪ 𝐶)) = ((𝐹 “ 𝐵) ∪ (𝐹 “ 𝐶))) | ||
Theorem | feq1dd 38341 | Equality deduction for functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) | ||
Theorem | fnresdmss 38342 | A function does not change when restricted to a set that contains its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐹 ↾ 𝐵) = 𝐹) | ||
Theorem | fmptsnxp 38343* | Maps-to notation and cross product for a singleton function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ {𝐴} ↦ 𝐵) = ({𝐴} × {𝐵})) | ||
Theorem | mptex2 38344* | If a class given as a map-to notation is a set, it's image values are set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑡 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐴) → 𝐵 ∈ 𝐶) | ||
Theorem | fvmpt2bd 38345* | Value of a function given by the "maps to" notation. Deduction version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵) | ||
Theorem | rnmptfi 38346* | The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐵 ∈ Fin → ran 𝐴 ∈ Fin) | ||
Theorem | fresin2 38347 | Restriction of a function with respect to the intersection with its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ (𝐶 ∩ 𝐴)) = (𝐹 ↾ 𝐶)) | ||
Theorem | rnmptc 38348* | Range of a constant function in map to notation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → ran 𝐹 = {𝐵}) | ||
Theorem | ffi 38349 | A function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin) | ||
Theorem | suprnmpt 38350* | An explicit bound for the range of a bounded function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐶 = sup(ran 𝐹, ℝ, < ) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | rnffi 38351 | The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ Fin) → ran 𝐹 ∈ Fin) | ||
Theorem | mptelpm 38352* | A function in maps-to notation is a partial map . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝐴 ⊆ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐶 ↑pm 𝐷)) | ||
Theorem | rnmptpr 38353* | Range of a function defined on an unordered pair. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐶) & ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ (𝜑 → ran 𝐹 = {𝐷, 𝐸}) | ||
Theorem | resmpti 38354* | Restriction of the mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐵 ⊆ 𝐴 ⇒ ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | founiiun 38355* | Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐹:𝐴–onto→𝐵 → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) | ||
Theorem | f1oeq2d 38356 | Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) | ||
Theorem | rnresun 38357 | Distribution law for range of a restriction over a union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ran (𝐹 ↾ (𝐴 ∪ 𝐵)) = (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) | ||
Theorem | f1oeq1d 38358 | Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵)) | ||
Theorem | dffo3f 38359* | An onto mapping expressed in terms of function values. As dffo3 6282 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) | ||
Theorem | rnresss 38360 | The range of a restriction is a subset of the whole range. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ran (𝐴 ↾ 𝐵) ⊆ ran 𝐴 | ||
Theorem | elrnmptd 38361* | The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐶 ∈ ran 𝐹) | ||
Theorem | elrnmptf 38362 | The range of a function in maps-to notation. Same as elrnmpt 5293, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | ||
Theorem | rnmptssrn 38363* | Inclusion relation for two ranges expressed in map-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐶 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ran (𝑦 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | disjf1 38364* | A 1 to 1 mapping built from disjoint, nonempty sets . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1→𝑉) | ||
Theorem | rnsnf 38365 | The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{𝐴}⟶𝐵) ⇒ ⊢ (𝜑 → ran 𝐹 = {(𝐹‘𝐴)}) | ||
Theorem | wessf1ornlem 38366* | Given a function 𝐹 on a well ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹) | ||
Theorem | wessf1orn 38367* | Given a function 𝐹 on a well ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 We 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹) | ||
Theorem | foelrnf 38368* | Property of a surjective function. As foelrn 6286 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
Theorem | nelrnres 38369 | If 𝐴 is not in the range, it is not in the range of any restriction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (¬ 𝐴 ∈ ran 𝐵 → ¬ 𝐴 ∈ ran (𝐵 ↾ 𝐶)) | ||
Theorem | disjrnmpt2 38370* | Disjointness of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran 𝐹 𝑦) | ||
Theorem | elrnmpt1sf 38371* | Elementhood in an image set. Same as elrnmpt1s 5294, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) | ||
Theorem | founiiun0 38372* | Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) | ||
Theorem | disjf1o 38373* | A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅} & ⊢ 𝐷 = (ran 𝐹 ∖ {∅}) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→𝐷) | ||
Theorem | fompt 38374* | Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = 𝐶)) | ||
Theorem | disjinfi 38375* | Only a finite number of disjoint sets can have a non empty intersection with a finite set 𝐶 (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Fin) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin) | ||
Theorem | fvovco 38376 | Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(𝑉 × 𝑊)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1st ‘(𝐹‘𝑌))𝑂(2nd ‘(𝐹‘𝑌)))) | ||
Theorem | ssnnf1octb 38377* | There exists a bijection between a subset of ℕ and a given nonempty countable set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴)) | ||
Theorem | mapdm0 38378 | The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 ∅) = {∅}) | ||
Theorem | nnf1oxpnn 38379 | There is a bijection between the set of positive integers and the Cartesian product of the set of positive integers with itself. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ∃𝑓 𝑓:ℕ–1-1-onto→(ℕ × ℕ) | ||
Theorem | rnmptssd 38380* | The range of an operation given by the "maps to" notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | projf1o 38381* | A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈𝐴, 𝑥〉) ⇒ ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→({𝐴} × 𝐵)) | ||
Theorem | fvmap 38382 | Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑𝑚 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐴) | ||
Theorem | mapsnd 38383* | The value of set exponentiation with a singleton exponent. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ↑𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}}) | ||
Theorem | fvixp2 38384* | Projection of a factor of an indexed Cartesian product. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | ||
Theorem | fidmfisupp 38385 | A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐹:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | mapsnend 38386 | Set exponentiation to a singleton exponent is equinumerous to its base. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ↑𝑚 {𝐵}) ≈ 𝐴) | ||
Theorem | choicefi 38387* | For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) | ||
Theorem | mpct 38388 | The exponentiation of a countable set to a finite set is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐴 ↑𝑚 𝐵) ≼ ω) | ||
Theorem | cnmetcoval 38389 | Value of the distance function of the metric space of complex numbers, composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝐷 = (abs ∘ − ) & ⊢ (𝜑 → 𝐹:𝐴⟶(ℂ × ℂ)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝐷 ∘ 𝐹)‘𝐵) = (abs‘((1st ‘(𝐹‘𝐵)) − (2nd ‘(𝐹‘𝐵))))) | ||
Theorem | fcomptss 38390* | Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑥)))) | ||
Theorem | elmapsnd 38391 | Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹 Fn {𝐴}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑𝑚 {𝐴})) | ||
Theorem | mapss2 38392 | Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶))) | ||
Theorem | fsneq 38393 | Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐵 = {𝐴} & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐺 Fn 𝐵) ⇒ ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) = (𝐺‘𝐴))) | ||
Theorem | difmap 38394 | Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → ((𝐴 ∖ 𝐵) ↑𝑚 𝐶) ⊆ ((𝐴 ↑𝑚 𝐶) ∖ (𝐵 ↑𝑚 𝐶))) | ||
Theorem | unirnmap 38395 | Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑𝑚 𝐴)) ⇒ ⊢ (𝜑 → 𝑋 ⊆ (ran ∪ 𝑋 ↑𝑚 𝐴)) | ||
Theorem | inmap 38396 | Intersection of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ((𝐴 ↑𝑚 𝐶) ∩ (𝐵 ↑𝑚 𝐶)) = ((𝐴 ∩ 𝐵) ↑𝑚 𝐶)) | ||
Theorem | fcoss 38397 | Composition of two mappings. Similar to fco 5971, but with a weaker condition on the domain of 𝐹. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐺:𝐷⟶𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐷⟶𝐵) | ||
Theorem | fsneqrn 38398 | Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐵 = {𝐴} & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐺 Fn 𝐵) ⇒ ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) ∈ ran 𝐺)) | ||
Theorem | difmapsn 38399 | Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ((𝐴 ↑𝑚 {𝐶}) ∖ (𝐵 ↑𝑚 {𝐶})) = ((𝐴 ∖ 𝐵) ↑𝑚 {𝐶})) | ||
Theorem | mapssbi 38400 | Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |