ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-06 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$\mathcal{P}(\varnothing) = \{\varnothing\}$ , $\mathcal{P}(\{\varnothing\}) = \{\varnothing,\{\varnothing\}\}$ , and $\mathcal{P}(\{\varnothing,\{\varnothing\}\})$ listed in full

Example

Write $A := \{\varnothing,\{\varnothing\}\}$ , and abbreviate $\{x,y,z,w\} := \{x,y\} \cup \{z,w\}$ . Then

$\mathcal{P}(\varnothing) = \{\varnothing\}, \qquad \mathcal{P}(\{\varnothing\}) = \{\varnothing,\{\varnothing\}\}, \qquad \mathcal{P}(A) = \{\varnothing,\{\varnothing\},\{\{\varnothing\}\},A\},$

and the four sets listed in $\mathcal{P}(A)$ are pairwise distinct.

Facts & Assumptions

Given: $A := \{\varnothing,\{\varnothing\}\}$ and the abbreviation $\{x,y,z,w\} := \{x,y\} \cup \{z,w\}$ .

[L1]

$\mathcal{P}(\varnothing) = \{\varnothing\}$ ( $\mathcal{P}(\varnothing) = \{\varnothing\}$ ; $\varnothing \in \mathcal{P}(a)$ and $a \in \mathcal{P}(a)$ ; $a \subseteq b$ if and only if $\mathcal{P}(a) \subseteq \mathcal{P}(b)$ ; $\bigcup \mathcal{P}(a) = a$ ; $\bigcap \mathcal{P}(a) = \varnothing$ ; and $\mathcal{P}(a \cap b) = \mathcal{P}(a) \cap \mathcal{P}(b)$ while only $\mathcal{P}(a) \cup \mathcal{P}(b) \subseteq \mathcal{P}(a \cup b)$ holds).

[L2]

$z \in \mathcal{P}(x)$ holds if and only if $z \subseteq x$ (The power set $\mathcal{P}(x) = \{\, z : z \subseteq x \,\}$ ).

[L3]

$x \subseteq y$ means that every element of $x$ is an element of $y$ (Subset $x \subseteq y$ , proper subset $x \subsetneq y$ , and the separation notation $\{\, z \in x : \varphi(z) \,\}$ ).

[L4]

$\{x,y\}$ is the set whose elements are exactly $x$ and $y$ , and $\{x\} := \{x,x\}$ (The unordered pair $\{x,y\}$ and the singleton $\{x\} = \{x,x\}$ ).

[L5]

If every $z$ satisfies $z \in x$ if and only if $z \in y$ , then $x = y$ (The Axiom of Extensionality: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$ ).

[L6]

There is exactly one set with no elements (There is exactly one set with no elements, written $\varnothing$ ).

[L7]

$z \in a \cup b$ holds if and only if $z \in a$ or $z \in b$ ( $\bigcup \varnothing = \varnothing$ , $\bigcup \{a\} = a$ , $\bigcup \{a,b\} = a \cup b$ , $\bigcap \{a\} = a$ , and $\bigcap \{a,b\} = a \cap b$ ).

[L8]

$a \cup b := \bigcup\{a,b\}$ (The union $\bigcup x$ of a set, and the binary union $a \cup b := \bigcup \{a,b\}$ ).

Verification

technique · direct

1.1

$\mathcal{P}(\varnothing) = \{\varnothing\}$ is the general identity applied at $\varnothing$ .

1.2

A set $z$ satisfies $z \subseteq \{\varnothing\}$ exactly when every element of $z$ equals $\varnothing$ , that is, exactly when $z$ has no element or $\varnothing$ is its only element; those two sets are $\varnothing$ and $\{\varnothing\}$ , and both are indeed included in $\{\varnothing\}$ . Hence $\mathcal{P}(\{\varnothing\}) = \{\varnothing,\{\varnothing\}\}$ .

L2L3L4L5L6

1.3

A set $z$ satisfies $z \subseteq A$ exactly when every element of $z$ is $\varnothing$ or $\{\varnothing\}$ , so $z$ is determined by whether it has $\varnothing$ as an element and whether it has $\{\varnothing\}$ as an element; the four resulting sets are $\varnothing$ , $\{\varnothing\}$ , $\{\{\varnothing\}\}$ and $A$ , and each is included in $A$ . Hence $\mathcal{P}(A) = \{\varnothing,\{\varnothing\},\{\{\varnothing\}\},A\}$ .

L2L3L4L5L6L7L8

1.4

The four are pairwise distinct: $\varnothing$ has no element, $\{\varnothing\}$ has $\varnothing$ as its only element, $\{\{\varnothing\}\}$ has $\{\varnothing\}$ as its only element, and $A$ has both; moreover $\varnothing \neq \{\varnothing\}$ , since the second has an element and the first does not.

L4L5L6

2.1

The three power sets are computed and the four members of $\mathcal{P}(A)$ are distinct, which is the example.

step 1.1step 1.2step 1.3step 1.4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 17 results over 7 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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

P(∅)={∅}\mathcal{P}(\varnothing) = \{\varnothing\}P(∅)={∅}, P({∅})={∅,{∅}}\mathcal{P}(\{\varnothing\}) = \{\varnothing,\{\varnothing\}\}P({∅})={∅,{∅}}, and P({∅,{∅}})\mathcal{P}(\{\varnothing,\{\varnothing\}\})P({∅,{∅}}) listed in full