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	|- -. { x | ( x e. x -> ph ) } e. V

Proof

Step	Hyp	Ref	Expression
1		currysetlem	|- ( { x | ( x e. x -> ph ) } e. { x | ( x e. x -> ph ) } -> ( { x | ( x e. x -> ph ) } e. { x | ( x e. x -> ph ) } <-> ( { x | ( x e. x -> ph ) } e. { x | ( x e. x -> ph ) } -> ph ) ) )
2	1	ibi	|- ( { x | ( x e. x -> ph ) } e. { x | ( x e. x -> ph ) } -> ( { x | ( x e. x -> ph ) } e. { x | ( x e. x -> ph ) } -> ph ) )
3	2	pm2.43i	|- ( { x | ( x e. x -> ph ) } e. { x | ( x e. x -> ph ) } -> ph )
4		currysetlem	|- ( { x | ( x e. x -> ph ) } e. V -> ( { x | ( x e. x -> ph ) } e. { x | ( x e. x -> ph ) } <-> ( { x | ( x e. x -> ph ) } e. { x | ( x e. x -> ph ) } -> ph ) ) )
5	3 4	mpbiri	|- ( { x | ( x e. x -> ph ) } e. V -> { x | ( x e. x -> ph ) } e. { x | ( x e. x -> ph ) } )
6		ax-1	|- ( ph -> ( x e. x -> ph ) )
7	6	alrimiv	|- ( ph -> A. x ( x e. x -> ph ) )
8		bj-abv	|- ( A. x ( x e. x -> ph ) -> { x | ( x e. x -> ph ) } = _V )
9	7 8	syl	|- ( ph -> { x | ( x e. x -> ph ) } = _V )
10		nvel	|- -. _V e. V
11		eleq1	|- ( { x | ( x e. x -> ph ) } = _V -> ( { x | ( x e. x -> ph ) } e. V <-> _V e. V ) )
12	10 11	mtbiri	|- ( { x | ( x e. x -> ph ) } = _V -> -. { x | ( x e. x -> ph ) } e. V )
13	5 3 9 12	4syl	|- ( { x | ( x e. x -> ph ) } e. V -> -. { x | ( x e. x -> ph ) } e. V )
14	13	bj-pm2.01i	|- -. { x | ( x e. x -> ph ) } e. V