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	⊢ 𝐹 : V –1-1-onto→ V
	permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
Assertion	permaxnul	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 𝑅 𝑥

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	⊢ 𝐹 : V –1-1-onto→ V
2		permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3		fvex	⊢ ( ◡ 𝐹 ‘ ∅ ) ∈ V
4		breq2	⊢ ( 𝑥 = ( ◡ 𝐹 ‘ ∅ ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 ( ◡ 𝐹 ‘ ∅ ) ) )
5	4	notbid	⊢ ( 𝑥 = ( ◡ 𝐹 ‘ ∅ ) → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 ( ◡ 𝐹 ‘ ∅ ) ) )
6	5	albidv	⊢ ( 𝑥 = ( ◡ 𝐹 ‘ ∅ ) → ( ∀ 𝑦 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ¬ 𝑦 𝑅 ( ◡ 𝐹 ‘ ∅ ) ) )
7		noel	⊢ ¬ 𝑦 ∈ ∅
8		vex	⊢ 𝑦 ∈ V
9		0ex	⊢ ∅ ∈ V
10	1 2 8 9	brpermmodelcnv	⊢ ( 𝑦 𝑅 ( ◡ 𝐹 ‘ ∅ ) ↔ 𝑦 ∈ ∅ )
11	7 10	mtbir	⊢ ¬ 𝑦 𝑅 ( ◡ 𝐹 ‘ ∅ )
12	11	ax-gen	⊢ ∀ 𝑦 ¬ 𝑦 𝑅 ( ◡ 𝐹 ‘ ∅ )
13	3 6 12	ceqsexv2d	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 𝑅 𝑥