![]() |
Metamath
Proof Explorer Theorem List (p. 463 of 480) | < 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: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nfich2 46201 | The second interchangeable setvar variable is not free. (Contributed by AV, 21-Aug-2023.) |
⊢ Ⅎ𝑦[𝑥⇄𝑦]𝜑 | ||
Theorem | ichv 46202* | Setvar variables are interchangeable in a wff they do not appear in. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichf 46203 | Setvar variables are interchangeable in a wff they are not free in. (Contributed by SN, 23-Nov-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichid 46204 | A setvar variable is always interchangeable with itself. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑥]𝜑 | ||
Theorem | icht 46205 | A theorem is interchangeable. (Contributed by SN, 4-May-2024.) |
⊢ 𝜑 ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichbidv 46206* | Formula building rule for interchangeability (deduction). (Contributed by SN, 4-May-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑥⇄𝑦]𝜓 ↔ [𝑥⇄𝑦]𝜒)) | ||
Theorem | ichcircshi 46207* | 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 46208 | 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 46199 instead of dfich2 46211 to reduce axioms. (Revised by SN, 4-May-2024.) |
⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 ∧ 𝜓)) | ||
Theorem | ichn 46209 | Negation does not affect interchangeability. (Contributed by SN, 30-Aug-2023.) |
⊢ ([𝑎⇄𝑏]𝜑 ↔ [𝑎⇄𝑏] ¬ 𝜑) | ||
Theorem | ichim 46210 | Formula building rule for implication in interchangeability. (Contributed by SN, 4-May-2024.) |
⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 → 𝜓)) | ||
Theorem | dfich2 46211* | 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 46212* | The interchangeability of setvar variables is commutative. (Contributed by AV, 20-Aug-2023.) |
⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑦⇄𝑥]𝜓) | ||
Theorem | ichbi12i 46213* | Equivalence for interchangeable setvar variables. (Contributed by AV, 29-Jul-2023.) |
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒) | ||
Theorem | icheqid 46214 | In an equality for the same setvar variable, the setvar variable is interchangeable by itself. Special case of ichid 46204 and icheq 46215 without distinct variables restriction. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑥]𝑥 = 𝑥 | ||
Theorem | icheq 46215* | In an equality of setvar variables, the setvar variables are interchangeable. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑦]𝑥 = 𝑦 | ||
Theorem | ichnfimlem 46216* | Lemma for ichnfim 46217: 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 46217* | 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 46218* | 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 46219* | Move a universal quantifier inside interchangeability. (Contributed by SN, 30-Aug-2023.) |
⊢ (∀𝑥[𝑎⇄𝑏]𝜑 → [𝑎⇄𝑏]∀𝑥𝜑) | ||
Theorem | ich2al 46220 | Two setvar variables are always interchangeable when there are two universal quantifiers. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]∀𝑥∀𝑦𝜑 | ||
Theorem | ich2ex 46221 | Two setvar variables are always interchangeable when there are two existential quantifiers. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]∃𝑥∃𝑦𝜑 | ||
Theorem | ichexmpl1 46222* | Example for interchangeable setvar variables in a statement of predicate calculus with equality. (Contributed by AV, 31-Jul-2023.) |
⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) | ||
Theorem | ichexmpl2 46223* | Example for interchangeable setvar variables in an arithmetic expression. (Contributed by AV, 31-Jul-2023.) |
⊢ [𝑎⇄𝑏]((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝑎↑2) + (𝑏↑2)) = (𝑐↑2)) | ||
Theorem | ich2exprop 46224* | 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 46225* | 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 46226* | 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 46227 | Two identical representations of the class of all unordered pairs. (Contributed by AV, 21-Nov-2021.) |
⊢ {𝑝 ∣ ∃𝑎 ∈ V ∃𝑏 ∈ V 𝑝 = {𝑎, 𝑏}} = {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} | ||
Theorem | elsprel 46228* | 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 4771, which is not an element of all unordered pairs, see spr0nelg 46229. (Contributed by AV, 21-Nov-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | spr0nelg 46229* | The empty set is not an element of all unordered pairs. (Contributed by AV, 21-Nov-2021.) |
⊢ ∅ ∉ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} | ||
Syntax | cspr 46230 | Extend class notation with set of pairs. |
class Pairs | ||
Definition | df-spr 46231* | 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 46232* | The set of all unordered pairs over a given set 𝑉. (Contributed by AV, 21-Nov-2021.) |
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | sprvalpw 46233* | 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 46234* | 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 46235 | The empty set is not an unordered pair over any set 𝑉. (Contributed by AV, 21-Nov-2021.) |
⊢ ∅ ∉ (Pairs‘𝑉) | ||
Theorem | sprvalpwn0 46236* | 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 46237* | 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 46238* | 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 46239 | 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 46240 | 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 46241 | 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 46242* | 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 46243* | Lemma for sprsymrelf 46248 and sprsymrelfv 46247. (Contributed by AV, 19-Nov-2021.) |
⊢ (𝑃 ⊆ (Pairs‘𝑉) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑃 𝑐 = {𝑥, 𝑦}} ∈ 𝒫 (𝑉 × 𝑉)) | ||
Theorem | sprsymrelf1lem 46244* | Lemma for sprsymrelf1 46249. (Contributed by AV, 22-Nov-2021.) |
⊢ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎 ⊆ 𝑏)) | ||
Theorem | sprsymrelfolem1 46245* | Lemma 1 for sprsymrelfo 46250. (Contributed by AV, 22-Nov-2021.) |
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)} ⇒ ⊢ 𝑄 ∈ 𝒫 (Pairs‘𝑉) | ||
Theorem | sprsymrelfolem2 46246* | Lemma 2 for sprsymrelfo 46250. (Contributed by AV, 23-Nov-2021.) |
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)) → (𝑥𝑅𝑦 ↔ ∃𝑐 ∈ 𝑄 𝑐 = {𝑥, 𝑦})) | ||
Theorem | sprsymrelfv 46247* | 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 46248* | 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 46249* | 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 46250* | 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 46251* | 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 46252* | 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 46253* | 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 12422). Examples for not proper unordered pairs are {1, 1} = {1} (see preqsn 4862), {1, V} = {1} (see prprc2 4770) or {V, V} = ∅ (see prprc 4771). | ||
Theorem | prpair 46254* | 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 46255 | Lemma 0 for prproropf1o 46260. 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 46256* | Lemma 1 for prproropf1o 46260. (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → {(1st ‘𝑊), (2nd ‘𝑊)} ∈ 𝑃) | ||
Theorem | prproropf1olem2 46257* | Lemma 2 for prproropf1o 46260. (Contributed by AV, 13-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃) → ⟨inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)⟩ ∈ 𝑂) | ||
Theorem | prproropf1olem3 46258* | Lemma 3 for prproropf1o 46260. (Contributed by AV, 13-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ ⟨inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)⟩) ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → (𝐹‘{(1st ‘𝑊), (2nd ‘𝑊)}) = ⟨(1st ‘𝑊), (2nd ‘𝑊)⟩) | ||
Theorem | prproropf1olem4 46259* | Lemma 4 for prproropf1o 46260. (Contributed by AV, 14-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ ⟨inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)⟩) ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝐹‘𝑍) = (𝐹‘𝑊) → 𝑍 = 𝑊)) | ||
Theorem | prproropf1o 46260* | 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 46261* | 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 46262* | 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 46263* | Two equivalent representations of the existence of a unique proper pair. (Contributed by AV, 1-Mar-2023.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (∃!𝑝 ∈ 𝑃 𝜑 ↔ ∃!𝑝 ∈ 𝒫 𝑉((♯‘𝑝) = 2 ∧ 𝜑)) | ||
Theorem | paireqne 46264* | 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 46265 | Extend class notation with set of proper unordered pairs. |
class Pairsproper | ||
Definition | df-prpr 46266* | 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 46267* | The set of all proper unordered pairs over a given set 𝑉. (Contributed by AV, 29-Apr-2023.) |
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}) | ||
Theorem | prprvalpw 46268* | 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 46269 | 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 46270* | 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 46271* | 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 46272* | 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 46273* | 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 46274* | 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 46275* | 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 46276* | 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 46277 | Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023.) |
⊢ (((Rel 𝑅 ∧ 𝑅 Po 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐶𝑅𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | 2exopprim 46278 | 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 46279* | 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 46281, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 46330, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 46336. 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 46329 (previously, it was ;;;4001, see 4001prm 17080). Another important result of this section is Goldbach's theorem goldbachth 46300, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 46341. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 46343. | ||
Syntax | cfmtno 46280 | Extend class notation with the Fermat numbers. |
class FermatNo | ||
Definition | df-fmtno 46281 | 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 46282 | The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1)) | ||
Theorem | fmtnoge3 46283 | Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3)) | ||
Theorem | fmtnonn 46284 | Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ ℕ) | ||
Theorem | fmtnom1nn 46285 | A Fermat number minus one is a power of a power of two. (Contributed by AV, 29-Jul-2021.) |
⊢ (𝑁 ∈ ℕ0 → ((FermatNo‘𝑁) − 1) = (2↑(2↑𝑁))) | ||
Theorem | fmtnoodd 46286 | Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.) |
⊢ (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁)) | ||
Theorem | fmtnorn 46287* | A Fermat number is a function value of the enumeration of the Fermat numbers. (Contributed by AV, 3-Aug-2021.) |
⊢ (𝐹 ∈ ran FermatNo ↔ ∃𝑛 ∈ ℕ0 (FermatNo‘𝑛) = 𝐹) | ||
Theorem | fmtnof1 46288 | The enumeration of the Fermat numbers is a one-one function into the positive integers. (Contributed by AV, 3-Aug-2021.) |
⊢ FermatNo:ℕ0–1-1→ℕ | ||
Theorem | fmtnoinf 46289 | The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.) |
⊢ ran FermatNo ∉ Fin | ||
Theorem | fmtnorec1 46290 | The first recurrence relation for Fermat numbers, see Wikipedia "Fermat number", https://en.wikipedia.org/wiki/Fermat_number#Basic_properties, 22-Jul-2021. (Contributed by AV, 22-Jul-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘(𝑁 + 1)) = ((((FermatNo‘𝑁) − 1)↑2) + 1)) | ||
Theorem | sqrtpwpw2p 46291 | The floor of the square root of 2 to the power of 2 to the power of a positive integer plus a bounded nonnegative integer. (Contributed by AV, 28-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < ((2↑((2↑(𝑁 − 1)) + 1)) + 1)) → (⌊‘(√‘((2↑(2↑𝑁)) + 𝑀))) = (2↑(2↑(𝑁 − 1)))) | ||
Theorem | fmtnosqrt 46292 | The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.) |
⊢ (𝑁 ∈ ℕ → (⌊‘(√‘(FermatNo‘𝑁))) = (2↑(2↑(𝑁 − 1)))) | ||
Theorem | fmtno0 46293 | The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘0) = 3 | ||
Theorem | fmtno1 46294 | The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘1) = 5 | ||
Theorem | fmtnorec2lem 46295* | Lemma for fmtnorec2 46296 (induction step). (Contributed by AV, 29-Jul-2021.) |
⊢ (𝑦 ∈ ℕ0 → ((FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2))) | ||
Theorem | fmtnorec2 46296* | The second recurrence relation for Fermat numbers, see ProofWiki "Product of Sequence of Fermat Numbers plus 2", 29-Jul-2021, https://proofwiki.org/wiki/Product_of_Sequence_of_Fermat_Numbers_plus_2 or Wikipedia "Fermat number", 29-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 29-Jul-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘(𝑁 + 1)) = (∏𝑛 ∈ (0...𝑁)(FermatNo‘𝑛) + 2)) | ||
Theorem | fmtnodvds 46297 | Any Fermat number divides a greater Fermat number minus 2. Corollary of fmtnorec2 46296, see ProofWiki "Product of Sequence of Fermat Numbers plus 2/Corollary", 31-Jul-2021. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ) → (FermatNo‘𝑁) ∥ ((FermatNo‘(𝑁 + 𝑀)) − 2)) | ||
Theorem | goldbachthlem1 46298 | Lemma 1 for goldbachth 46300. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → (FermatNo‘𝑀) ∥ ((FermatNo‘𝑁) − 2)) | ||
Theorem | goldbachthlem2 46299 | Lemma 2 for goldbachth 46300. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1) | ||
Theorem | goldbachth 46300 | Goldbach's theorem: Two different Fermat numbers are coprime. See ProofWiki "Goldbach's theorem", 31-Jul-2021, https://proofwiki.org/wiki/Goldbach%27s_Theorem or Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ≠ 𝑀) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |