Theorem curryset

Description: Curry's paradox in set theory. This can be seen as a generalization of Russell's paradox, which corresponds to the case where ph is F. . See alternate exposal of basically the same proof currysetALT . (Contributed by BJ, 23-Sep-2023) This proof is intuitionistically valid. (Proof modification is discouraged.)

	Ref	Expression
Assertion	curryset	⊢ ¬ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ 𝑉

Proof

Step	Hyp	Ref	Expression
1		currysetlem	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } → ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ↔ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } → 𝜑 ) ) )
2	1	ibi	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } → ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } → 𝜑 ) )
3	2	pm2.43i	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } → 𝜑 )
4		currysetlem	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ 𝑉 → ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ↔ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } → 𝜑 ) ) )
5	3 4	mpbiri	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ 𝑉 → { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } )
6		ax-1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑥 → 𝜑 ) )
7	6	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝑥 → 𝜑 ) )
8		bj-abv	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑥 → 𝜑 ) → { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } = V )
9	7 8	syl	⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } = V )
10		nvel	⊢ ¬ V ∈ 𝑉
11		eleq1	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } = V → ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ 𝑉 ↔ V ∈ 𝑉 ) )
12	10 11	mtbiri	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } = V → ¬ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ 𝑉 )
13	5 3 9 12	4syl	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ 𝑉 → ¬ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ 𝑉 )
14	13	pm2.01i	⊢ ¬ { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) } ∈ 𝑉