Axiom ax-nin 4079

Description: State the axiom of anti-intersection. Axiom P1 of [Hailperin] p. 6. This axiom sets up boolean operations on sets.

Note on this and the following axioms: this axiom, ax-xp 4080, ax-cnv 4081, ax-1c 4082, ax-sset 4083, ax-si 4084, ax-ins2 4085, ax-ins3 4086, and ax-typlower 4087 are from Hailperin and are designed to implement the Stratification Axiom of Quine.

A well-formed formula using only propositional symbols, predicate symbols, and ∈ is "stratified" iff you can make a (metalogical) mapping from the variables to the natural numbers such that any formulas of the form x = y have the same number, and any formulas of the form x ∈ y have x as one less than y. Quine's stratification axiom states that there is a set corresponding to any stratified formula.

Since we cannot state stratification from within the logic, we use Hailperin's axioms and prove existence of stratified sets using Hailperin's algorithm. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
ax-nin	⊢ ∃z∀w(w ∈ z ↔ (w ∈ x ⊼ w ∈ y))

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-nin

Step	Hyp	Ref	Expression
1		vw	. . . . 5 setvar w
2		vz	. . . . 5 setvar z
3	1, 2	wel 1711	. . . 4 wff w ∈ z
4		vx	. . . . . 6 setvar x
5	1, 4	wel 1711	. . . . 5 wff w ∈ x
6		vy	. . . . . 6 setvar y
7	1, 6	wel 1711	. . . . 5 wff w ∈ y
8	5, 7	wnan 1287	. . . 4 wff (w ∈ x ⊼ w ∈ y)
9	3, 8	wb 176	. . 3 wff (w ∈ z ↔ (w ∈ x ⊼ w ∈ y))
10	9, 1	wal 1540	. 2 wff ∀w(w ∈ z ↔ (w ∈ x ⊼ w ∈ y))
11	10, 2	wex 1541	1 wff ∃z∀w(w ∈ z ↔ (w ∈ x ⊼ w ∈ y))

This axiom is referenced by:  ninexg  4098