Home | Metamath
Proof Explorer Theorem List (p. 399 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cytpfn 39801 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ CytP Fn ℕ | ||
Theorem | cytpval 39802* | 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 39803* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)}) | ||
Theorem | fgraphxp 39804* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {𝑥 ∈ (𝐴 × 𝐵) ∣ (𝐹‘(1st ‘𝑥)) = (2nd ‘𝑥)}) | ||
Theorem | hausgraph 39805 | 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 39806 | The class of separable toplogies. |
class TopSep | ||
Syntax | ctoplnd 39807 | The class of Lindelöf toplogies. |
class TopLnd | ||
Definition | df-topsep 39808* | 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 39809* | A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
⊢ TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))} | ||
Theorem | iocunico 39810 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶)) | ||
Theorem | iocinico 39811 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝐵}) | ||
Theorem | iocmbl 39812 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ∈ dom vol) | ||
Theorem | cnioobibld 39813* | 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 24435 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐿1) | ||
Theorem | itgpowd 39814* | 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 39815 | 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 39816* | 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 39817 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂)))) | ||
Theorem | ifpan23 39818 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏))) | ||
Theorem | ifpdfor2 39819 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓)) | ||
Theorem | ifporcor 39820 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑)) | ||
Theorem | ifpdfan2 39821 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑)) | ||
Theorem | ifpancor 39822 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓)) | ||
Theorem | ifpdfor 39823 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓)) | ||
Theorem | ifpdfan 39824 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥)) | ||
Theorem | ifpbi2 39825 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃))) | ||
Theorem | ifpbi3 39826 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓))) | ||
Theorem | ifpim1 39827 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓)) | ||
Theorem | ifpnot 39828 | Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤)) | ||
Theorem | ifpid2 39829 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥)) | ||
Theorem | ifpim2 39830 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑)) | ||
Theorem | ifpbi23 39831 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃))) | ||
Theorem | ifpdfbi 39832 | Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) | ||
Theorem | ifpbiidcor 39833 | Restatement of biid 263. (Contributed by RP, 25-Apr-2020.) |
⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
Theorem | ifpbicor 39834 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | ifpxorcor 39835 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑)) | ||
Theorem | ifpbi1 39836 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃))) | ||
Theorem | ifpnot23 39837 | Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
Theorem | ifpnotnotb 39838 | Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpnorcor 39839 | Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnancor 39840 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓)) | ||
Theorem | ifpnot23b 39841 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒)) | ||
Theorem | ifpbiidcor2 39842 | Restatement of biid 263. (Contributed by RP, 25-Apr-2020.) |
⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑) | ||
Theorem | ifpnot23c 39843 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒)) | ||
Theorem | ifpnot23d 39844 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpdfnan 39845 | Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤)) | ||
Theorem | ifpdfxor 39846 | Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓)) | ||
Theorem | ifpbi12 39847 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏))) | ||
Theorem | ifpbi13 39848 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜏, 𝜒) ↔ if-(𝜓, 𝜏, 𝜃))) | ||
Theorem | ifpbi123 39849 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜂))) | ||
Theorem | ifpidg 39850 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑 ∧ 𝜓) → 𝜃) ∧ ((𝜑 ∧ 𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑 ∨ 𝜃)) ∧ (𝜃 → (𝜑 ∨ 𝜒))))) | ||
Theorem | ifpid3g 39851 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜒 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝜓))) | ||
Theorem | ifpid2g 39852 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜓 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜓 → (𝜑 ∨ 𝜒)) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpid1g 39853 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜒 → 𝜑) ∧ (𝜑 → 𝜓))) | ||
Theorem | ifpim23g 39854 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (((𝜑 → 𝜓) ↔ if-(𝜒, 𝜓, ¬ 𝜑)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpim3 39855 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnim1 39856 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑)) | ||
Theorem | ifpim4 39857 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnim2 39858 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜓, ¬ 𝜓, 𝜑)) | ||
Theorem | ifpim123g 39859 | 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 39860 | Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)))) | ||
Theorem | ifp1bi 39861 | Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))))) | ||
Theorem | ifpbi1b 39862 | When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜒, 𝜒) ↔ if-(𝜓, 𝜒, 𝜒)) | ||
Theorem | ifpimimb 39863 | Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpororb 39864 | Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpananb 39865 | Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpnannanb 39866 | Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpor123g 39867 | Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂))))) | ||
Theorem | ifpimim 39868 | Consequnce of implication. (Contributed by RP, 17-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpbibib 39869 | Factor conditional logic operator over biimplication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜃 ↔ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ↔ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpxorxorb 39870 | Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ⊻ 𝜒), (𝜃 ⊻ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊻ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | rp-fakeimass 39871 | A special case where implication appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.) |
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) | ||
Theorem | rp-fakeanorass 39872 | A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020.) |
⊢ ((𝜒 → 𝜑) ↔ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒)))) | ||
Theorem | rp-fakeoranass 39873 | A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.) |
⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))) | ||
Theorem | rp-fakeinunass 39874 | A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020.) |
⊢ (𝐶 ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ∪ 𝐶) = (𝐴 ∩ (𝐵 ∪ 𝐶))) | ||
Theorem | rp-fakeuninass 39875 | A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.) |
⊢ (𝐴 ⊆ 𝐶 ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐴 ∪ (𝐵 ∩ 𝐶))) | ||
Membership in the class of finite sets can be expressed in many ways. | ||
Theorem | rp-isfinite5 39876* | 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 RP, 3-Mar-2020.) |
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ℕ0 (1...𝑛) ≈ 𝐴) | ||
Theorem | rp-isfinite6 39877* | 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 RP, 10-Mar-2020.) |
⊢ (𝐴 ∈ Fin ↔ (𝐴 = ∅ ∨ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴)) | ||
Theorem | intabssd 39878* | When for each element 𝑦 there is a subset 𝐴 which may substituted for 𝑥 such that 𝑦 satisfying 𝜒 implies 𝑥 satisfies 𝜓 then the intersection of all 𝑥 that satisfy 𝜓 is a subclass the intersection of all 𝑦 that satisfy 𝜒. (Contributed by RP, 17-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑦) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ 𝜓} ⊆ ∩ {𝑦 ∣ 𝜒}) | ||
Theorem | eu0 39879* | There is only one empty set. (Contributed by RP, 1-Oct-2023.) |
⊢ (∀𝑥 ¬ 𝑥 ∈ ∅ ∧ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | epelon2 39880 | Over the ordinal numbers, one may define the relation 𝐴 E 𝐵 iff 𝐴 ∈ 𝐵 and one finds that, under this ordering, On is a well-ordered class, see epweon 7491. This is a weak form of epelg 5461 which only requires that we know 𝐵 to be a set. (Contributed by RP, 27-Sep-2023.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | ontric3g 39881* | For all 𝑥, 𝑦 ∈ On, one and only one of the following hold: 𝑥 ∈ 𝑦, 𝑦 = 𝑥, or 𝑦 ∈ 𝑥. This is a transparent strict trichotomy. (Contributed by RP, 27-Sep-2023.) |
⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On ((𝑥 ∈ 𝑦 ↔ ¬ (𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 = 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 ∈ 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥))) | ||
Theorem | dfsucon 39882* | 𝐴 is called a successor ordinal if it is not a limit ordinal and not the empty set. (Contributed by RP, 11-Nov-2023.) |
⊢ ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ∃𝑥 ∈ On 𝐴 = suc 𝑥) | ||
Theorem | snen1g 39883 | A singleton is equinumerous to ordinal one iff its content is a set. (Contributed by RP, 8-Oct-2023.) |
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ V) | ||
Theorem | snen1el 39884 | A singleton is equinumerous to ordinal one if its content is an element of it. (Contributed by RP, 8-Oct-2023.) |
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ {𝐴}) | ||
Theorem | sn1dom 39885 | A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023.) |
⊢ {𝐴} ≼ 1o | ||
Theorem | pr2dom 39886 | An unordered pair is dominated by ordinal two. (Contributed by RP, 29-Oct-2023.) |
⊢ {𝐴, 𝐵} ≼ 2o | ||
Theorem | tr3dom 39887 | An unordered triple is dominated by ordinal three. (Contributed by RP, 29-Oct-2023.) |
⊢ {𝐴, 𝐵, 𝐶} ≼ 3o | ||
Theorem | ensucne0 39888 | A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof shortened by SN, 16-Nov-2023.) |
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅) | ||
Theorem | ensucne0OLD 39889 | A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅) | ||
Theorem | nndomog 39890 | Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 8706 when both are natural numbers. (Originally by NM, 17-Jun-1998.) (Contributed by RP, 5-Nov-2023.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | dfom6 39891 | Let ω be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.) |
⊢ ω = ∪ (On ∩ Fin) | ||
Theorem | infordmin 39892 | ω is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.) |
⊢ ∀𝑥 ∈ (On ∖ Fin)ω ⊆ 𝑥 | ||
Theorem | iscard4 39893 | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ ran card) | ||
Theorem | iscard5 39894* | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴)) | ||
Theorem | elrncard 39895* | Let us define a cardinal number to be an element 𝐴 ∈ On such that 𝐴 is not equipotent with any 𝑥 ∈ 𝐴. (Contributed by RP, 1-Oct-2023.) |
⊢ (𝐴 ∈ ran card ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴)) | ||
Theorem | harsucnn 39896 | The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.) |
⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴) | ||
Theorem | harval3 39897* | (har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.) |
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | harval3on 39898* | For any ordinal number 𝐴 let (har‘𝐴) denote the least cardinal that is greater than 𝐴; (Contributed by RP, 4-Nov-2023.) |
⊢ (𝐴 ∈ On → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | en2pr 39899* | A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.) |
⊢ (𝐴 ≈ 2o ↔ ∃𝑥∃𝑦(𝐴 = {𝑥, 𝑦} ∧ 𝑥 ≠ 𝑦)) | ||
Theorem | pr2cv 39900 | If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |