The power set $\mathcal{P}(x)=\{z:z\subseteq x\}$

Depends on

• For every set $x$ there is exactly one set whose elements are precisely the subsets of $x$
• Subset $x \subseteq y$, proper subset $x \subsetneq y$, and the separation notation $\{\, z \in x : \varphi(z) \,\}$

Used by

• For a nonempty index set I: B ∩ ⋃_i ∈ I Aᵢ = ⋃_i ∈ I (B ∩ Aᵢ), B ∪ ⋂_i ∈ I Aᵢ = ⋂_i ∈ I (B ∪ Aᵢ), X ∖ ⋃_i ∈ I Aᵢ = ⋂_i ∈ I (X ∖ Aᵢ), and X ∖ ⋂_i ∈ I Aᵢ = ⋃_i ∈ I (X ∖ Aᵢ) Corollary
• Sets a and b with P(a) ∪ P(b) ⊊ P(a ∪ b) Counterexample
• Balanced bracket words, defined by the recursive grammar Definition
• Binary trees, defined recursively, and their size Definition
• Boundable sentences over an atom set Definition
• Choice function Definition
• Epsilon-NFAs, finite epsilon closure, and extended word transition Definition
• Equivalence relation, equivalence class, and the quotient set A/∼ Definition
• Filter on a set Definition
• Nondeterministic finite automata with epsilon-moves Definition
• The Cartesian product A × B := { z ∈ P(P(A ∪ B)) : ∃ a ∈ A ∃ b ∈ B z = (a,b) } Definition
• {∅} × {∅,{∅}} listed in full, together with the inclusion in P(P(A ∪ B)) that makes it a set Example
• Adjoining one of two fixed points defines commuting closure-operator monads whose distributive law yields their composite 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
• Singletons define a natural transformation from the identity functor on sets to the covariant power-set functor Example
• The power-set functor is lax monoidal but not strong Example
• The self-adjunction of the contravariant power-set functor induces the double-power-set monad Example
• FALSE: every lax monoidal functor has invertible structure maps False statement
• Dependent choice implies countable choice Lemma
• Direct and inverse image satisfy Beck–Chevalley for pullback squares of sets Lemma
• For sets A and B the collection of all functions A → B is a set, being a subset of P(A × B) Lemma
• If a ∈ A and b ∈ B then (a,b) ∈ P(P(A ∪ B)) Lemma
• The equivalence classes of an equivalence relation are nonempty, cover A, and are pairwise equal or disjoint; conversely every such cover arises from exactly one equivalence relation Lemma
• 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
• The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes Remark
• a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) and a ∪ (b ∩ c) = (a ∪ b) ∩ (a ∪ c); and for a nonempty set F, a ∩ ⋃ F = ⋃ { a ∩ b : b ∈ F } and a ∪ ⋂ F = ⋂ { a ∪ b : b ∈ F } Theorem
• Let ∼ be an equivalence relation on A with quotient map π : A → A/∼, and let f : A → B. There is a function g : A/∼ → B with g ∘ π = f if and only if a ∼ a' implies f(a) = f(a'); and such a g is then unique Theorem
• On a set A, R ↦ R ∖ Δ_A and S ↦ S ∪ Δ_A are mutually inverse bijections between the partial orders on A and the irreflexive, transitive relations on A; R ∖ Δ_A is the strict order of R, and every irreflexive transitive relation is asymmetric Theorem
• Singleton and union define the covariant power-set monad Theorem
• The contravariant power-set functor is monadic Theorem
• X ∖ (a ∪ b) = (X ∖ a) ∩ (X ∖ b) and X ∖ (a ∩ b) = (X ∖ a) ∪ (X ∖ b); and for a nonempty set F, X ∖ ⋃ F = ⋂ { X ∖ a : a ∈ F } and X ∖ ⋂ F = ⋃ { X ∖ a : a ∈ F } Theorem

Dependency tree · two levels

6 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

• Power set (Wikipedia) (standard reference, not scraped)
• B. Kaya, MATH 320 Set Theory (METU), Axiom 6 (standard reference, not scraped)
• C. Wilson, A Brief Introduction to ZFC (Chicago REU 2016), §2.3 (standard reference, not scraped)