Theorem mirimanoff

Description: Mirimanoff's paradox: The class of grounded sets is not a set. Here, a set x is grounded if there is no infinite membership-descending sequence of sets beginning with x . See Paragraph 1 of Quine p. 37 . (Contributed by Adrian Ducourtial, 11-Oct-2026)

	Ref	Expression
Hypothesis	mirimanoff.1	⊢ 𝑀 = { 𝑥 ∣ ¬ ∃ 𝑓 ( 𝑓 Fn ω ∧ ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ∀ 𝑛 ∈ ω ( 𝑓 ‘ suc 𝑛 ) ∈ ( 𝑓 ‘ 𝑛 ) ) }
Assertion	mirimanoff	⊢ 𝑀 ∉ V

Proof

Step	Hyp	Ref	Expression
1		mirimanoff.1	⊢ 𝑀 = { 𝑥 ∣ ¬ ∃ 𝑓 ( 𝑓 Fn ω ∧ ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ∀ 𝑛 ∈ ω ( 𝑓 ‘ suc 𝑛 ) ∈ ( 𝑓 ‘ 𝑛 ) ) }
2		rabab	⊢ { 𝑥 ∈ V ∣ ¬ ∃ 𝑓 ( 𝑓 Fn ω ∧ ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ∀ 𝑛 ∈ ω ( 𝑓 ‘ suc 𝑛 ) ∈ ( 𝑓 ‘ 𝑛 ) ) } = { 𝑥 ∣ ¬ ∃ 𝑓 ( 𝑓 Fn ω ∧ ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ∀ 𝑛 ∈ ω ( 𝑓 ‘ suc 𝑛 ) ∈ ( 𝑓 ‘ 𝑛 ) ) }
3	1 2	eqtr4i	⊢ 𝑀 = { 𝑥 ∈ V ∣ ¬ ∃ 𝑓 ( 𝑓 Fn ω ∧ ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ∀ 𝑛 ∈ ω ( 𝑓 ‘ suc 𝑛 ) ∈ ( 𝑓 ‘ 𝑛 ) ) }
4	3	mirimanoffr	⊢ 𝑀 ∉ V