Home | Metamath
Proof Explorer Theorem List (p. 55 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | snopeqopsnid 5401 | Equivalence for an ordered pair of two identical singletons equal to a singleton of an ordered pair. (Contributed by AV, 24-Sep-2020.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {〈𝐴, 𝐴〉} = 〈{𝐴}, {𝐴}〉 | ||
Theorem | mosubopt 5402* | "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.) |
⊢ (∀𝑦∀𝑧∃*𝑥𝜑 → ∃*𝑥∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝜑)) | ||
Theorem | mosubop 5403* | "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.) |
⊢ ∃*𝑥𝜑 ⇒ ⊢ ∃*𝑥∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝜑) | ||
Theorem | euop2 5404* | Transfer existential uniqueness to second member of an ordered pair. (Contributed by NM, 10-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑥∃𝑦(𝑥 = 〈𝐴, 𝑦〉 ∧ 𝜑) ↔ ∃!𝑦𝜑) | ||
Theorem | euotd 5405* | Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶))) ⇒ ⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) | ||
Theorem | opthwiener 5406 | Justification theorem for the ordered pair definition in Norbert Wiener, "A simplification of the logic of relations", Proc. of the Cambridge Philos. Soc., 1914, vol. 17, pp.387-390. It is also shown as a definition in [Enderton] p. 36 and as Exercise 4.8(b) of [Mendelson] p. 230. It is meaningful only for classes that exist as sets (i.e. are not proper classes). See df-op 4576 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | uniop 5407 | The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ 〈𝐴, 𝐵〉 = {𝐴, 𝐵} | ||
Theorem | uniopel 5408 | Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → ∪ 〈𝐴, 𝐵〉 ∈ ∪ 𝐶) | ||
Theorem | opthhausdorff 5409 | Justification theorem for the ordered pair definition of Felix Hausdorff in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), 1914, p. 32: 〈𝐴, 𝐵〉H = {{𝐴, 𝑂}, {𝐵, 𝑇}}. Hausdorff used 1 and 2 instead of 𝑂 and 𝑇, but actually, any two different fixed sets will do (e.g., 𝑂 = ∅ and 𝑇 = {∅}, see 0nep0 5260). Furthermore, Hausdorff demanded that 𝑂 and 𝑇 are both different from 𝐴 as well as 𝐵, which is actually not necessary in full extent (𝐴 ≠ 𝑇 is not required). This definition is meaningful only for classes 𝐴 and 𝐵 that exist as sets (i.e. are not proper classes): If 𝐴 and 𝐶 were different proper classes (𝐴 ≠ 𝐶), then {{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇} ↔ {{𝑂}, {𝐵, 𝑇}} = {{𝑂}, {𝐷, 𝑇} is true if 𝐵 = 𝐷, but (𝐴 = 𝐶 ∧ 𝐵 = 𝐷) would be false. See df-op 4576 for other ordered pair definitions. (Contributed by AV, 14-Jun-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐴 ≠ 𝑂 & ⊢ 𝐵 ≠ 𝑂 & ⊢ 𝐵 ≠ 𝑇 & ⊢ 𝑂 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝑂 ≠ 𝑇 ⇒ ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthhausdorff0 5410 | Justification theorem for the ordered pair definition of Felix Hausdorff in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), 1914, p. 32: 〈𝐴, 𝐵〉H = {{𝐴, 𝑂}, {𝐵, 𝑇}}. Hausdorff used 1 and 2 instead of 𝑂 and 𝑇, but actually, any two different fixed sets will do (e.g., 𝑂 = ∅ and 𝑇 = {∅}, see 0nep0 5260). Furthermore, Hausdorff demanded that 𝑂 and 𝑇 are both different from 𝐴 as well as 𝐵, which is actually not necessary if all involved classes exist as sets (i.e. are not proper classes), in contrast to opthhausdorff 5409. See df-op 4576 for other ordered pair definitions. (Contributed by AV, 12-Jun-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝑂 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝑂 ≠ 𝑇 ⇒ ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | otsndisj 5411* | The singletons consisting of ordered triples which have distinct third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑉 {〈𝐴, 𝐵, 𝑐〉}) | ||
Theorem | otiunsndisj 5412* | The union of singletons consisting of ordered triples which have distinct first and third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉}) | ||
Theorem | iunopeqop 5413* | Implication of an ordered pair being equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020.) (Avoid depending on this detail.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧})) | ||
Theorem | opabidw 5414* | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5415 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 14-Apr-1995.) (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) | ||
Theorem | opabid 5415 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker opabidw 5414 when possible. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) |
⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) | ||
Theorem | elopab 5416* | Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) | ||
Theorem | rexopabb 5417* | Restricted existential quantification over an ordered-pair class abstraction. (Contributed by AV, 8-Nov-2023.) |
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ 𝜑} & ⊢ (𝑜 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑜 ∈ 𝑂 𝜓 ↔ ∃𝑥∃𝑦(𝜑 ∧ 𝜒)) | ||
Theorem | opelopabsbALT 5418* | The law of concretion in terms of substitutions. Less general than opelopabsb 5419, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑) | ||
Theorem | opelopabsb 5419* | The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) | ||
Theorem | brabsb 5420* | The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) | ||
Theorem | opelopabt 5421* | Closed theorem form of opelopab 5431. (Contributed by NM, 19-Feb-2013.) |
⊢ ((∀𝑥∀𝑦(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥∀𝑦(𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | opelopabga 5422* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | brabga 5423* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) | ||
Theorem | opelopab2a 5424* | Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜓)) | ||
Theorem | opelopaba 5425* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | braba 5426* | The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜓) | ||
Theorem | opelopabg 5427* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | brabg 5428* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒)) | ||
Theorem | opelopabgf 5429* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopabg 5427 uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | opelopab2 5430* | Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜒)) | ||
Theorem | opelopab 5431* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) | ||
Theorem | brab 5432* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜒) | ||
Theorem | opelopabaf 5433* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 5431 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | opelopabf 5434* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 5431 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) | ||
Theorem | ssopab2 5435 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) | ||
Theorem | ssopab2bw 5436* | Equivalence of ordered pair abstraction subclass and implication. Version of ssopab2b 5438 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 27-Dec-1996.) (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
Theorem | eqopab2bw 5437* | Equivalence of ordered pair abstraction equality and biconditional. Version of eqopab2b 5441 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by Mario Carneiro, 4-Jan-2017.) (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) | ||
Theorem | ssopab2b 5438 | Equivalence of ordered pair abstraction subclass and implication. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker ssopab2bw 5436 when possible. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) (New usage is discouraged.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
Theorem | ssopab2i 5439 | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} | ||
Theorem | ssopab2dv 5440* | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜒}) | ||
Theorem | eqopab2b 5441 | Equivalence of ordered pair abstraction equality and biconditional. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker eqopab2bw 5437 when possible. (Contributed by Mario Carneiro, 4-Jan-2017.) (New usage is discouraged.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) | ||
Theorem | opabn0 5442 | Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥∃𝑦𝜑) | ||
Theorem | opab0 5443 | Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = ∅ ↔ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | csbopab 5444* | Move substitution into a class abstraction. Version of csbopabgALT 5445 without a sethood antecedent but depending on more axioms. (Contributed by NM, 6-Aug-2007.) (Revised by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥]𝜑} | ||
Theorem | csbopabgALT 5445* | Move substitution into a class abstraction. Version of csbopab 5444 with a sethood antecedent but depending on fewer axioms. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥]𝜑}) | ||
Theorem | csbmpt12 5446* | Move substitution into a maps-to notation. (Contributed by AV, 26-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍)) | ||
Theorem | csbmpt2 5447* | Move substitution into the second part of a maps-to notation. (Contributed by AV, 26-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ 𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍)) | ||
Theorem | iunopab 5448* | Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ ∪ 𝑧 ∈ 𝐴 {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 𝜑} | ||
Theorem | elopabr 5449* | Membership in a class abstraction of pairs, defined by a binary relation. (Contributed by AV, 16-Feb-2021.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} → 𝐴 ∈ 𝑅) | ||
Theorem | elopabran 5450* | Membership in a class abstraction of pairs, defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} → 𝐴 ∈ 𝑅) | ||
Theorem | rbropapd 5451* | Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒)))) | ||
Theorem | rbropap 5452* | Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the condition 𝜓. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒))) | ||
Theorem | 2rbropap 5453* | Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the conditions 𝜓 and 𝜏. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓 ∧ 𝜏)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜏 ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒 ∧ 𝜃))) | ||
Theorem | 0nelopab 5454 | The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
⊢ ¬ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | brabv 5455 | If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
⊢ (𝑋{〈𝑥, 𝑦〉 ∣ 𝜑}𝑌 → (𝑋 ∈ V ∧ 𝑌 ∈ V)) | ||
Theorem | pwin 5456 | The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) |
⊢ 𝒫 (𝐴 ∩ 𝐵) = (𝒫 𝐴 ∩ 𝒫 𝐵) | ||
Theorem | pwunssOLD 5457 | Obsolete version of pwunss 4561 as of 30-Dec-2023. (Contributed by NM, 23-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | pwssun 5458 | The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ 𝒫 (𝐴 ∪ 𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵)) | ||
Theorem | pwundifOLD 5459 | Obsolete proof of pwundif 4567 as of 26-Dec-2023. (Contributed by NM, 25-Mar-2007.) (Proof shortened by Thierry Arnoux, 20-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) | ||
Theorem | pwun 5460 | The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by NM, 23-Nov-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ 𝒫 (𝐴 ∪ 𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵)) | ||
Syntax | cid 5461 | Extend the definition of a class to include the identity relation. |
class I | ||
Definition | df-id 5462* | Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5 (ex-id 28215). (Contributed by NM, 13-Aug-1995.) |
⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | ||
Theorem | dfid4 5463 | The identity function expressed using maps-to notation. (Contributed by Scott Fenton, 15-Dec-2017.) |
⊢ I = (𝑥 ∈ V ↦ 𝑥) | ||
Theorem | dfid3 5464 | A stronger version of df-id 5462 that does not require 𝑥 and 𝑦 to be disjoint. This is not the "official" definition since our definition soundness check without this requirement would be much more complex. The proof can be instructive in showing how disjoint variable requirements may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.) Use directly the definition df-id 5462 when sufficient, since the derivation of dfid3 5464 is nontrivial and uses auxiliary axioms ax-10 2145 to ax-13 2390. (New usage is discouraged.) |
⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | ||
Theorem | dfid2 5465 | Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.) Use df-id 5462 when sufficient (see comment at dfid3 5464). (New usage is discouraged.) |
⊢ I = {〈𝑥, 𝑥〉 ∣ 𝑥 = 𝑥} | ||
Syntax | cep 5466 | Extend class notation to include the membership relation. |
class E | ||
Definition | df-eprel 5467* | Define the membership relation (also called "epsilon relation" since it is sometimes denoted by the lowercase Greek letter "epsilon"). Similar to Definition 6.22 of [TakeutiZaring] p. 30. The membership relation and the membership predicate agree, that is, (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵), when 𝐵 is a set (see epelg 5468). Thus, ⊢ 5 E {1, 5} (ex-eprel 28214). (Contributed by NM, 13-Aug-1995.) |
⊢ E = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ 𝑦} | ||
Theorem | epelg 5468 | The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5471 and closed form of epeli 5470. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 14-Jul-2023.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | epelgOLD 5469 | Obsolete version of epelg 5468 as of 14-Jul-2023. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | epeli 5470 | The membership relation and the membership predicate agree when the "containing" class is a set. Inference associated with epelg 5468. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | epel 5471 | The membership relation and the membership predicate agree when the "containing" class is a setvar. (Contributed by NM, 13-Aug-1995.) Replace the first setvar variable with a class variable. (Revised by BJ, 13-Sep-2022.) |
⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥) | ||
Theorem | 0sn0ep 5472 | An example for the membership relation. (Contributed by AV, 19-Jun-2022.) |
⊢ ∅ E {∅} | ||
Theorem | epn0 5473 | The membership relation is nonempty. (Contributed by AV, 19-Jun-2022.) |
⊢ E ≠ ∅ | ||
We have not yet defined relations (df-rel 5564), but here we introduce a few related notions we will use to develop ordinals. The class variable 𝑅 is no different from other class variables, but it reminds us that normally it represents what we will later call a "relation". | ||
Syntax | wpo 5474 | Extend wff notation to include the strict partial ordering predicate. Read: "𝑅 is a partial order on 𝐴". |
wff 𝑅 Po 𝐴 | ||
Syntax | wor 5475 | Extend wff notation to include the strict total ordering predicate. Read: "𝑅 orders 𝐴". |
wff 𝑅 Or 𝐴 | ||
Definition | df-po 5476* | Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on 𝐴. For example, < Po ℝ is true, while ≤ Po ℝ is false (ex-po 28216). (Contributed by NM, 16-Mar-1997.) |
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) | ||
Definition | df-so 5477* | Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 10723). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.) |
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
Theorem | poss 5478 | Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴)) | ||
Theorem | poeq1 5479 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) | ||
Theorem | poeq2 5480 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵)) | ||
Theorem | nfpo 5481 | Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Po 𝐴 | ||
Theorem | nfso 5482 | Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Or 𝐴 | ||
Theorem | pocl 5483 | Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) | ||
Theorem | ispod 5484* | Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | swopolem 5485* | Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) | ||
Theorem | swopo 5486* | A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | poirr 5487 | A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | potr 5488 | A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | po2nr 5489 | A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
Theorem | po3nr 5490 | A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | po2ne 5491 | Two classes which are in a partial order relation are not equal. (Contributed by AV, 13-Mar-2023.) |
⊢ ((𝑅 Po 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴𝑅𝐵) → 𝐴 ≠ 𝐵) | ||
Theorem | po0 5492 | Any relation is a partial ordering of the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ 𝑅 Po ∅ | ||
Theorem | pofun 5493* | A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.) |
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ 𝑋𝑅𝑌} & ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) | ||
Theorem | sopo 5494 | A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.) |
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) | ||
Theorem | soss 5495 | Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) | ||
Theorem | soeq1 5496 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | ||
Theorem | soeq2 5497 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) | ||
Theorem | sonr 5498 | A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | sotr 5499 | A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | solin 5500 | A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |