Home | Metamath
Proof Explorer Theorem List (p. 369 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 | isdomn3 36801 | Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈ (SubMnd‘𝑈))) | ||
Theorem | mon1pid 36802 | Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → ( 1 ∈ 𝑀 ∧ (𝐷‘ 1 ) = 0)) | ||
Theorem | mon1psubm 36803 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑃) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑀 ∈ (SubMnd‘𝑈)) | ||
Theorem | deg1mhm 36804 | Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑌 = ((mulGrp‘𝑃) ↾s (𝐵 ∖ { 0 })) & ⊢ 𝑁 = (ℂfld ↾s ℕ0) ⇒ ⊢ (𝑅 ∈ Domn → (𝐷 ↾ (𝐵 ∖ { 0 })) ∈ (𝑌 MndHom 𝑁)) | ||
Theorem | cytpfn 36805 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ CytP Fn ℕ | ||
Theorem | cytpval 36806* | Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝑇 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ 𝑂 = (od‘𝑇) & ⊢ 𝑃 = (Poly1‘ℂfld) & ⊢ 𝑋 = (var1‘ℂfld) & ⊢ 𝑄 = (mulGrp‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ (𝑁 ∈ ℕ → (CytP‘𝑁) = (𝑄 Σg (𝑟 ∈ (◡𝑂 “ {𝑁}) ↦ (𝑋 − (𝐴‘𝑟))))) | ||
Theorem | fgraphopab 36807* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)}) | ||
Theorem | fgraphxp 36808* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {𝑥 ∈ (𝐴 × 𝐵) ∣ (𝐹‘(1st ‘𝑥)) = (2nd ‘𝑥)}) | ||
Theorem | hausgraph 36809 | The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×t 𝐾))) | ||
Syntax | ctopsep 36810 | The class of separable toplogies. |
class TopSep | ||
Syntax | ctoplnd 36811 | The class of Lindelöf toplogies. |
class TopLnd | ||
Definition | df-topsep 36812* | A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
⊢ TopSep = {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 ∪ 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = ∪ 𝑗)} | ||
Definition | df-toplnd 36813* | A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
⊢ TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))} | ||
Theorem | ioounsn 36814 | The closure of the upper end of an open real interval. (Contributed by Jon Pennant, 8-Jun-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵)) | ||
Theorem | iocunico 36815 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶)) | ||
Theorem | iocinico 36816 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝐵}) | ||
Theorem | iocmbl 36817 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ∈ dom vol) | ||
Theorem | cnioobibld 36818* | A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider 𝐹 = (𝑥 ∈ (0(,)1) ↦ (1 / 𝑥)). See cniccibl 23413 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐿1) | ||
Theorem | itgpowd 36819* | The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥 = (((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1))) / (𝑁 + 1))) | ||
Theorem | arearect 36820 | The area of a rectangle whose sides are parallel to the coordinate axes in (ℝ × ℝ) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐷 ∈ ℝ & ⊢ 𝐴 ≤ 𝐵 & ⊢ 𝐶 ≤ 𝐷 & ⊢ 𝑆 = ((𝐴[,]𝐵) × (𝐶[,]𝐷)) ⇒ ⊢ (area‘𝑆) = ((𝐵 − 𝐴) · (𝐷 − 𝐶)) | ||
Theorem | areaquad 36821* | The area of a quadrilateral with two sides which are parallel to the y-axis in (ℝ × ℝ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐷 ∈ ℝ & ⊢ 𝐸 ∈ ℝ & ⊢ 𝐹 ∈ ℝ & ⊢ 𝐴 < 𝐵 & ⊢ 𝐶 ≤ 𝐸 & ⊢ 𝐷 ≤ 𝐹 & ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) & ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⇒ ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴)) | ||
Theorem | ifpan123g 36822 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂)))) | ||
Theorem | ifpan23 36823 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏))) | ||
Theorem | ifpdfor2 36824 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓)) | ||
Theorem | ifporcor 36825 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑)) | ||
Theorem | ifpdfan2 36826 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑)) | ||
Theorem | ifpancor 36827 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓)) | ||
Theorem | ifpdfor 36828 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓)) | ||
Theorem | ifpdfan 36829 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥)) | ||
Theorem | ifpbi2 36830 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃))) | ||
Theorem | ifpbi3 36831 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓))) | ||
Theorem | ifpim1 36832 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓)) | ||
Theorem | ifpnot 36833 | Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤)) | ||
Theorem | ifpid2 36834 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥)) | ||
Theorem | ifpim2 36835 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑)) | ||
Theorem | ifpbi23 36836 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃))) | ||
Theorem | ifpdfbi 36837 | Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) | ||
Theorem | ifpbiidcor 36838 | Restatement of biid 250. (Contributed by RP, 25-Apr-2020.) |
⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
Theorem | ifpbicor 36839 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | ifpxorcor 36840 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑)) | ||
Theorem | ifpbi1 36841 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃))) | ||
Theorem | ifpnot23 36842 | Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
Theorem | ifpnotnotb 36843 | Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpnorcor 36844 | Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnancor 36845 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓)) | ||
Theorem | ifpnot23b 36846 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒)) | ||
Theorem | ifpbiidcor2 36847 | Restatement of biid 250. (Contributed by RP, 25-Apr-2020.) |
⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑) | ||
Theorem | ifpnot23c 36848 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒)) | ||
Theorem | ifpnot23d 36849 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpdfnan 36850 | Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤)) | ||
Theorem | ifpdfxor 36851 | Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓)) | ||
Theorem | ifpbi12 36852 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏))) | ||
Theorem | ifpbi13 36853 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜏, 𝜒) ↔ if-(𝜓, 𝜏, 𝜃))) | ||
Theorem | ifpbi123 36854 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜂))) | ||
Theorem | ifpidg 36855 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑 ∧ 𝜓) → 𝜃) ∧ ((𝜑 ∧ 𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑 ∨ 𝜃)) ∧ (𝜃 → (𝜑 ∨ 𝜒))))) | ||
Theorem | ifpid3g 36856 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜒 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝜓))) | ||
Theorem | ifpid2g 36857 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜓 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜓 → (𝜑 ∨ 𝜒)) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpid1g 36858 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜒 → 𝜑) ∧ (𝜑 → 𝜓))) | ||
Theorem | ifpim23g 36859 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (((𝜑 → 𝜓) ↔ if-(𝜒, 𝜓, ¬ 𝜑)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpim3 36860 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnim1 36861 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑)) | ||
Theorem | ifpim4 36862 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnim2 36863 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜓, ¬ 𝜓, 𝜑)) | ||
Theorem | ifpim123g 36864 | Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂))))) | ||
Theorem | ifpim1g 36865 | Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)))) | ||
Theorem | ifp1bi 36866 | Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))))) | ||
Theorem | ifpbi1b 36867 | When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜒, 𝜒) ↔ if-(𝜓, 𝜒, 𝜒)) | ||
Theorem | ifpimimb 36868 | Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpororb 36869 | Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpananb 36870 | Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpnannanb 36871 | Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpor123g 36872 | Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂))))) | ||
Theorem | ifpimim 36873 | Consequnce of implication. (Contributed by RP, 17-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpbibib 36874 | Factor conditional logic operator over biimplication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜃 ↔ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ↔ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpxorxorb 36875 | Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ⊻ 𝜒), (𝜃 ⊻ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊻ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | rp-fakeimass 36876 | A special case where implication appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.) |
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) | ||
Theorem | rp-fakeanorass 36877 | A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.) |
⊢ ((𝜒 → 𝜑) ↔ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒)))) | ||
Theorem | rp-fakeoranass 36878 | A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.) |
⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))) | ||
Theorem | rp-fakenanass 36879 | A special case where nand appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.) |
⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))) | ||
Theorem | rp-fakeinunass 36880 | A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.) |
⊢ (𝐶 ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ∪ 𝐶) = (𝐴 ∩ (𝐵 ∪ 𝐶))) | ||
Theorem | rp-fakeuninass 36881 | A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.) |
⊢ (𝐴 ⊆ 𝐶 ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐴 ∪ (𝐵 ∩ 𝐶))) | ||
Membership in the class of finite sets can be expressed in many ways. | ||
Theorem | rp-isfinite5 36882* | A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some 𝑛 ∈ ℕ0. (Contributed by Richard Penner, 3-Mar-2020.) |
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ℕ0 (1...𝑛) ≈ 𝐴) | ||
Theorem | rp-isfinite6 36883* | A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some 𝑛 ∈ ℕ. (Contributed by Richard Penner, 10-Mar-2020.) |
⊢ (𝐴 ∈ Fin ↔ (𝐴 = ∅ ∨ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴)) | ||
Theorem | pwelg 36884* | The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.) |
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵)) | ||
Theorem | pwinfig 36885* | The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝐵 is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.) |
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ (𝐵 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝐵 ∖ Fin))) | ||
Theorem | pwinfi2 36886 | The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑈 is a weak universe. (Contributed by RP, 21-Mar-2020.) |
⊢ (𝑈 ∈ WUni → (𝐴 ∈ (𝑈 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑈 ∖ Fin))) | ||
Theorem | pwinfi3 36887 | The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑇 is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.) |
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → (𝐴 ∈ (𝑇 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑇 ∖ Fin))) | ||
Theorem | pwinfi 36888 | The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.) |
⊢ (𝐴 ∈ (V ∖ Fin) ↔ 𝒫 𝐴 ∈ (V ∖ Fin)) | ||
While there is not yet a definition, the finite intersection property of a class is introduced by fiint 8122 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 5671, ordelinel 5742 ), chains of sets ordered by the proper subset relation (sorpssin 6843), various sets in the field of topology (inopn 20529, incld 20657, innei 20739, ... ) and "universal" classes like weak universes (wunin 9414, tskin 9460) and the class of all sets (inex1g 4729) . | ||
Theorem | fipjust 36889* | A definition of the finite intersection property of a class based on closure under pair-wise intersection of its elements is independent of the dummy variables. (Contributed by Richard Penner, 1-Jan-2020.) |
⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 ∩ 𝑣) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴) | ||
Theorem | cllem0 36890* | The class of all sets with property 𝜑(𝑧) is closed under the binary operation on sets defined in 𝑅(𝑥, 𝑦). (Contributed by Richard Penner, 3-Jan-2020.) |
⊢ 𝑉 = {𝑧 ∣ 𝜑} & ⊢ 𝑅 ∈ 𝑈 & ⊢ (𝑧 = 𝑅 → (𝜑 ↔ 𝜓)) & ⊢ (𝑧 = 𝑥 → (𝜑 ↔ 𝜒)) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ ((𝜒 ∧ 𝜃) → 𝜓) ⇒ ⊢ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑅 ∈ 𝑉 | ||
Theorem | superficl 36891* | The class of all supersets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 | ||
Theorem | superuncl 36892* | The class of all supersets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
Theorem | ssficl 36893* | The class of all subsets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 | ||
Theorem | ssuncl 36894* | The class of all subsets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
Theorem | ssdifcl 36895* | The class of all subsets of a class is closed under class difference. (Contributed by Richard Penner, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴 | ||
Theorem | sssymdifcl 36896* | The class of all subsets of a class is closed under symmetric difference. (Contributed by Richard Penner, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴 | ||
Theorem | fiinfi 36897* | If two classes have the finite intersection property, then so does their intersection. (Contributed by Richard Penner, 1-Jan-2020.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶) | ||
Theorem | rababg 36898 | Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.) |
⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) | ||
Theorem | elintabg 36899* | Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | ||
Theorem | elinintab 36900* | Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∈ (𝐵 ∩ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |