![]() |
Metamath
Proof Explorer Theorem List (p. 457 of 473) | < 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-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iccpartxr 45601 | If there is a partition, then all intermediate points and bounds are extended real numbers. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (0...𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ*) | ||
Theorem | iccpartgtprec 45602 | If there is a partition, then all intermediate points and the upper bound are strictly greater than the preceeding intermediate points or lower bound. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘(𝐼 − 1)) < (𝑃‘𝐼)) | ||
Theorem | iccpartipre 45603 | If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ) | ||
Theorem | iccpartiltu 45604* | If there is a partition, then all intermediate points are strictly less than the upper bound. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀)) | ||
Theorem | iccpartigtl 45605* | If there is a partition, then all intermediate points are strictly greater than the lower bound. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖)) | ||
Theorem | iccpartlt 45606 | If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 44349 in GS's mathbox. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘0) < (𝑃‘𝑀)) | ||
Theorem | iccpartltu 45607* | If there is a partition, then all intermediate points and the lower bound are strictly less than the upper bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀)) | ||
Theorem | iccpartgtl 45608* | If there is a partition, then all intermediate points and the upper bound are strictly greater than the lower bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)(𝑃‘0) < (𝑃‘𝑖)) | ||
Theorem | iccpartgt 45609* | If there is a partition, then all intermediate points and the bounds are strictly ordered. (Contributed by AV, 18-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)(𝑖 < 𝑗 → (𝑃‘𝑖) < (𝑃‘𝑗))) | ||
Theorem | iccpartleu 45610* | If there is a partition, then all intermediate points and the lower and the upper bound are less than or equal to the upper bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘𝑖) ≤ (𝑃‘𝑀)) | ||
Theorem | iccpartgel 45611* | If there is a partition, then all intermediate points and the upper and the lower bound are greater than or equal to the lower bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑖)) | ||
Theorem | iccpartrn 45612 | 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‘𝑀)) ⇒ ⊢ (𝜑 → ran 𝑃 ⊆ ((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccpartf 45613 | The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 44353 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → 𝑃:(0...𝑀)⟶((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccpartel 45614 | 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 45615* | 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 45616* | 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 45617 | Lemma for icceuelpart 45618. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (𝐼 < 𝐽 → (𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽)))) | ||
Theorem | icceuelpart 45618* | 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 45619* | 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 45620 | A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 44350 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 8-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑃) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑃‘𝐼)(,)(𝑃‘(𝐼 + 1)))) | ||
Theorem | fargshiftfv 45621* | 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 45622* | 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 45623* | 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 45624* | 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 45625* | 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 45626 | 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 45627 | 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 45628* | 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 45636. Another, equivalent definition using two temporary setvar variables is provided in dfich2 45640. (Contributed by AV, 29-Jul-2023.) |
⊢ ([𝑥⇄𝑦]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)) | ||
Theorem | nfich1 45629 | The first interchangeable setvar variable is not free. (Contributed by AV, 21-Aug-2023.) |
⊢ Ⅎ𝑥[𝑥⇄𝑦]𝜑 | ||
Theorem | nfich2 45630 | The second interchangeable setvar variable is not free. (Contributed by AV, 21-Aug-2023.) |
⊢ Ⅎ𝑦[𝑥⇄𝑦]𝜑 | ||
Theorem | ichv 45631* | Setvar variables are interchangeable in a wff they do not appear in. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichf 45632 | Setvar variables are interchangeable in a wff they are not free in. (Contributed by SN, 23-Nov-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichid 45633 | A setvar variable is always interchangeable with itself. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑥]𝜑 | ||
Theorem | icht 45634 | A theorem is interchangeable. (Contributed by SN, 4-May-2024.) |
⊢ 𝜑 ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichbidv 45635* | Formula building rule for interchangeability (deduction). (Contributed by SN, 4-May-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑥⇄𝑦]𝜓 ↔ [𝑥⇄𝑦]𝜒)) | ||
Theorem | ichcircshi 45636* | 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 45637 | 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 45628 instead of dfich2 45640 to reduce axioms. (Revised by SN, 4-May-2024.) |
⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 ∧ 𝜓)) | ||
Theorem | ichn 45638 | Negation does not affect interchangeability. (Contributed by SN, 30-Aug-2023.) |
⊢ ([𝑎⇄𝑏]𝜑 ↔ [𝑎⇄𝑏] ¬ 𝜑) | ||
Theorem | ichim 45639 | Formula building rule for implication in interchangeability. (Contributed by SN, 4-May-2024.) |
⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 → 𝜓)) | ||
Theorem | dfich2 45640* | 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 45641* | The interchangeability of setvar variables is commutative. (Contributed by AV, 20-Aug-2023.) |
⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑦⇄𝑥]𝜓) | ||
Theorem | ichbi12i 45642* | Equivalence for interchangeable setvar variables. (Contributed by AV, 29-Jul-2023.) |
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒) | ||
Theorem | icheqid 45643 | In an equality for the same setvar variable, the setvar variable is interchangeable by itself. Special case of ichid 45633 and icheq 45644 without distinct variables restriction. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑥]𝑥 = 𝑥 | ||
Theorem | icheq 45644* | In an equality of setvar variables, the setvar variables are interchangeable. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑦]𝑥 = 𝑦 | ||
Theorem | ichnfimlem 45645* | Lemma for ichnfim 45646: A substitution for a nonfree variable has no effect. (Contributed by Wolf Lammen, 6-Aug-2023.) Avoid ax-13 2370. (Revised by Gino Giotto, 1-May-2024.) |
⊢ (∀𝑦Ⅎ𝑥𝜑 → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)) | ||
Theorem | ichnfim 45646* | 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 45647* | 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 45648* | Move a universal quantifier inside interchangeability. (Contributed by SN, 30-Aug-2023.) |
⊢ (∀𝑥[𝑎⇄𝑏]𝜑 → [𝑎⇄𝑏]∀𝑥𝜑) | ||
Theorem | ich2al 45649 | Two setvar variables are always interchangeable when there are two universal quantifiers. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]∀𝑥∀𝑦𝜑 | ||
Theorem | ich2ex 45650 | Two setvar variables are always interchangeable when there are two existential quantifiers. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]∃𝑥∃𝑦𝜑 | ||
Theorem | ichexmpl1 45651* | Example for interchangeable setvar variables in a statement of predicate calculus with equality. (Contributed by AV, 31-Jul-2023.) |
⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) | ||
Theorem | ichexmpl2 45652* | Example for interchangeable setvar variables in an arithmetic expression. (Contributed by AV, 31-Jul-2023.) |
⊢ [𝑎⇄𝑏]((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝑎↑2) + (𝑏↑2)) = (𝑐↑2)) | ||
Theorem | ich2exprop 45653* | 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 45654* | 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 45655* | 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 45656 | Two identical representations of the class of all unordered pairs. (Contributed by AV, 21-Nov-2021.) |
⊢ {𝑝 ∣ ∃𝑎 ∈ V ∃𝑏 ∈ V 𝑝 = {𝑎, 𝑏}} = {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} | ||
Theorem | elsprel 45657* | 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 4728, which is not an element of all unordered pairs, see spr0nelg 45658. (Contributed by AV, 21-Nov-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | spr0nelg 45658* | The empty set is not an element of all unordered pairs. (Contributed by AV, 21-Nov-2021.) |
⊢ ∅ ∉ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} | ||
Syntax | cspr 45659 | Extend class notation with set of pairs. |
class Pairs | ||
Definition | df-spr 45660* | 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 45661* | The set of all unordered pairs over a given set 𝑉. (Contributed by AV, 21-Nov-2021.) |
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | sprvalpw 45662* | 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 45663* | 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 45664 | The empty set is not an unordered pair over any set 𝑉. (Contributed by AV, 21-Nov-2021.) |
⊢ ∅ ∉ (Pairs‘𝑉) | ||
Theorem | sprvalpwn0 45665* | 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 45666* | 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 45667* | 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 45668 | 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 45669 | 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 45670 | 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 45671* | 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 45672* | Lemma for sprsymrelf 45677 and sprsymrelfv 45676. (Contributed by AV, 19-Nov-2021.) |
⊢ (𝑃 ⊆ (Pairs‘𝑉) → {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑃 𝑐 = {𝑥, 𝑦}} ∈ 𝒫 (𝑉 × 𝑉)) | ||
Theorem | sprsymrelf1lem 45673* | Lemma for sprsymrelf1 45678. (Contributed by AV, 22-Nov-2021.) |
⊢ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎 ⊆ 𝑏)) | ||
Theorem | sprsymrelfolem1 45674* | Lemma 1 for sprsymrelfo 45679. (Contributed by AV, 22-Nov-2021.) |
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)} ⇒ ⊢ 𝑄 ∈ 𝒫 (Pairs‘𝑉) | ||
Theorem | sprsymrelfolem2 45675* | Lemma 2 for sprsymrelfo 45679. (Contributed by AV, 23-Nov-2021.) |
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)) → (𝑥𝑅𝑦 ↔ ∃𝑐 ∈ 𝑄 𝑐 = {𝑥, 𝑦})) | ||
Theorem | sprsymrelfv 45676* | 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 45677* | 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 45678* | 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 45679* | 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 45680* | 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 45681* | 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 45682* | 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 12361). Examples for not proper unordered pairs are {1, 1} = {1} (see preqsn 4819), {1, V} = {1} (see prprc2 4727) or {V, V} = ∅ (see prprc 4728). | ||
Theorem | prpair 45683* | 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 45684 | Lemma 0 for prproropf1o 45689. 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 45685* | Lemma 1 for prproropf1o 45689. (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → {(1st ‘𝑊), (2nd ‘𝑊)} ∈ 𝑃) | ||
Theorem | prproropf1olem2 45686* | Lemma 2 for prproropf1o 45689. (Contributed by AV, 13-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃) → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ 𝑂) | ||
Theorem | prproropf1olem3 45687* | Lemma 3 for prproropf1o 45689. (Contributed by AV, 13-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉) ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → (𝐹‘{(1st ‘𝑊), (2nd ‘𝑊)}) = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) | ||
Theorem | prproropf1olem4 45688* | Lemma 4 for prproropf1o 45689. (Contributed by AV, 14-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉) ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝐹‘𝑍) = (𝐹‘𝑊) → 𝑍 = 𝑊)) | ||
Theorem | prproropf1o 45689* | 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 45690* | 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 45691* | 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 45692* | Two equivalent representations of the existence of a unique proper pair. (Contributed by AV, 1-Mar-2023.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (∃!𝑝 ∈ 𝑃 𝜑 ↔ ∃!𝑝 ∈ 𝒫 𝑉((♯‘𝑝) = 2 ∧ 𝜑)) | ||
Theorem | paireqne 45693* | 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 45694 | Extend class notation with set of proper unordered pairs. |
class Pairsproper | ||
Definition | df-prpr 45695* | 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 45696* | The set of all proper unordered pairs over a given set 𝑉. (Contributed by AV, 29-Apr-2023.) |
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}) | ||
Theorem | prprvalpw 45697* | 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 45698 | 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 45699* | 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 45700* | 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} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |