Theorem wfaxnul

Description: The class of well-founded sets models the Null Set Axiom ax-nul . (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Hypothesis	wfax.1	⊢ 𝑊 = ∪ ( 𝑅1 “ On )
Assertion	wfaxnul	⊢ ∃ 𝑥 ∈ 𝑊 ∀ 𝑦 ∈ 𝑊 ¬ 𝑦 ∈ 𝑥

Proof

Step	Hyp	Ref	Expression
1		wfax.1	⊢ 𝑊 = ∪ ( 𝑅1 “ On )
2		onwf	⊢ On ⊆ ∪ ( 𝑅1 “ On )
3		0elon	⊢ ∅ ∈ On
4	2 3	sselii	⊢ ∅ ∈ ∪ ( 𝑅1 “ On )
5	4 1	eleqtrri	⊢ ∅ ∈ 𝑊
6		0elaxnul	⊢ ( ∅ ∈ 𝑊 → ∃ 𝑥 ∈ 𝑊 ∀ 𝑦 ∈ 𝑊 ¬ 𝑦 ∈ 𝑥 )
7	5 6	ax-mp	⊢ ∃ 𝑥 ∈ 𝑊 ∀ 𝑦 ∈ 𝑊 ¬ 𝑦 ∈ 𝑥