-- Checked aliases for the primitive foundation laws, and the global ∪.
-- Elaborated before the module graph; its names form the global interface.
-- Part of the Grace17 proof assistant for mathematics based on set theory.
-- Copyright (c) 2026 Grant Olney Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

-- ∅, {x, y}, (x, y), 𝒫(A), ⋃ A, ε₀, and ℕ are read by the parser itself;
-- the binary union is the one token the bootstrap must declare.
notation infixl 60 "∪" => union2

theorem empty.membership
  shows ∀ x, x ∉ ∅
proof
  exact set.empty

theorem pair.membership
  shows ∀ x, ∀ y, ∀ z, z ∈ {x, y} ↔ (z = x ∨ z = y)
proof
  exact set.pairing

theorem extensionality
  shows ∀ x, ∀ y, (∀ z, z ∈ x ↔ z ∈ y) → x = y
proof
  exact set.extensionality

theorem powerset.membership
  shows ∀ x, ∀ y, x ∈ 𝒫(y) ↔ (∀ z ∈ x, z ∈ y)
proof
  exact set.powerset

theorem foundation
  shows ∀ x, x ≠ ∅ → (∃ y ∈ x, ∀ z ∈ y, z ∉ x)
proof
  exact set.foundation