![]() |
Metamath
Proof Explorer Theorem List (p. 53 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43661) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | opeqpr 5201 | Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = {𝐶, 𝐷} ↔ ((𝐶 = {𝐴} ∧ 𝐷 = {𝐴, 𝐵}) ∨ (𝐶 = {𝐴, 𝐵} ∧ 𝐷 = {𝐴}))) | ||
Theorem | snopeqop 5202 | Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({〈𝐴, 𝐵〉} = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = {𝐴})) | ||
Theorem | snopeqopOLD 5203 | Obsolete version of snopeqop 5202 as of 15-Jul-2022 . (Contributed by AV, 18-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ({〈𝐴, 𝐵〉} = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = {𝐴})) | ||
Theorem | propeqop 5204 | Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020.) (Proof shortened by AV, 16-Jun-2022.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ ({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = 〈𝐸, 𝐹〉 ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) | ||
Theorem | propssopi 5205 | If a pair of ordered pairs is a subset of an ordered pair, their first components are equal. (Contributed by AV, 20-Sep-2020.) (Proof shortened by AV, 16-Jun-2022.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ ({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ⊆ 〈𝐸, 𝐹〉 → 𝐴 = 𝐶) | ||
Theorem | snopeqopsnid 5206 | 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 5207* | "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.) |
⊢ (∀𝑦∀𝑧∃*𝑥𝜑 → ∃*𝑥∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝜑)) | ||
Theorem | mosubop 5208* | "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.) |
⊢ ∃*𝑥𝜑 ⇒ ⊢ ∃*𝑥∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝜑) | ||
Theorem | euop2 5209* | Transfer existential uniqueness to second member of an ordered pair. (Contributed by NM, 10-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑥∃𝑦(𝑥 = 〈𝐴, 𝑦〉 ∧ 𝜑) ↔ ∃!𝑦𝜑) | ||
Theorem | euotd 5210* | Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶))) ⇒ ⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) | ||
Theorem | opthwiener 5211 | 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 4405 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | uniop 5212 | 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 5213 | 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 5214 | 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 5070). 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 4405 for other ordered pair definitions. (Contributed by AV, 14-Jun-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐴 ≠ 𝑂 & ⊢ 𝐵 ≠ 𝑂 & ⊢ 𝐵 ≠ 𝑇 & ⊢ 𝑂 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝑂 ≠ 𝑇 ⇒ ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthhausdorff0 5215 | 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 5070). 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 5214. See df-op 4405 for other ordered pair definitions. (Contributed by AV, 12-Jun-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝑂 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝑂 ≠ 𝑇 ⇒ ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | otsndisj 5216* | 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 5217* | 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 5218* | 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 | opabid 5219 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) | ||
Theorem | elopab 5220* | Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) | ||
Theorem | opelopabsbALT 5221* | The law of concretion in terms of substitutions. Less general than opelopabsb 5222, 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 5222* | The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) | ||
Theorem | brabsb 5223* | The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) | ||
Theorem | opelopabt 5224* | Closed theorem form of opelopab 5234. (Contributed by NM, 19-Feb-2013.) |
⊢ ((∀𝑥∀𝑦(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥∀𝑦(𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | opelopabga 5225* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | brabga 5226* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) | ||
Theorem | opelopab2a 5227* | Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜓)) | ||
Theorem | opelopaba 5228* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | braba 5229* | The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜓) | ||
Theorem | opelopabg 5230* | 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 5231* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒)) | ||
Theorem | opelopabgf 5232* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopabg 5230 uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | opelopab2 5233* | Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜒)) | ||
Theorem | opelopab 5234* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) | ||
Theorem | brab 5235* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜒) | ||
Theorem | opelopabaf 5236* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 5234 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 5237* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 5234 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) | ||
Theorem | ssopab2 5238 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) | ||
Theorem | ssopab2b 5239 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
Theorem | ssopab2i 5240 | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} | ||
Theorem | ssopab2dv 5241* | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜒}) | ||
Theorem | eqopab2b 5242 | Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) | ||
Theorem | opabn0 5243 | Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥∃𝑦𝜑) | ||
Theorem | opab0 5244 | Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = ∅ ↔ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | csbopab 5245* | Move substitution into a class abstraction. Version of csbopabgALT 5246 without a sethood antecedent but depending on more axioms. (Contributed by NM, 6-Aug-2007.) (Revised by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥]𝜑} | ||
Theorem | csbopabgALT 5246* | Move substitution into a class abstraction. Version of csbopab 5245 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 5247* | Move substitution into a maps-to notation. (Contributed by AV, 26-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍)) | ||
Theorem | csbmpt2 5248* | Move substitution into the second part of a maps-to notation. (Contributed by AV, 26-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ 𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍)) | ||
Theorem | iunopab 5249* | Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ ∪ 𝑧 ∈ 𝐴 {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 𝜑} | ||
Theorem | elopabr 5250* | Membership in a class abstraction of pairs, defined by a binary relation. (Contributed by AV, 16-Feb-2021.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} → 𝐴 ∈ 𝑅) | ||
Theorem | elopabran 5251* | Membership in a class abstraction of pairs, defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} → 𝐴 ∈ 𝑅) | ||
Theorem | rbropapd 5252* | Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒)))) | ||
Theorem | rbropap 5253* | 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 5254* | 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 | pwin 5255 | 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 | pwunss 5256 | The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) |
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | pwssun 5257 | 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 | pwundif 5258 | Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007.) (Proof shortened by Thierry Arnoux, 20-Dec-2016.) |
⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) | ||
Theorem | pwun 5259 | 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 5260 | Extend the definition of a class to include the identity relation. |
class I | ||
Definition | df-id 5261* | Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5 (ex-id 27866). (Contributed by NM, 13-Aug-1995.) |
⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | ||
Theorem | dfid3 5262 | A stronger version of df-id 5261 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 5261 when sufficient, since the derivation of dfid3 5262 is nontrivial and uses auxiliary axioms ax-10 2135 to ax-13 2334. (New usage is discouraged.) |
⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | ||
Theorem | dfid4 5263 | The identity function using maps-to notation. (Contributed by Scott Fenton, 15-Dec-2017.) |
⊢ I = (𝑥 ∈ V ↦ 𝑥) | ||
Theorem | dfid2 5264 | Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.) Use df-id 5261 when sufficient (see comment at dfid3 5262). (New usage is discouraged.) |
⊢ I = {〈𝑥, 𝑥〉 ∣ 𝑥 = 𝑥} | ||
Syntax | cep 5265 | Extend class notation to include the membership relation. |
class E | ||
Definition | df-eprel 5266* | 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 5267). Thus, ⊢ 5 E {1, 5} (ex-eprel 27865). (Contributed by NM, 13-Aug-1995.) |
⊢ E = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ 𝑦} | ||
Theorem | epelg 5267 | The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5269 and closed form of epeli 5268. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | epeli 5268 | The membership relation and the membership predicate agree when the "containing" class is a set. Inference associated with epelg 5267. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | epel 5269 | 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 5270 | An example for the membership relation. (Contributed by AV, 19-Jun-2022.) |
⊢ ∅ E {∅} | ||
Theorem | epn0 5271 | The membership relation is nonempty. (Contributed by AV, 19-Jun-2022.) |
⊢ E ≠ ∅ | ||
We have not yet defined relations (df-rel 5362), 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 5272 | Extend wff notation to include the strict partial ordering predicate. Read: "𝑅 is a partial order on 𝐴". |
wff 𝑅 Po 𝐴 | ||
Syntax | wor 5273 | Extend wff notation to include the strict complete ordering predicate. Read: "𝑅 orders 𝐴". |
wff 𝑅 Or 𝐴 | ||
Definition | df-po 5274* | 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 27867). (Contributed by NM, 16-Mar-1997.) |
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) | ||
Definition | df-so 5275* | Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 10457). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.) |
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
Theorem | poss 5276 | 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 5277 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) | ||
Theorem | poeq2 5278 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵)) | ||
Theorem | nfpo 5279 | Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Po 𝐴 | ||
Theorem | nfso 5280 | Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Or 𝐴 | ||
Theorem | pocl 5281 | Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) | ||
Theorem | ispod 5282* | Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | swopolem 5283* | Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) | ||
Theorem | swopo 5284* | A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | poirr 5285 | A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | potr 5286 | A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | po2nr 5287 | A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
Theorem | po3nr 5288 | A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | po2ne 5289 | Two classes which are in a partial order relation are not equal. (Contributed by AV, 13-Mar-2023.) |
⊢ ((𝑅 Po 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴𝑅𝐵) → 𝐴 ≠ 𝐵) | ||
Theorem | po0 5290 | 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 5291* | A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.) |
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ 𝑋𝑅𝑌} & ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) | ||
Theorem | sopo 5292 | A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.) |
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) | ||
Theorem | soss 5293 | 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 5294 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | ||
Theorem | soeq2 5295 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) | ||
Theorem | sonr 5296 | A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | sotr 5297 | A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | solin 5298 | A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) | ||
Theorem | so2nr 5299 | A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
Theorem | so3nr 5300 | A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |