Norman Megill has been producing shorter and shorter expansions of Metamath's ax-groth to set-theory primitives; below is a summary of his work so far.
Note that some URLs here point to pages on the development site of Metamath, and may change or disappear at any time.
Last update: 4:13 PM 6/29/2007
⊢ ∃y(x ∈ y ⋀ ∀z ∈ y (∀w(w ⊆ z → w ∈ y) ⋀ ∃w ∈ y ∀v(v ⊆ z → v ∈ w)) ⋀ ∀z(z ⊆ y → (z ≈ y ⋁ z ∈ y)))
163 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → ∃v(v ∈ y ⋀ ∀w(∀u(u ∈ w → u ∈ z) → (w ∈ y ⋀ w ∈ v)))) ⋀ ∃w((w ∈ z → w ∈ y) → (∀v((v ∈ z → ∃t∀u(∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = v ⋁ h = u))) → u = t)) ⋀ (v ∈ y → (v ∈ z ⋁ ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = u ⋁ h = v))))))) ⋁ z ∈ y))))
179 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ ∃w((w ∈ z → w ∈ y) → (∀v((v ∈ z → ∃t∀u(∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = v ⋁ h = u))) → u = t)) ⋀ (v ∈ y → (v ∈ z ⋁ ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = u ⋁ h = v))))))) ⋁ z ∈ y))))
181 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ (∀w(w ∈ z → w ∈ y) → (∃w∀v((v ∈ z → ∃t∀u(∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = v ⋁ h = u))) → u = t)) ⋀ (v ∈ y → (v ∈ z ⋁ ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = u ⋁ h = v))))))) ⋁ z ∈ y))))
194 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ (∀w(w ∈ z → w ∈ y) → (∃w∀v((v ∈ z → ∃t∀u(((u ∈ y ⋀ ¬ u ∈ z) ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = v ⋁ h = u)))) → u = t)) ⋀ (v ∈ y → (v ∈ z ⋁ ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = u ⋁ h = v))))))) ⋁ z ∈ y))))
195 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ (∀w(w ∈ z → w ∈ y) → (∃w∀v((v ∈ z → ∃t∀u(((u ∈ y ⋀ ¬ u ∈ z) ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = v ⋁ h = u)))) → u = t)) ⋀ ((v ∈ y ⋀ ¬ v ∈ z) → ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = u ⋁ h = v)))))) ⋁ z ∈ y))))
197 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ (∀w(w ∈ z → w ∈ y) → (∃w∀v(∃t∀u(∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = v ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u))))) → u = t) ⋀ (v ∈ y → ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = u ⋁ ∀f(f ∈ h ↔ (f = u ⋁ f = v)))))))) ⋁ z ∈ y))))
209 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ (∀w(w ∈ z → w ∈ y) → (∃w∀v((v ∈ z → ∃t∀u((u ∈ y ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = v ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u)))))) ↔ u = t)) ⋀ (v ∈ y → ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = u ⋁ ∀f(f ∈ h ↔ (f = u ⋁ f = v)))))))) ⋁ z ∈ y))))
217 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ (∀w(w ∈ z → w ∈ y) → (∃w∀v((v ∈ z → ∃t∀u((u ∈ y ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = v ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u)))))) ↔ u = t)) ⋀ (v ∈ y → ∃t∀u((u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (h = u ⋁ ∀f(f ∈ h ↔ (f = u ⋁ f = v)))))) ↔ u = t))) ⋁ z ∈ y))))
233 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ (∀w(w ∈ z → w ∈ y) → (∃w∀v((v ∈ z → ∃t∀u((u ∈ y ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u)))))) ↔ u = t)) ⋀ (v ∈ y → ∃t∀u((u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = u) ⋁ ∀f(f ∈ h ↔ (f = u ⋁ f = v)))))) ↔ u = t))) ⋁ z ∈ y))))
235 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ (∀w(w ∈ z → w ∈ y) → (∃w(∀v(v ∈ z → ∃t∀u((u ∈ y ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u)))))) ↔ u = t)) ⋀ ∀u(u ∈ y → ∃t∀v((v ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u)))))) ↔ v = t))) ⋁ z ∈ y))))
335 symbols.
⊢ ∃y(x ∈ y ⋀ ∀z((z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ (∀w(w ∈ z → w ∈ y) → (∃w∀v(((v ∈ z → ∃u(u ∈ y ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u))))))) ⋀ (v ∈ y → ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = u) ⋁ ∀f(f ∈ h ↔ (f = u ⋁ f = v)))))))) ⋀ ∀u∀t∀k((∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u))))) ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = t) ⋁ ∀f(f ∈ h ↔ (f = t ⋁ f = k)))))) → (v = t ↔ u = k))) ⋁ z ∈ y))))
337 symbols.
⊢ ∃y(x ∈ y ⋀ (∀z(z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ ∀z(∀w(w ∈ z → w ∈ y) → (∃w∀v(((v ∈ z → ∃u(u ∈ y ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u))))))) ⋀ (v ∈ y → ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = u) ⋁ ∀f(f ∈ h ↔ (f = u ⋁ f = v)))))))) ⋀ ∀u∀t∀k((∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u))))) ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = t) ⋁ ∀f(f ∈ h ↔ (f = t ⋁ f = k)))))) → (v = t ↔ u = k))) ⋁ z ∈ y))))
341 symbols.
⊢ ∃y(x ∈ y ⋀ (∀z(z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ ∀z(∀w(w ∈ z → w ∈ y) → (∃w((∀v(v ∈ z → ∃u(u ∈ y ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u))))))) ⋀ ∀v(v ∈ y → ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = u) ⋁ ∀f(f ∈ h ↔ (f = u ⋁ f = v)))))))) ⋀ ∀v∀u∀t∀k((∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u))))) ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = t) ⋁ ∀f(f ∈ h ↔ (f = t ⋁ f = k)))))) → (v = t ↔ u = k))) ⋁ z ∈ y))))
345 symbols.
⊢ ∃y(x ∈ y ⋀ (∀z(z ∈ y → (∀w(∀v(v ∈ w → v ∈ z) → w ∈ y) ⋀ ∃w(w ∈ y ⋀ ∀v(∀u(u ∈ v → u ∈ z) → v ∈ w)))) ⋀ ∀z(∀w(w ∈ z → w ∈ y) → (∃w((∀v(v ∈ z → ∃u(u ∈ y ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u))))))) ⋀ ∀v(v ∈ y → ∃u(u ∈ z ⋀ ∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = u) ⋁ ∀f(f ∈ h ↔ (f = u ⋁ f = v)))))))) ⋀ (∀v∃t∀u(∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = v) ⋁ ∀f(f ∈ h ↔ (f = v ⋁ f = u))))) → u = t) ⋀ ∀v∃t∀u(∃g(g ∈ w ⋀ ∀h(h ∈ g ↔ (∀f(f ∈ h ↔ f = u) ⋁ ∀f(f ∈ h ↔ (f = u ⋁ f = v))))) → u = t))) ⋁ z ∈ y))))