Home | Metamath
Proof Explorer Theorem List (p. 398 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 | itgpowd 39701* | 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 39702 | 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 39703* | 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 39704 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂)))) | ||
Theorem | ifpan23 39705 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏))) | ||
Theorem | ifpdfor2 39706 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓)) | ||
Theorem | ifporcor 39707 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑)) | ||
Theorem | ifpdfan2 39708 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑)) | ||
Theorem | ifpancor 39709 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓)) | ||
Theorem | ifpdfor 39710 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓)) | ||
Theorem | ifpdfan 39711 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥)) | ||
Theorem | ifpbi2 39712 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃))) | ||
Theorem | ifpbi3 39713 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓))) | ||
Theorem | ifpim1 39714 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓)) | ||
Theorem | ifpnot 39715 | Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤)) | ||
Theorem | ifpid2 39716 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥)) | ||
Theorem | ifpim2 39717 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑)) | ||
Theorem | ifpbi23 39718 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃))) | ||
Theorem | ifpdfbi 39719 | Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) | ||
Theorem | ifpbiidcor 39720 | Restatement of biid 262. (Contributed by RP, 25-Apr-2020.) |
⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
Theorem | ifpbicor 39721 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | ifpxorcor 39722 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑)) | ||
Theorem | ifpbi1 39723 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃))) | ||
Theorem | ifpnot23 39724 | Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
Theorem | ifpnotnotb 39725 | Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpnorcor 39726 | Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnancor 39727 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓)) | ||
Theorem | ifpnot23b 39728 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒)) | ||
Theorem | ifpbiidcor2 39729 | Restatement of biid 262. (Contributed by RP, 25-Apr-2020.) |
⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑) | ||
Theorem | ifpnot23c 39730 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒)) | ||
Theorem | ifpnot23d 39731 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpdfnan 39732 | Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤)) | ||
Theorem | ifpdfxor 39733 | Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓)) | ||
Theorem | ifpbi12 39734 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏))) | ||
Theorem | ifpbi13 39735 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜏, 𝜒) ↔ if-(𝜓, 𝜏, 𝜃))) | ||
Theorem | ifpbi123 39736 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜂))) | ||
Theorem | ifpidg 39737 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑 ∧ 𝜓) → 𝜃) ∧ ((𝜑 ∧ 𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑 ∨ 𝜃)) ∧ (𝜃 → (𝜑 ∨ 𝜒))))) | ||
Theorem | ifpid3g 39738 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜒 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝜓))) | ||
Theorem | ifpid2g 39739 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜓 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜓 → (𝜑 ∨ 𝜒)) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpid1g 39740 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜒 → 𝜑) ∧ (𝜑 → 𝜓))) | ||
Theorem | ifpim23g 39741 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (((𝜑 → 𝜓) ↔ if-(𝜒, 𝜓, ¬ 𝜑)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpim3 39742 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnim1 39743 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑)) | ||
Theorem | ifpim4 39744 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnim2 39745 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜓, ¬ 𝜓, 𝜑)) | ||
Theorem | ifpim123g 39746 | 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 39747 | Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)))) | ||
Theorem | ifp1bi 39748 | Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))))) | ||
Theorem | ifpbi1b 39749 | When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜒, 𝜒) ↔ if-(𝜓, 𝜒, 𝜒)) | ||
Theorem | ifpimimb 39750 | Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpororb 39751 | Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpananb 39752 | Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpnannanb 39753 | Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpor123g 39754 | Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂))))) | ||
Theorem | ifpimim 39755 | Consequnce of implication. (Contributed by RP, 17-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpbibib 39756 | Factor conditional logic operator over biimplication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜃 ↔ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ↔ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpxorxorb 39757 | Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ⊻ 𝜒), (𝜃 ⊻ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊻ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | rp-fakeimass 39758 | A special case where implication appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.) |
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) | ||
Theorem | rp-fakeanorass 39759 | 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 39760 | 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 39761 | 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 39762 | 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 39763* | 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 39764* | 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 39765* | 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 39766* | There is only one empty set. (Contributed by RP, 1-Oct-2023.) |
⊢ (∀𝑥 ¬ 𝑥 ∈ ∅ ∧ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | epelon2 39767 | 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 7485. This is a weak form of epelg 5460 which only requires that we know 𝐵 to be a set. (Contributed by RP, 27-Sep-2023.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | ontric3g 39768* | 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 39769* | 𝐴 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 39770 | A singleton is equinumerous to ordinal one iff its content is a set. (Contributed by RP, 8-Oct-2023.) |
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ V) | ||
Theorem | snen1el 39771 | A singleton is equinumerous to ordinal one if its content is an element of it. (Contributed by RP, 8-Oct-2023.) |
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ {𝐴}) | ||
Theorem | sn1dom 39772 | A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023.) |
⊢ {𝐴} ≼ 1o | ||
Theorem | pr2dom 39773 | An unordered pair is dominated by ordinal two. (Contributed by RP, 29-Oct-2023.) |
⊢ {𝐴, 𝐵} ≼ 2o | ||
Theorem | tr3dom 39774 | An unordered triple is dominated by ordinal three. (Contributed by RP, 29-Oct-2023.) |
⊢ {𝐴, 𝐵, 𝐶} ≼ 3o | ||
Theorem | ensucne0 39775 | 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 39776 | 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 39777 | Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 8701 when both are natural numbers. (Originally by NM, 17-Jun-1998.) (Contributed by RP, 5-Nov-2023.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | dfom6 39778 | Let ω be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.) |
⊢ ω = ∪ (On ∩ Fin) | ||
Theorem | infordmin 39779 | ω is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.) |
⊢ ∀𝑥 ∈ (On ∖ Fin)ω ⊆ 𝑥 | ||
Theorem | iscard4 39780 | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ ran card) | ||
Theorem | iscard5 39781* | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴)) | ||
Theorem | elrncard 39782* | 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 39783 | The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.) |
⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴) | ||
Theorem | harval3 39784* | (har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.) |
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | harval3on 39785* | 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 39786* | A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.) |
⊢ (𝐴 ≈ 2o ↔ ∃𝑥∃𝑦(𝐴 = {𝑥, 𝑦} ∧ 𝑥 ≠ 𝑦)) | ||
Theorem | pr2cv 39787 | If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | pr2el1 39788 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ {𝐴, 𝐵}) | ||
Theorem | pr2cv1 39789 | If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ V) | ||
Theorem | pr2el2 39790 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ {𝐴, 𝐵}) | ||
Theorem | pr2cv2 39791 | If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ V) | ||
Theorem | pren2 39792 | An unordered pair is equinumerous to ordinal two iff both parts are sets not equal to each other. (Contributed by RP, 8-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | pr2eldif1 39793 | If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ ({𝐴, 𝐵} ∖ {𝐵})) | ||
Theorem | pr2eldif2 39794 | If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ ({𝐴, 𝐵} ∖ {𝐴})) | ||
Theorem | pren2d 39795 | A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) | ||
Theorem | aleph1min 39796 | (ℵ‘1o) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023.) |
⊢ (ℵ‘1o) = ∩ {𝑥 ∈ On ∣ ω ≺ 𝑥} | ||
Theorem | alephiso2 39797 | ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.) |
⊢ ℵ Isom E , ≺ (On, {𝑥 ∈ ran card ∣ ω ⊆ 𝑥}) | ||
Theorem | alephiso3 39798 | ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.) |
⊢ ℵ Isom E , ≺ (On, (ran card ∖ ω)) | ||
Theorem | pwelg 39799* | 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 39800* | 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))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |