# Von Neumann ordinals #

This file works towards the development of von Neumann ordinals, i.e. transitive sets, well-ordered
under `∈`

. We currently only have an initial development of transitive sets.

Further development can be found on the branch `von_neumann_v2`

.

## Definitions #

`ZFSet.IsTransitive`

means that every element of a set is a subset.

## Todo #

- Define von Neumann ordinals.
- Define the basic arithmetic operations on ordinals from a purely set-theoretic perspective.
- Prove the equivalences between these definitions and those provided in
`SetTheory/Ordinal/Arithmetic.lean`

.

**Alias** of the forward direction of `ZFSet.isTransitive_iff_mem_trans`

.

theorem
ZFSet.IsTransitive.inter
{x : ZFSet}
{y : ZFSet}
(hx : x.IsTransitive)
(hy : y.IsTransitive)
:

(x ∩ y).IsTransitive

theorem
ZFSet.IsTransitive.union
{x : ZFSet}
{y : ZFSet}
(hx : x.IsTransitive)
(hy : y.IsTransitive)
:

(x ∪ y).IsTransitive

**Alias** of the forward direction of `ZFSet.isTransitive_iff_sUnion_subset`

.

**Alias** of the forward direction of `ZFSet.isTransitive_iff_subset_powerset`

.