Theorem currysetlem3

Description: Lemma for currysetALT . (Contributed by BJ, 23-Sep-2023) This proof is intuitionistically valid. (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	currysetlem2.def	|- X = { x | ( x e. x -> ph ) }
Assertion	currysetlem3	|- -. X e. V

Proof

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