Grace/Bootstrap/Aliases.g17
Imports
None
Declarations
- empty.membership theorem derivation
- pair.membership theorem derivation
- extensionality theorem derivation
- powerset.membership theorem derivation
- foundation theorem derivation
Source
1-- Checked aliases for the primitive foundation laws, and the global ∪.2-- Elaborated before the module graph; its names form the global interface.3-- Part of the Grace17 proof assistant for mathematics based on set theory.4-- Copyright (c) 2026 Grant Olney Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78-- ∅, {x, y}, (x, y), 𝒫(A), ⋃ A, ε₀, and ℕ are read by the parser itself;9-- the binary union is the one token the bootstrap must declare.10notation infixl 60 "∪" => union21112theorem empty.membership13 shows ∀ x, x ∉ ∅14proof15 exact set.empty1617theorem pair.membership18 shows ∀ x, ∀ y, ∀ z, z ∈ {x, y} ↔ (z = x ∨ z = y)19proof20 exact set.pairing2122theorem extensionality23 shows ∀ x, ∀ y, (∀ z, z ∈ x ↔ z ∈ y) → x = y24proof25 exact set.extensionality2627theorem powerset.membership28 shows ∀ x, ∀ y, x ∈ 𝒫(y) ↔ (∀ z ∈ x, z ∈ y)29proof30 exact set.powerset3132theorem foundation33 shows ∀ x, x ≠ ∅ → (∃ y ∈ x, ∀ z ∈ y, z ∉ x)34proof35 exact set.foundation36