Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-adaptedprecheck 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.

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

Statement

For all sets a and b:

  • (i) P(∅)={∅};
  • (ii) ∅∈P(a) and a∈P(a);
  • (iii) a⊆b if and only if P(a)⊆P(b);
  • (iv) ⋃P(a)=a;
  • (v) ⋂P(a)=∅;
  • (vi) P(a∩b)=P(a)∩P(b);
  • (vii) P(a)∪P(b)⊆P(a∪b);
  • (viii) the inclusion in (vii) is an equality if and only if a⊆b or b⊆a.

Facts & Assumptions

Given: sets a and b.

[L1]

z∈P(x) holds if and only if z⊆x (The power set P(x)={ z:z⊆x }).

[L6]

⋃x is the set whose elements are exactly the elements of the elements of x (The union ⋃x of a set, and the binary union a∪b:=⋃{a,b}).

[L7]

For x≠∅, ⋂x is the set whose elements are exactly the sets belonging to every element of x (The intersection ⋂x of a nonempty set, the binary intersection a∩b:=⋂{a,b}, and disjointness).

[L10]

There is exactly one set with no elements, written ∅ (There is exactly one set with no elements, written ∅).

[L11]

{x}:={x,x}, the singleton of x, is the set whose only element is x (The unordered pair {x,y} and the singleton {x}={x,x}).

[L12]

If every z satisfies z∈x if and only if z∈y, then x=y (The Axiom of Extensionality: ∀x ∀y (∀z (z∈x↔z∈y)→x=y)).

Proof

technique · direct
1.1

Claim (i): z∈P(∅) holds exactly when z⊆∅, that is, when every element of z lies in ∅; since ∅ has no elements this says z has no elements, hence z=∅. So the elements of P(∅) are exactly ∅, and P(∅)={∅}.

L1L2L10L11L12
1.2

Claim (ii): ∅⊆a and a⊆a, so both ∅ and a are elements of P(a).

L1L3L4
1.3

Claim (iii): if a⊆b and z∈P(a), then z⊆a and a⊆b give z⊆b, so z∈P(b); conversely if P(a)⊆P(b) then a∈P(a), since a⊆a, so a∈P(b), which says a⊆b.

L1L2L4L5
1.4

Claim (iv): z∈⋃P(a) holds exactly when z belongs to some element of P(a), that is, to some s with s⊆a, and any such z lies in a; conversely if z∈a then z lies in the element a of P(a). So the two sets have the same elements.

L1L2L4L6L12
1.5

Claim (v): ∅∈P(a), so P(a)≠∅ and ⋂P(a) is defined; an element of it would have to belong to every element of P(a), in particular to ∅, which has no elements. So ⋂P(a) has no elements and equals ∅.

L1L3L7L10
1.6

Claim (vi): z∈P(a∩b) holds exactly when every element of z lies in a∩b, that is, lies in a and in b; this is exactly z⊆a together with z⊆b, that is, z∈P(a) and z∈P(b), which is z∈P(a)∩P(b).

L1L2L9L12
1.7

Claim (vii): if z∈P(a)∪P(b) then z⊆a or z⊆b; in either case every element of z lies in a or in b, hence in a∪b, so z∈P(a∪b).

L1L2L8
2.1

Claim (viii): if a⊆b then the elements of a∪b are exactly those of b, so z⊆a∪b is equivalent to z⊆b and P(a∪b)=P(b)⊆P(a)∪P(b), which with the reverse inclusion gives equality; the case b⊆a is symmetric. Conversely, if equality holds then a∪b⊆a∪b puts a∪b in P(a)∪P(b), so a∪b⊆a or a∪b⊆b, and since b⊆a∪b and a⊆a∪b these give b⊆a and a⊆b respectively.

L1L2L4L5L8step 1.7
3.1

Claims (i) to (viii) are established, which is the statement.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 1.7step 2.1∎

Depends on

Used by

Dependency tree · two levels

15 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