Theorem permaxnul

Description: The Null Set Axiom ax-nul holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148. (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Hypotheses	permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
	permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
Assertion	permaxnul	$$⊢\exists x\forall y\neg yRx$$

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
2		permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
3		fvex	$$⊢F^{-1}\left(\varnothing \right)\in \mathrm{V}$$
4		breq2	$$⊢x=F^{-1}\left(\varnothing \right)\to \left(yRx\leftrightarrow yR{F}^{-1}\left(\varnothing \right)\right)$$
5	4	notbid	$$⊢x=F^{-1}\left(\varnothing \right)\to \left(\neg yRx\leftrightarrow \neg yR{F}^{-1}\left(\varnothing \right)\right)$$
6	5	albidv	$$⊢x=F^{-1}\left(\varnothing \right)\to \left(\forall y\neg yRx\leftrightarrow \forall y\neg yR{F}^{-1}\left(\varnothing \right)\right)$$
7		noel	$$⊢\neg y\in \varnothing$$
8		vex	$$⊢y\in \mathrm{V}$$
9		0ex	$$⊢\varnothing \in \mathrm{V}$$
10	1 2 8 9	brpermmodelcnv	$$⊢yR{F}^{-1}\left(\varnothing \right)\leftrightarrow y\in \varnothing$$
11	7 10	mtbir	$$⊢\neg yR{F}^{-1}\left(\varnothing \right)$$
12	11	ax-gen	$$⊢\forall y\neg yR{F}^{-1}\left(\varnothing \right)$$
13	3 6 12	ceqsexv2d	$$⊢\exists x\forall y\neg yRx$$