P. 445 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44401-44500   *Has distinct variable group(s)

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))))
20.41.9  Shifting functions with an integer range domain
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) / 𝑥⦌𝑃))
20.41.10  Words over a set (extension)
20.41.10.1  Last symbol of a word - extension
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‘𝑊) ≠ ∅)
20.41.11  Unordered pairs
20.41.11.1  Interchangeable setvar variables
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.)
⊢ ([𝑎⇄𝑏]𝜑 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑)))
20.41.11.2  Set of unordered pairs
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‘𝑉)    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝑃 ≈ 𝑅)
20.41.11.3  Proper (unordered) 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}    ⇒   ⊢ (𝜑 → (∃!𝑝 ∈ 𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 ≠ 𝐵))
20.41.11.4  Set of proper unordered pairs
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‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
20.41.12  Number theory (extension)
20.41.12.1  Fermat numbers 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))