Home | Metamath
Proof Explorer Theorem List (p. 445 of 460) | < 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-28845) |
Hilbert Space Explorer
(28846-30368) |
Users' Mathboxes
(30369-45946) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iccpartf 44401 | The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 43189 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → 𝑃:(0...𝑀)⟶((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccpartel 44402 | If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ (0...𝑀)) → (𝑃‘𝐼) ∈ ((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccelpart 44403* | An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) | ||
Theorem | iccpartiun 44404* | A half-open interval of extended reals is the union of the parts of its partition. (Contributed by AV, 18-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ((𝑃‘0)[,)(𝑃‘𝑀)) = ∪ 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) | ||
Theorem | icceuelpartlem 44405 | Lemma for icceuelpart 44406. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (𝐼 < 𝐽 → (𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽)))) | ||
Theorem | icceuelpart 44406* | An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ ((𝑃‘0)[,)(𝑃‘𝑀))) → ∃!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) | ||
Theorem | iccpartdisj 44407* | The segments of a partitioned half-open interval of extended reals are a disjoint collection. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → Disj 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) | ||
Theorem | iccpartnel 44408 | A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 43186 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 8-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑃) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑃‘𝐼)(,)(𝑃‘(𝐼 + 1)))) | ||
Theorem | fargshiftfv 44409* | If a class is a function, then the values of the "shifted function" correspond to the function values of the class. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (𝑋 ∈ (0..^𝑁) → (𝐺‘𝑋) = (𝐹‘(𝑋 + 1)))) | ||
Theorem | fargshiftf 44410* | If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → 𝐺:(0..^(♯‘𝐹))⟶dom 𝐸) | ||
Theorem | fargshiftf1 44411* | If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–1-1→dom 𝐸) → 𝐺:(0..^(♯‘𝐹))–1-1→dom 𝐸) | ||
Theorem | fargshiftfo 44412* | If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–onto→dom 𝐸) → 𝐺:(0..^(♯‘𝐹))–onto→dom 𝐸) | ||
Theorem | fargshiftfva 44413* | The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (∀𝑘 ∈ (1...𝑁)(𝐸‘(𝐹‘𝑘)) = ⦋𝑘 / 𝑥⦌𝑃 → ∀𝑙 ∈ (0..^𝑁)(𝐸‘(𝐺‘𝑙)) = ⦋(𝑙 + 1) / 𝑥⦌𝑃)) | ||
Theorem | lswn0 44414 | The last symbol of a not empty word exists. The empty set must be excluded as symbol, because otherwise, it cannot be distinguished between valid cases (∅ is the last symbol) and invalid cases (∅ means that no last symbol exists. This is because of the special definition of a function in set.mm. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∅ ∉ 𝑉 ∧ (♯‘𝑊) ≠ 0) → (lastS‘𝑊) ≠ ∅) | ||
Syntax | wich 44415 | Extend wff notation to include the propery of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. Read this notation as "𝑥 and 𝑦 are interchangeable in wff 𝜑". |
wff [𝑥⇄𝑦]𝜑 | ||
Definition | df-ich 44416* | Define the property of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. For an alternate definition using implicit substitution and a temporary setvar variable see ichcircshi 44424. Another, equivalent definition using two temporary setvar variables is provided in dfich2 44428. (Contributed by AV, 29-Jul-2023.) |
⊢ ([𝑥⇄𝑦]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)) | ||
Theorem | nfich1 44417 | The first interchangeable setvar variable is not free. (Contributed by AV, 21-Aug-2023.) |
⊢ Ⅎ𝑥[𝑥⇄𝑦]𝜑 | ||
Theorem | nfich2 44418 | The second interchangeable setvar variable is not free. (Contributed by AV, 21-Aug-2023.) |
⊢ Ⅎ𝑦[𝑥⇄𝑦]𝜑 | ||
Theorem | ichv 44419* | Setvar variables are interchangeable in a wff they do not appear in. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichf 44420 | Setvar variables are interchangeable in a wff they are not free in. (Contributed by SN, 23-Nov-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichid 44421 | A setvar variable is always interchangeable with itself. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑥]𝜑 | ||
Theorem | icht 44422 | A theorem is interchangeable. (Contributed by SN, 4-May-2024.) |
⊢ 𝜑 ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichbidv 44423* | Formula building rule for interchangeability (deduction). (Contributed by SN, 4-May-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑥⇄𝑦]𝜓 ↔ [𝑥⇄𝑦]𝜒)) | ||
Theorem | ichcircshi 44424* | The setvar variables are interchangeable if they can be circularily shifted using a third setvar variable, using implicit substitution. (Contributed by AV, 29-Jul-2023.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜑)) ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichan 44425 | If two setvar variables are interchangeable in two wffs, then they are interchangeable in the conjunction of these two wffs. Notice that the reverse implication is not necessarily true. Corresponding theorems will hold for other commutative operations, too. (Contributed by AV, 31-Jul-2023.) Use df-ich 44416 instead of dfich2 44428 to reduce axioms. (Revised by SN, 4-May-2024.) |
⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 ∧ 𝜓)) | ||
Theorem | ichn 44426 | Negation does not affect interchangeability. (Contributed by SN, 30-Aug-2023.) |
⊢ ([𝑎⇄𝑏]𝜑 ↔ [𝑎⇄𝑏] ¬ 𝜑) | ||
Theorem | ichim 44427 | Formula building rule for implication in interchangeability. (Contributed by SN, 4-May-2024.) |
⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 → 𝜓)) | ||
Theorem | dfich2 44428* | Alternate definition of the propery of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. (Contributed by AV and WL, 6-Aug-2023.) |
⊢ ([𝑥⇄𝑦]𝜑 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)) | ||
Theorem | ichcom 44429* | The interchangeability of setvar variables is commutative. (Contributed by AV, 20-Aug-2023.) |
⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑦⇄𝑥]𝜓) | ||
Theorem | ichbi12i 44430* | Equivalence for interchangeable setvar variables. (Contributed by AV, 29-Jul-2023.) |
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒) | ||
Theorem | icheqid 44431 | In an equality for the same setvar variable, the setvar variable is interchangeable by itself. Special case of ichid 44421 and icheq 44432 without distinct variables restriction. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑥]𝑥 = 𝑥 | ||
Theorem | icheq 44432* | In an equality of setvar variables, the setvar variables are interchangeable. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑦]𝑥 = 𝑦 | ||
Theorem | ichnfimlem 44433* | Lemma for ichnfim 44434: A substitution for a nonfree variable has no effect. (Contributed by Wolf Lammen, 6-Aug-2023.) Avoid ax-13 2371. (Revised by Gino Giotto, 1-May-2024.) |
⊢ (∀𝑦Ⅎ𝑥𝜑 → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)) | ||
Theorem | ichnfim 44434* | If in an interchangeability context 𝑥 is not free in 𝜑, the same holds for 𝑦. (Contributed by Wolf Lammen, 6-Aug-2023.) (Revised by AV, 23-Sep-2023.) |
⊢ ((∀𝑦Ⅎ𝑥𝜑 ∧ [𝑥⇄𝑦]𝜑) → ∀𝑥Ⅎ𝑦𝜑) | ||
Theorem | ichnfb 44435* | If 𝑥 and 𝑦 are interchangeable in 𝜑, they are both free or both not free in 𝜑. (Contributed by Wolf Lammen, 6-Aug-2023.) (Revised by AV, 23-Sep-2023.) |
⊢ ([𝑥⇄𝑦]𝜑 → (∀𝑥Ⅎ𝑦𝜑 ↔ ∀𝑦Ⅎ𝑥𝜑)) | ||
Theorem | ichal 44436* | Move a universal quantifier inside interchangeability. (Contributed by SN, 30-Aug-2023.) |
⊢ (∀𝑥[𝑎⇄𝑏]𝜑 → [𝑎⇄𝑏]∀𝑥𝜑) | ||
Theorem | ich2al 44437 | Two setvar variables are always interchangeable when there are two universal quantifiers. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]∀𝑥∀𝑦𝜑 | ||
Theorem | ich2ex 44438 | Two setvar variables are always interchangeable when there are two existential quantifiers. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]∃𝑥∃𝑦𝜑 | ||
Theorem | ichexmpl1 44439* | Example for interchangeable setvar variables in a statement of predicate calculus with equality. (Contributed by AV, 31-Jul-2023.) |
⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) | ||
Theorem | ichexmpl2 44440* | Example for interchangeable setvar variables in an arithmetic expression. (Contributed by AV, 31-Jul-2023.) |
⊢ [𝑎⇄𝑏]((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝑎↑2) + (𝑏↑2)) = (𝑐↑2)) | ||
Theorem | ich2exprop 44441* | If the setvar variables are interchangeable in a wff, there is an ordered pair fulfilling the wff iff there is an unordered pair fulfilling the wff. (Contributed by AV, 16-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [𝑎⇄𝑏]𝜑) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏(〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝜑))) | ||
Theorem | ichnreuop 44442* | If the setvar variables are interchangeable in a wff, there is never a unique ordered pair with different components fulfilling the wff (because if 〈𝑎, 𝑏〉 fulfils the wff, then also 〈𝑏, 𝑎〉 fulfils the wff). (Contributed by AV, 27-Aug-2023.) |
⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)) | ||
Theorem | ichreuopeq 44443* | If the setvar variables are interchangeable in a wff, and there is a unique ordered pair fulfilling the wff, then both setvar variables must be equal. (Contributed by AV, 28-Aug-2023.) |
⊢ ([𝑎⇄𝑏]𝜑 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜑) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑))) | ||
Theorem | sprid 44444 | Two identical representations of the class of all unordered pairs. (Contributed by AV, 21-Nov-2021.) |
⊢ {𝑝 ∣ ∃𝑎 ∈ V ∃𝑏 ∈ V 𝑝 = {𝑎, 𝑏}} = {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} | ||
Theorem | elsprel 44445* | An unordered pair is an element of all unordered pairs. At least one of the two elements of the unordered pair must be a set. Otherwise, the unordered pair would be the empty set, see prprc 4655, which is not an element of all unordered pairs, see spr0nelg 44446. (Contributed by AV, 21-Nov-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | spr0nelg 44446* | The empty set is not an element of all unordered pairs. (Contributed by AV, 21-Nov-2021.) |
⊢ ∅ ∉ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} | ||
Syntax | cspr 44447 | Extend class notation with set of pairs. |
class Pairs | ||
Definition | df-spr 44448* | Define the function which maps a set 𝑣 to the set of pairs consisting of elements of the set 𝑣. (Contributed by AV, 21-Nov-2021.) |
⊢ Pairs = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | sprval 44449* | The set of all unordered pairs over a given set 𝑉. (Contributed by AV, 21-Nov-2021.) |
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | sprvalpw 44450* | The set of all unordered pairs over a given set 𝑉, expressed by a restricted class abstraction. (Contributed by AV, 21-Nov-2021.) |
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | sprssspr 44451* | The set of all unordered pairs over a given set 𝑉 is a subset of the set of all unordered pairs. (Contributed by AV, 21-Nov-2021.) |
⊢ (Pairs‘𝑉) ⊆ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} | ||
Theorem | spr0el 44452 | The empty set is not an unordered pair over any set 𝑉. (Contributed by AV, 21-Nov-2021.) |
⊢ ∅ ∉ (Pairs‘𝑉) | ||
Theorem | sprvalpwn0 44453* | The set of all unordered pairs over a given set 𝑉, expressed by a restricted class abstraction. (Contributed by AV, 21-Nov-2021.) |
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | sprel 44454* | An element of the set of all unordered pairs over a given set 𝑉 is a pair of elements of the set 𝑉. (Contributed by AV, 22-Nov-2021.) |
⊢ (𝑋 ∈ (Pairs‘𝑉) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑋 = {𝑎, 𝑏}) | ||
Theorem | prssspr 44455* | An element of a subset of the set of all unordered pairs over a given set 𝑉, is a pair of elements of the set 𝑉. (Contributed by AV, 22-Nov-2021.) |
⊢ ((𝑃 ⊆ (Pairs‘𝑉) ∧ 𝑋 ∈ 𝑃) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑋 = {𝑎, 𝑏}) | ||
Theorem | prelspr 44456 | An unordered pair of elements of a fixed set 𝑉 belongs to the set of all unordered pairs over the set 𝑉. (Contributed by AV, 21-Nov-2021.) |
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → {𝑋, 𝑌} ∈ (Pairs‘𝑉)) | ||
Theorem | prsprel 44457 | The elements of a pair from the set of all unordered pairs over a given set 𝑉 are elements of the set 𝑉. (Contributed by AV, 22-Nov-2021.) |
⊢ (({𝑋, 𝑌} ∈ (Pairs‘𝑉) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) | ||
Theorem | prsssprel 44458 | The elements of a pair from a subset of the set of all unordered pairs over a given set 𝑉 are elements of the set 𝑉. (Contributed by AV, 21-Nov-2021.) |
⊢ ((𝑃 ⊆ (Pairs‘𝑉) ∧ {𝑋, 𝑌} ∈ 𝑃 ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) | ||
Theorem | sprvalpwle2 44459* | The set of all unordered pairs over a given set 𝑉, expressed by a restricted class abstraction. (Contributed by AV, 24-Nov-2021.) |
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑝) ≤ 2}) | ||
Theorem | sprsymrelfvlem 44460* | Lemma for sprsymrelf 44465 and sprsymrelfv 44464. (Contributed by AV, 19-Nov-2021.) |
⊢ (𝑃 ⊆ (Pairs‘𝑉) → {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑃 𝑐 = {𝑥, 𝑦}} ∈ 𝒫 (𝑉 × 𝑉)) | ||
Theorem | sprsymrelf1lem 44461* | Lemma for sprsymrelf1 44466. (Contributed by AV, 22-Nov-2021.) |
⊢ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎 ⊆ 𝑏)) | ||
Theorem | sprsymrelfolem1 44462* | Lemma 1 for sprsymrelfo 44467. (Contributed by AV, 22-Nov-2021.) |
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)} ⇒ ⊢ 𝑄 ∈ 𝒫 (Pairs‘𝑉) | ||
Theorem | sprsymrelfolem2 44463* | Lemma 2 for sprsymrelfo 44467. (Contributed by AV, 23-Nov-2021.) |
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)) → (𝑥𝑅𝑦 ↔ ∃𝑐 ∈ 𝑄 𝑐 = {𝑥, 𝑦})) | ||
Theorem | sprsymrelfv 44464* | The value of the function 𝐹 which maps a subset of the set of pairs over a fixed set 𝑉 to the relation relating two elements of the set 𝑉 iff they are in a pair of the subset. (Contributed by AV, 19-Nov-2021.) |
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) & ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}) ⇒ ⊢ (𝑋 ∈ 𝑃 → (𝐹‘𝑋) = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑋 𝑐 = {𝑥, 𝑦}}) | ||
Theorem | sprsymrelf 44465* | The mapping 𝐹 is a function from the subsets of the set of pairs over a fixed set 𝑉 into the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 19-Nov-2021.) |
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) & ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}) ⇒ ⊢ 𝐹:𝑃⟶𝑅 | ||
Theorem | sprsymrelf1 44466* | The mapping 𝐹 is a one-to-one function from the subsets of the set of pairs over a fixed set 𝑉 into the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 19-Nov-2021.) |
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) & ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}) ⇒ ⊢ 𝐹:𝑃–1-1→𝑅 | ||
Theorem | sprsymrelfo 44467* | The mapping 𝐹 is a function from the subsets of the set of pairs over a fixed set 𝑉 onto the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 23-Nov-2021.) |
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) & ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}) ⇒ ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝑃–onto→𝑅) | ||
Theorem | sprsymrelf1o 44468* | The mapping 𝐹 is a bijection between the subsets of the set of pairs over a fixed set 𝑉 into the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 23-Nov-2021.) |
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) & ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}) ⇒ ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝑃–1-1-onto→𝑅) | ||
Theorem | sprbisymrel 44469* | There is a bijection between the subsets of the set of pairs over a fixed set 𝑉 and the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 23-Nov-2021.) |
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) & ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} ⇒ ⊢ (𝑉 ∈ 𝑊 → ∃𝑓 𝑓:𝑃–1-1-onto→𝑅) | ||
Theorem | sprsymrelen 44470* | The class 𝑃 of subsets of the set of pairs over a fixed set 𝑉 and the class 𝑅 of symmetric relations on the fixed set 𝑉 are equinumerous. (Contributed by AV, 27-Nov-2021.) |
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) & ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} ⇒ ⊢ (𝑉 ∈ 𝑊 → 𝑃 ≈ 𝑅) | ||
Proper (unordered) pairs are unordered pairs with exactly 2 elements. The set of proper pairs with elements of a class 𝑉 is defined by {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}. For example, {1, 2} is a proper pair, because 1 ≠ 2 ( see 1ne2 11917). Examples for not proper unordered pairs are {1, 1} = {1} (see preqsn 4744), {1, V} = {1} (see prprc2 4654) or {V, V} = ∅ (see prprc 4655). | ||
Theorem | prpair 44471* | Characterization of a proper pair: A class is a proper pair iff it consists of exactly two different sets. (Contributed by AV, 11-Mar-2023.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (𝑋 ∈ 𝑃 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) | ||
Theorem | prproropf1olem0 44472 | Lemma 0 for prproropf1o 44477. Remark: 𝑂, the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component, can alternatively be written as 𝑂 = {𝑥 ∈ (𝑉 × 𝑉) ∣ (1st ‘𝑥)𝑅(2nd ‘𝑥)} or even as 𝑂 = {𝑥 ∈ (𝑉 × 𝑉) ∣ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑅}, by which the relationship between ordered and unordered pair is immediately visible. (Contributed by AV, 18-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) ⇒ ⊢ (𝑊 ∈ 𝑂 ↔ (𝑊 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉 ∧ ((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) | ||
Theorem | prproropf1olem1 44473* | Lemma 1 for prproropf1o 44477. (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → {(1st ‘𝑊), (2nd ‘𝑊)} ∈ 𝑃) | ||
Theorem | prproropf1olem2 44474* | Lemma 2 for prproropf1o 44477. (Contributed by AV, 13-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃) → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ 𝑂) | ||
Theorem | prproropf1olem3 44475* | Lemma 3 for prproropf1o 44477. (Contributed by AV, 13-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉) ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → (𝐹‘{(1st ‘𝑊), (2nd ‘𝑊)}) = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) | ||
Theorem | prproropf1olem4 44476* | Lemma 4 for prproropf1o 44477. (Contributed by AV, 14-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉) ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝐹‘𝑍) = (𝐹‘𝑊) → 𝑍 = 𝑊)) | ||
Theorem | prproropf1o 44477* | There is a bijection between the set of proper pairs and the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component. (Contributed by AV, 15-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉) ⇒ ⊢ (𝑅 Or 𝑉 → 𝐹:𝑃–1-1-onto→𝑂) | ||
Theorem | prproropen 44478* | The set of proper pairs and the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component, are equinumerous. (Contributed by AV, 15-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑅 Or 𝑉) → 𝑂 ≈ 𝑃) | ||
Theorem | prproropreud 44479* | There is exactly one ordered ordered pair fulfilling a wff iff there is exactly one proper pair fulfilling an equivalent wff. (Contributed by AV, 20-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ (𝜑 → 𝑅 Or 𝑉) & ⊢ (𝑥 = 〈inf(𝑦, 𝑉, 𝑅), sup(𝑦, 𝑉, 𝑅)〉 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝑂 𝜓 ↔ ∃!𝑦 ∈ 𝑃 𝜒)) | ||
Theorem | pairreueq 44480* | Two equivalent representations of the existence of a unique proper pair. (Contributed by AV, 1-Mar-2023.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (∃!𝑝 ∈ 𝑃 𝜑 ↔ ∃!𝑝 ∈ 𝒫 𝑉((♯‘𝑝) = 2 ∧ 𝜑)) | ||
Theorem | paireqne 44481* | Two sets are not equal iff there is exactly one proper pair whose elements are either one of these sets. (Contributed by AV, 27-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (𝜑 → (∃!𝑝 ∈ 𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 ≠ 𝐵)) | ||
Syntax | cprpr 44482 | Extend class notation with set of proper unordered pairs. |
class Pairsproper | ||
Definition | df-prpr 44483* | Define the function which maps a set 𝑣 to the set of proper unordered pairs consisting of exactly two (different) elements of the set 𝑣. (Contributed by AV, 29-Apr-2023.) |
⊢ Pairsproper = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}) | ||
Theorem | prprval 44484* | The set of all proper unordered pairs over a given set 𝑉. (Contributed by AV, 29-Apr-2023.) |
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}) | ||
Theorem | prprvalpw 44485* | The set of all proper unordered pairs over a given set 𝑉, expressed by a restricted class abstraction. (Contributed by AV, 29-Apr-2023.) |
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}) | ||
Theorem | prprelb 44486 | An element of the set of all proper unordered pairs over a given set 𝑉 is a subset of 𝑉 of size two. (Contributed by AV, 29-Apr-2023.) |
⊢ (𝑉 ∈ 𝑊 → (𝑃 ∈ (Pairsproper‘𝑉) ↔ (𝑃 ∈ 𝒫 𝑉 ∧ (♯‘𝑃) = 2))) | ||
Theorem | prprelprb 44487* | A set is an element of the set of all proper unordered pairs over a given set 𝑋 iff it is a pair of different elements of the set 𝑋. (Contributed by AV, 7-May-2023.) |
⊢ (𝑃 ∈ (Pairsproper‘𝑋) ↔ (𝑋 ∈ V ∧ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑃 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏))) | ||
Theorem | prprspr2 44488* | The set of all proper unordered pairs over a given set 𝑉 is the set of all unordered pairs over that set of size two. (Contributed by AV, 29-Apr-2023.) |
⊢ (Pairsproper‘𝑉) = {𝑝 ∈ (Pairs‘𝑉) ∣ (♯‘𝑝) = 2} | ||
Theorem | prprsprreu 44489* | There is a unique proper unordered pair over a given set 𝑉 fulfilling a wff iff there is a unique unordered pair over 𝑉 of size two fulfilling this wff. (Contributed by AV, 30-Apr-2023.) |
⊢ (𝑉 ∈ 𝑊 → (∃!𝑝 ∈ (Pairsproper‘𝑉)𝜑 ↔ ∃!𝑝 ∈ (Pairs‘𝑉)((♯‘𝑝) = 2 ∧ 𝜑))) | ||
Theorem | prprreueq 44490* | There is a unique proper unordered pair over a given set 𝑉 fulfilling a wff iff there is a unique subset of 𝑉 of size two fulfilling this wff. (Contributed by AV, 29-Apr-2023.) |
⊢ (𝑉 ∈ 𝑊 → (∃!𝑝 ∈ (Pairsproper‘𝑉)𝜑 ↔ ∃!𝑝 ∈ 𝒫 𝑉((♯‘𝑝) = 2 ∧ 𝜑))) | ||
Theorem | sbcpr 44491* | The proper substitution of an unordered pair for a setvar variable corresponds to a proper substitution of each of its elements. (Contributed by AV, 7-Apr-2023.) |
⊢ (𝑝 = {𝑥, 𝑦} → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([{𝑎, 𝑏} / 𝑝]𝜑 ↔ [𝑏 / 𝑦][𝑎 / 𝑥]𝜓) | ||
Theorem | reupr 44492* | There is a unique unordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 7-Apr-2023.) |
⊢ (𝑝 = {𝑎, 𝑏} → (𝜓 ↔ 𝜒)) & ⊢ (𝑝 = {𝑥, 𝑦} → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (Pairs‘𝑋)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝜃 → {𝑥, 𝑦} = {𝑎, 𝑏})))) | ||
Theorem | reuprpr 44493* | There is a unique proper unordered pair fulfilling a wff iff there are uniquely two different sets fulfilling a corresponding wff. (Contributed by AV, 30-Apr-2023.) |
⊢ (𝑝 = {𝑎, 𝑏} → (𝜓 ↔ 𝜒)) & ⊢ (𝑝 = {𝑥, 𝑦} → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (Pairsproper‘𝑋)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 ∧ 𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 ≠ 𝑦 ∧ 𝜃) → {𝑥, 𝑦} = {𝑎, 𝑏})))) | ||
Theorem | poprelb 44494 | Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023.) |
⊢ (((Rel 𝑅 ∧ 𝑅 Po 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐶𝑅𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | 2exopprim 44495 | The existence of an ordered pair fulfilling a wff implies the existence of an unordered pair fulfilling the wff. (Contributed by AV, 29-Jul-2023.) |
⊢ (∃𝑎∃𝑏(〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) → ∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ 𝜑)) | ||
Theorem | reuopreuprim 44496* | There is a unique unordered pair with ordered elements fulfilling a wff if there is a unique ordered pair fulfilling the wff. (Contributed by AV, 28-Jul-2023.) |
⊢ (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜑) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑))) | ||
At first, the (sequence of) Fermat numbers FermatNo (the 𝑛-th Fermat number is denoted as (FermatNo‘𝑛)) is defined, see df-fmtno 44498, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 44547, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 44553. The fourth Fermat number (i.e., the fifth Fermat prime) (FermatNo‘4) = ;;;;65537 is currently the biggest number proven to be prime in set.mm, see 65537prm 44546 (previously, it was ;;;4001, see 4001prm 16574). Another important result of this section is Goldbach's theorem goldbachth 44517, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 44558. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 44560. | ||
Syntax | cfmtno 44497 | Extend class notation with the Fermat numbers. |
class FermatNo | ||
Definition | df-fmtno 44498 | Define the function that enumerates the Fermat numbers, see definition in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1)) | ||
Theorem | fmtno 44499 | The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1)) | ||
Theorem | fmtnoge3 44500 | Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |