Theorem mirimanofff

Description: Mirimanoff's paradox mirimanoff for founded sets. A set x is founded if every set containing x has a minimal element under membership. Compare with zfreg the defining condition of M in the hypothesis. (Contributed by Adrian Ducourtial, 28-Oct-2026)

	Ref	Expression
Hypothesis	mirimanofff.1	⊢ 𝑀 = { 𝑥 ∣ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝑦 ) = ∅ ) }
Assertion	mirimanofff	⊢ 𝑀 ∉ V

Proof

Step	Hyp	Ref	Expression
1		mirimanofff.1	⊢ 𝑀 = { 𝑥 ∣ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝑦 ) = ∅ ) }
2		rabab	⊢ { 𝑥 ∈ V ∣ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝑦 ) = ∅ ) } = { 𝑥 ∣ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝑦 ) = ∅ ) }
3	1 2	eqtr4i	⊢ 𝑀 = { 𝑥 ∈ V ∣ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝑦 ) = ∅ ) }
4	3	mirimanofffr	⊢ 𝑀 ∉ V