The unordered pair $\{x,y\}$ and the singleton $\{x\}=\{x,x\}$

Depends on

• The Axiom of Pairing: $\forall x\,\forall y\,\exists z\,\forall t\,(t \in z \leftrightarrow (t = x \vee t = y))$
• The Axiom of Extensionality: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$

Used by

• For f : A → B: S ⊆ f⁻¹[f[S]] for every S ⊆ A, with equality for every such S if and only if f is injective; and f[f⁻¹[T]] = T ∩ f[A] for every T ⊆ B, so equality with T holds for every such T if and only if f is surjective Corollary
• If x ∪ {x} = y ∪ {y} then x = y Corollary
• A function f and sets S, T with f[S ∩ T] ⊊ f[S] ∩ f[T] Counterexample
• A symmetric and transitive relation on a two-element set that is not reflexive on it Counterexample
• Relations R and S on a two-element set with S ∘ R ≠ R ∘ S Counterexample
• Sets a and b with P(a) ∪ P(b) ⊊ P(a ∪ b) Counterexample
• Sets A, B, C with (A × B) × C ≠ A × (B × C) Counterexample
• Sets with (A × C) ∪ (B × D) ⊊ (A ∪ B) × (C ∪ D) Counterexample
• Inductive set Definition
• The intersection ⋂ x of a nonempty set, the binary intersection a ∩ b := ⋂{a,b}, and disjointness Definition
• The Kuratowski ordered pair (a,b) := {{a},{a,b}} Definition
• The union ⋃ x of a set, and the binary union a ∪ b := ⋃ {a,b} Definition
• (∅,∅) = {{∅}} and (∅,{∅}) = {{∅},{∅,{∅}}}, with the characterising property checked on them Example
• {∅} × {∅,{∅}} listed in full, together with the inclusion in P(P(A ∪ B)) that makes it a set Example
• ∅ is a relation on every set, is the unique equivalence relation on ∅, is a function ∅ → B for every B, is a bijection ∅ → ∅, and is not a surjection ∅ → {∅} Example
• ⋃ ⋂ (a,b) = a for all a and b, and ⋃(a,b) = {a,b}, so both coordinates are recovered from the pair as a set Example
• A four-pair relation on {∅,{∅},{∅,{∅}}} with its domain, range, field, inverse, restriction, image and self-composite computed Example
• A two-cell partition of a three-element set, the equivalence relation it induces listed pair by pair, and the quotient set recovered from it Example
• A two-to-one function on a four-element set, its kernel, the quotient, and the canonical factorisation computed explicitly Example
• For any indexed family the product ∏_i ∈ I P(Xᵢ) contains the constant function with value ∅, and ∏_i ∈ I {i} has exactly one element Example
• P(∅) = {∅}, P({∅}) = {∅,{∅}}, and P({∅,{∅}}) listed in full Example
• The distributive and exponential laws of sets are natural isomorphisms Example
• FALSE: (a ∖ b) ∖ c = a ∖ (b ∖ c) for all sets a, b, c False statement
• FALSE: a symmetric and transitive relation on a set A is reflexive on A, so reflexivity is redundant in the definition of an equivalence relation False statement
• {a,b} = {c,d} if and only if (a = c and b = d) or (a = d and b = c); in particular {a} = {c,d} if and only if a = c = d Lemma
• ⋃ ∅ = ∅, ⋃ {a} = a, ⋃ {a,b} = a ∪ b, ⋂ {a} = a, and ⋂ {a,b} = a ∩ b Lemma
• For I = {∅,{∅}} with A_∅ = A and A_{∅} = B, the map f ↦ (f(∅), f({∅})) is a bijection ∏_i ∈ I Aᵢ → A × B Lemma
• If a ∈ A and b ∈ B then (a,b) ∈ P(P(A ∪ B)) Lemma
• If every element of R is an ordered pair, then { a : ∃ b (a,b) ∈ R } and { b : ∃ a (a,b) ∈ R } are sets, both included in ⋃⋃ R Lemma
• ∏_i ∈ ∅ Aᵢ = {∅}; if Aⱼ = ∅ for some j ∈ I then ∏_i ∈ I Aᵢ = ∅; and for I = {j} the evaluation f ↦ f(j) is a bijection ∏_i ∈ I Aᵢ → Aⱼ Proposition
• A weighted limit of a set-valued diagram is the set of natural transformations from the weight Proposition
• For f : A → B and S, T ⊆ A: f[S ∪ T] = f[S] ∪ f[T], f[S ∩ T] ⊆ f[S] ∩ f[T] and f[S] ∖ f[T] ⊆ f[S ∖ T]; both inclusions are equalities for all S and T if and only if f is injective Proposition
• P(∅) = {∅}; ∅ ∈ P(a) and a ∈ P(a); a ⊆ b if and only if P(a) ⊆ P(b); ⋃ P(a) = a; ⋂ P(a) = ∅; and P(a ∩ b) = P(a) ∩ P(b) while only P(a) ∪ P(b) ⊆ P(a ∪ b) holds Proposition
• (a,b) = (c,d) if and only if a = c and b = d Theorem
• Under Foundation, x ∉ x for every set x, there are no sets with x ∈ y ∈ x, and there are no sets with x ∈ y ∈ z ∈ x Theorem
• Weighting by the constant singleton gives exactly the ordinary limit Theorem

Dependency tree · two levels

3 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

• B. Kaya, MATH 320 Set Theory (METU), §1.2 (standard reference, not scraped)
• Axiom of pairing (Wikipedia) (standard reference, not scraped)
• C. Wilson, A Brief Introduction to ZFC (Chicago REU 2016), §2.2 (standard reference, not scraped)