Home | New
Foundations Explorer Theorem List (p. 41 of 64) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > NFE Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfiun2 4001* | Alternate definition of indexed union when B is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ B ∈ V ⇒ ⊢ ∪x ∈ A B = ∪{y ∣ ∃x ∈ A y = B} | ||
Theorem | dfiin2 4002* | Alternate definition of indexed intersection when B is a set. Definition 15(b) of [Suppes] p. 44. (Contributed by NM, 28-Jun-1998.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ B ∈ V ⇒ ⊢ ∩x ∈ A B = ∩{y ∣ ∃x ∈ A y = B} | ||
Theorem | cbviun 4003* | Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.) |
⊢ ℲyB & ⊢ ℲxC & ⊢ (x = y → B = C) ⇒ ⊢ ∪x ∈ A B = ∪y ∈ A C | ||
Theorem | cbviin 4004* | Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ ℲyB & ⊢ ℲxC & ⊢ (x = y → B = C) ⇒ ⊢ ∩x ∈ A B = ∩y ∈ A C | ||
Theorem | cbviunv 4005* | Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.) |
⊢ (x = y → B = C) ⇒ ⊢ ∪x ∈ A B = ∪y ∈ A C | ||
Theorem | cbviinv 4006* | Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) |
⊢ (x = y → B = C) ⇒ ⊢ ∩x ∈ A B = ∩y ∈ A C | ||
Theorem | iunss 4007* | Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∪x ∈ A B ⊆ C ↔ ∀x ∈ A B ⊆ C) | ||
Theorem | ssiun 4008* | Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∃x ∈ A C ⊆ B → C ⊆ ∪x ∈ A B) | ||
Theorem | ssiun2 4009 | Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (x ∈ A → B ⊆ ∪x ∈ A B) | ||
Theorem | ssiun2s 4010* | Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.) |
⊢ (x = C → B = D) ⇒ ⊢ (C ∈ A → D ⊆ ∪x ∈ A B) | ||
Theorem | iunss2 4011* | A subclass condition on the members of two indexed classes C(x) and D(y) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59. Compare uniss2 3922. (Contributed by NM, 9-Dec-2004.) |
⊢ (∀x ∈ A ∃y ∈ B C ⊆ D → ∪x ∈ A C ⊆ ∪y ∈ B D) | ||
Theorem | iunab 4012* | The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.) |
⊢ ∪x ∈ A {y ∣ φ} = {y ∣ ∃x ∈ A φ} | ||
Theorem | iunrab 4013* | The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
⊢ ∪x ∈ A {y ∈ B ∣ φ} = {y ∈ B ∣ ∃x ∈ A φ} | ||
Theorem | iunxdif2 4014* | Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004.) |
⊢ (x = y → C = D) ⇒ ⊢ (∀x ∈ A ∃y ∈ (A ∖ B)C ⊆ D → ∪y ∈ (A ∖ B)D = ∪x ∈ A C) | ||
Theorem | ssiinf 4015 | Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.) |
⊢ ℲxC ⇒ ⊢ (C ⊆ ∩x ∈ A B ↔ ∀x ∈ A C ⊆ B) | ||
Theorem | ssiin 4016* | Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003.) |
⊢ (C ⊆ ∩x ∈ A B ↔ ∀x ∈ A C ⊆ B) | ||
Theorem | iinss 4017* | Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∃x ∈ A B ⊆ C → ∩x ∈ A B ⊆ C) | ||
Theorem | iinss2 4018 | An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.) |
⊢ (x ∈ A → ∩x ∈ A B ⊆ B) | ||
Theorem | uniiun 4019* | Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.) |
⊢ ∪A = ∪x ∈ A x | ||
Theorem | intiin 4020* | Class intersection in terms of indexed intersection. Definition in [Stoll] p. 44. (Contributed by NM, 28-Jun-1998.) |
⊢ ∩A = ∩x ∈ A x | ||
Theorem | iunid 4021* | An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.) |
⊢ ∪x ∈ A {x} = A | ||
Theorem | iun0 4022 | An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ∪x ∈ A ∅ = ∅ | ||
Theorem | 0iun 4023 | An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ∪x ∈ ∅ A = ∅ | ||
Theorem | 0iin 4024 | An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.) |
⊢ ∩x ∈ ∅ A = V | ||
Theorem | viin 4025* | Indexed intersection with a universal index class. When A doesn't depend on x, this evaluates to A by 19.3 1785 and abid2 2470. When A = x, this evaluates to ∅ by intiin 4020 and intv in set.mm. (Contributed by NM, 11-Sep-2008.) |
⊢ ∩x ∈ V A = {y ∣ ∀x y ∈ A} | ||
Theorem | iunn0 4026* | There is a nonempty class in an indexed collection B(x) iff the indexed union of them is nonempty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∃x ∈ A B ≠ ∅ ↔ ∪x ∈ A B ≠ ∅) | ||
Theorem | iinab 4027* | Indexed intersection of a class builder. (Contributed by NM, 6-Dec-2011.) |
⊢ ∩x ∈ A {y ∣ φ} = {y ∣ ∀x ∈ A φ} | ||
Theorem | iinrab 4028* | Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.) |
⊢ (A ≠ ∅ → ∩x ∈ A {y ∈ B ∣ φ} = {y ∈ B ∣ ∀x ∈ A φ}) | ||
Theorem | iinrab2 4029* | Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.) |
⊢ (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = {y ∈ B ∣ ∀x ∈ A φ} | ||
Theorem | iunin2 4030* | Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4019 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) |
⊢ ∪x ∈ A (B ∩ C) = (B ∩ ∪x ∈ A C) | ||
Theorem | iunin1 4031* | Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4019 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ∪x ∈ A (C ∩ B) = (∪x ∈ A C ∩ B) | ||
Theorem | iinun2 4032* | Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4020 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.) |
⊢ ∩x ∈ A (B ∪ C) = (B ∪ ∩x ∈ A C) | ||
Theorem | iundif2 4033* | Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 4020 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.) |
⊢ ∪x ∈ A (B ∖ C) = (B ∖ ∩x ∈ A C) | ||
Theorem | 2iunin 4034* | Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.) |
⊢ ∪x ∈ A ∪y ∈ B (C ∩ D) = (∪x ∈ A C ∩ ∪y ∈ B D) | ||
Theorem | iindif2 4035* | Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 4019 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.) |
⊢ (A ≠ ∅ → ∩x ∈ A (B ∖ C) = (B ∖ ∪x ∈ A C)) | ||
Theorem | iinin2 4036* | Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4020 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (A ≠ ∅ → ∩x ∈ A (B ∩ C) = (B ∩ ∩x ∈ A C)) | ||
Theorem | iinin1 4037* | Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4020 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (A ≠ ∅ → ∩x ∈ A (C ∩ B) = (∩x ∈ A C ∩ B)) | ||
Theorem | elriin 4038* | Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (B ∈ (A ∩ ∩x ∈ X S) ↔ (B ∈ A ∧ ∀x ∈ X B ∈ S)) | ||
Theorem | riin0 4039* | Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (X = ∅ → (A ∩ ∩x ∈ X S) = A) | ||
Theorem | riinn0 4040* | Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((∀x ∈ X S ⊆ A ∧ X ≠ ∅) → (A ∩ ∩x ∈ X S) = ∩x ∈ X S) | ||
Theorem | riinrab 4041* | Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (A ∩ ∩x ∈ X {y ∈ A ∣ φ}) = {y ∈ A ∣ ∀x ∈ X φ} | ||
Theorem | iinxsng 4042* | A singleton index picks out an instance of an indexed intersection's argument. (Contributed by NM, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ (x = A → B = C) ⇒ ⊢ (A ∈ V → ∩x ∈ {A}B = C) | ||
Theorem | iinxprg 4043* | Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.) |
⊢ (x = A → C = D) & ⊢ (x = B → C = E) ⇒ ⊢ ((A ∈ V ∧ B ∈ W) → ∩x ∈ {A, B}C = (D ∩ E)) | ||
Theorem | iunxsng 4044* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) |
⊢ (x = A → B = C) ⇒ ⊢ (A ∈ V → ∪x ∈ {A}B = C) | ||
Theorem | iunxsn 4045* | A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 25-Jun-2016.) |
⊢ A ∈ V & ⊢ (x = A → B = C) ⇒ ⊢ ∪x ∈ {A}B = C | ||
Theorem | iunun 4046 | Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ∪x ∈ A (B ∪ C) = (∪x ∈ A B ∪ ∪x ∈ A C) | ||
Theorem | iunxun 4047 | Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ∪x ∈ (A ∪ B)C = (∪x ∈ A C ∪ ∪x ∈ B C) | ||
Theorem | iunxiun 4048* | Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.) |
⊢ ∪x ∈ ∪ y ∈ A BC = ∪y ∈ A ∪x ∈ B C | ||
Theorem | iinuni 4049* | A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ (A ∪ ∩B) = ∩x ∈ B (A ∪ x) | ||
Theorem | iununi 4050* | A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ((B = ∅ → A = ∅) ↔ (A ∪ ∪B) = ∪x ∈ B (A ∪ x)) | ||
Theorem | sspwuni 4051 | Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
⊢ (A ⊆ ℘B ↔ ∪A ⊆ B) | ||
Theorem | pwssb 4052* | Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.) |
⊢ (A ⊆ ℘B ↔ ∀x ∈ A x ⊆ B) | ||
Theorem | elpwuni 4053 | Relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
⊢ (B ∈ A → (A ⊆ ℘B ↔ ∪A = B)) | ||
Theorem | iinpw 4054* | The power class of an intersection in terms of indexed intersection. Exercise 24(a) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.) |
⊢ ℘∩A = ∩x ∈ A ℘x | ||
Theorem | iunpwss 4055* | Inclusion of an indexed union of a power class in the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) |
⊢ ∪x ∈ A ℘x ⊆ ℘∪A | ||
Theorem | rintn0 4056 | Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Revised by Mario Carneiro, 5-Jun-2015.) |
⊢ ((X ⊆ ℘A ∧ X ≠ ∅) → (A ∩ ∩X) = ∩X) | ||
Syntax | copk 4057 | Extend class notation to include Kuratowski ordered pair. |
class ⟪A, B⟫ | ||
Definition | df-opk 4058 | Define the Kuratowski ordered pair. This ordered pair definition is standard for ZFC set theory, but we do not use it beyond establishing df-op 4566, since it is not type-level. We state this definition since it is a simple definition that can be used by the set construction axioms that follow this section. (Contributed by SF, 12-Jan-2015.) |
⊢ ⟪A, B⟫ = {{A}, {A, B}} | ||
Theorem | opkeq1 4059 | Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) |
⊢ (A = B → ⟪A, C⟫ = ⟪B, C⟫) | ||
Theorem | opkeq2 4060 | Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) |
⊢ (A = B → ⟪C, A⟫ = ⟪C, B⟫) | ||
Theorem | opkeq12 4061 | Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.) |
⊢ ((A = C ∧ B = D) → ⟪A, B⟫ = ⟪C, D⟫) | ||
Theorem | opkeq1i 4062 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ A = B ⇒ ⊢ ⟪A, C⟫ = ⟪B, C⟫ | ||
Theorem | opkeq2i 4063 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ A = B ⇒ ⊢ ⟪C, A⟫ = ⟪C, B⟫ | ||
Theorem | opkeq12i 4064 | Equality inference for ordered pairs. (The proof was shortened by Eric Schmidt, 4-Apr-2007.) (Contributed by NM, 16-Dec-2006.) |
⊢ A = B & ⊢ C = D ⇒ ⊢ ⟪A, C⟫ = ⟪B, D⟫ | ||
Theorem | opkeq1d 4065 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ (φ → A = B) ⇒ ⊢ (φ → ⟪A, C⟫ = ⟪B, C⟫) | ||
Theorem | opkeq2d 4066 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ (φ → A = B) ⇒ ⊢ (φ → ⟪C, A⟫ = ⟪C, B⟫) | ||
Theorem | opkeq12d 4067 | Equality deduction for ordered pairs. (The proof was shortened by Andrew Salmon, 29-Jun-2011.) (Contributed by NM, 16-Dec-2006.) |
⊢ (φ → A = B) & ⊢ (φ → C = D) ⇒ ⊢ (φ → ⟪A, C⟫ = ⟪B, D⟫) | ||
Theorem | nfopk 4068 | Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.) |
⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx⟪A, B⟫ | ||
Theorem | compldif 4069 | Complement in terms of difference. (Contributed by SF, 2-Jan-2018.) |
⊢ ∼ A = (V ∖ A) | ||
Theorem | complV 4070 | The complement of the universe is the empty set. (Contributed by SF, 2-Jan-2018.) |
⊢ ∼ V = ∅ | ||
Theorem | compl0 4071 | The complement of the empty set is the universe. (Contributed by SF, 2-Jan-2018.) |
⊢ ∼ ∅ = V | ||
Theorem | nincompl 4072 | Anti-intersection with complement. (Contributed by SF, 2-Jan-2018.) |
⊢ (A ⩃ ∼ A) = V | ||
Theorem | incompl 4073 | Intersection with complement. (Contributed by SF, 2-Jan-2018.) |
⊢ (A ∩ ∼ A) = ∅ | ||
Theorem | uncompl 4074 | Union with complement. (Contributed by SF, 2-Jan-2018.) |
⊢ (A ∪ ∼ A) = V | ||
Theorem | inindif 4075 | The intersection of an intersection and a difference is empty. (Contributed by set.mm contributors, 10-Mar-2015.) |
⊢ ((A ∩ B) ∩ (A ∖ B)) = ∅ | ||
Theorem | ssofss 4076* | Condition for subset when A is already known to be a subset. (Contributed by SF, 13-Jan-2015.) |
⊢ (A ⊆ C → (A ⊆ B ↔ ∀x ∈ C (x ∈ A → x ∈ B))) | ||
Theorem | ssofeq 4077* | When A and B are subsets of C, equality depends only on the elements of C. (Contributed by SF, 13-Jan-2015.) |
⊢ ((A ⊆ C ∧ B ⊆ C) → (A = B ↔ ∀x ∈ C (x ∈ A ↔ x ∈ B))) | ||
Axiom | ax-nin 4078* |
State the axiom of anti-intersection. Axiom P1 of [Hailperin] p. 6.
This axiom sets up boolean operations on sets.
Note on this and the following axioms: this axiom, ax-xp 4079, ax-cnv 4080, ax-1c 4081, ax-sset 4082, ax-si 4083, ax-ins2 4084, ax-ins3 4085, and ax-typlower 4086 are from Hailperin and are designed to implement the Stratification Axiom of Quine. A well-formed formula using only propositional symbols, predicate symbols, and ∈ is "stratified" iff you can make a (metalogical) mapping from the variables to the natural numbers such that any formulas of the form x = y have the same number, and any formulas of the form x ∈ y have x as one less than y. Quine's stratification axiom states that there is a set corresponding to any stratified formula. Since we cannot state stratification from within the logic, we use Hailperin's axioms and prove existence of stratified sets using Hailperin's algorithm. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃z∀w(w ∈ z ↔ (w ∈ x ⊼ w ∈ y)) | ||
Axiom | ax-xp 4079* | State the axiom of cross product. This axiom guarantees the existence of the (Kuratowski) cross product of V with x. Axiom P5 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃y∀z(z ∈ y ↔ ∃w∃t(z = ⟪w, t⟫ ∧ t ∈ x)) | ||
Axiom | ax-cnv 4080* | State the axiom of converse. This axiom guarantees the existence of the Kuratowski converse of x. Axiom P7 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃y∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x) | ||
Axiom | ax-1c 4081* | State the axiom of cardinal one. This axiom guarantees the existence of the set of all singletons, which will become cardinal one later in our development. Axiom P8 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)) | ||
Axiom | ax-sset 4082* | State the axiom of the subset relationship. This axiom guarantees the existence of the Kuratowski relationship representing subset. Slight generalization of axiom P9 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃x∀y∀z(⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z)) | ||
Axiom | ax-si 4083* | State the axiom of the singleton image. This axiom guarantees that guarantees the existence of a set that raises the "type" of another set when considered as a relationship. Axiom P2 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃y∀z∀w(⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ x) | ||
Axiom | ax-ins2 4084* | State the insertion two axiom. This axiom sets up a set that inserts an extra variable at the second place of the relationship described by x. Axiom P3 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x) | ||
Axiom | ax-ins3 4085* | State the insertion three axiom. This axiom sets up a set that inserts an extra variable at the third place of the relationship described by x. Axiom P4 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, w⟫ ∈ x) | ||
Axiom | ax-typlower 4086* | The type lowering axiom. This axiom eventually sets up both the existence of the sum set and the existence of the range of a relationship. Axiom P6 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃y∀z(z ∈ y ↔ ∀w⟪w, {z}⟫ ∈ x) | ||
Axiom | ax-sn 4087* | The singleton axiom. This axiom sets up the existence of a singleton set. This appears to have been an oversight on Hailperin's part, as it is needed to prove the properties of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.) |
⊢ ∃y∀z(z ∈ y ↔ z = x) | ||
Theorem | axprimlem1 4088* | Lemma for the primitive axioms. Primitive form of equality to a singleton. (Contributed by SF, 25-Mar-2015.) |
⊢ (a = {B} ↔ ∀c(c ∈ a ↔ c = B)) | ||
Theorem | axprimlem2 4089* | Lemma for the primitive axioms. Primitive form of equality to a Kuratowski ordered pair. (Contributed by SF, 25-Mar-2015.) |
⊢ (a = ⟪B, C⟫ ↔ ∀d(d ∈ a ↔ (∀e(e ∈ d ↔ e = B) ∨ ∀f(f ∈ d ↔ (f = B ∨ f = C))))) | ||
Theorem | axxpprim 4090* | ax-xp 4079 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.) |
⊢ ∃y∀z(z ∈ y ↔ ∃w∃t(∀a(a ∈ z ↔ (∀b(b ∈ a ↔ b = w) ∨ ∀c(c ∈ a ↔ (c = w ∨ c = t)))) ∧ t ∈ x)) | ||
Theorem | axcnvprim 4091* | ax-cnv 4080 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.) |
⊢ ∃y∀z∀w(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ c = z) ∨ ∀d(d ∈ b ↔ (d = z ∨ d = w)))) ∧ a ∈ y) ↔ ∃e(∀f(f ∈ e ↔ (∀g(g ∈ f ↔ g = w) ∨ ∀h(h ∈ f ↔ (h = w ∨ h = z)))) ∧ e ∈ x)) | ||
Theorem | axssetprim 4092* | ax-sset 4082 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.) |
⊢ ∃x∀y∀z(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ c = y) ∨ ∀d(d ∈ b ↔ (d = y ∨ d = z)))) ∧ a ∈ x) ↔ ∀e(e ∈ y → e ∈ z)) | ||
Theorem | axsiprim 4093* | ax-si 4083 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.) |
⊢ ∃y∀z∀w(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ d = z)) ∨ ∀e(e ∈ b ↔ (∀f(f ∈ e ↔ f = z) ∨ ∀g(g ∈ e ↔ g = w))))) ∧ a ∈ y) ↔ ∃h(∀i(i ∈ h ↔ (∀j(j ∈ i ↔ j = z) ∨ ∀k(k ∈ i ↔ (k = z ∨ k = w)))) ∧ h ∈ x)) | ||
Theorem | axtyplowerprim 4094* | ax-typlower 4086 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.) |
⊢ ∃y∀z(z ∈ y ↔ ∀w∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ c = w) ∨ ∀d(d ∈ b ↔ (d = w ∨ ∀e(e ∈ d ↔ e = z))))) ∧ a ∈ x)) | ||
Theorem | axins2prim 4095* | ax-ins2 4084 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.) |
⊢ ∃y∀z∀w∀t(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x)) | ||
Theorem | axins3prim 4096* | ax-ins3 4085 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.) |
⊢ ∃y∀z∀w∀t(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = w)))) ∧ k ∈ x)) | ||
Theorem | ninexg 4097 | The anti-intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.) |
⊢ ((A ∈ V ∧ B ∈ W) → (A ⩃ B) ∈ V) | ||
Theorem | ninex 4098 | The anti-intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A ⩃ B) ∈ V | ||
Theorem | complexg 4099 | The complement of a set is a set. (Contributed by SF, 12-Jan-2015.) |
⊢ (A ∈ V → ∼ A ∈ V) | ||
Theorem | inexg 4100 | The intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.) |
⊢ ((A ∈ V ∧ B ∈ W) → (A ∩ B) ∈ V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |