-- The membership order on ε₀, cut out of 𝒫(𝒫(ε₀ ∪ ε₀)) by Separation.
-- Elaborated before the module graph, after Aliases, Nat, and OrderedPair.
-- 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

def epsilon0.less : Set :=
  { p ∈ 𝒫(𝒫(ε₀ ∪ ε₀)) | ∃ x ∈ ε₀, ∃ y ∈ ε₀, x ∈ y ∧ p = (x, y) }

theorem epsilon0.less.membership (a b : Set)
  shows relates(ε₀.less, a, b) ↔ (a ∈ ε₀ ∧ b ∈ ε₀ ∧ a ∈ b)
proof
  constructor
  . intro h
    simp [relates, ε₀.less] at h
    obtain ⟨bound, x, hx, y, hy, hxy, pair⟩ := h
    obtain ⟨ha, hb⟩ := bootstrap.orderedPair.injective at a, b, x, y with pair
    rw [ha, hb]
    exact ⟨hx, hy, hxy⟩
  . intro h
    obtain ⟨ha, hb, hab⟩ := h
    have bound := bootstrap.orderedPair.bounded at a, b, ε₀, ε₀ with ha, hb
    simp [relates, ε₀.less]