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=\left\{x|\left(x\in x\to \phi \right)\right\}$$
Assertion	currysetlem3	$$⊢\neg X\in V$$

Proof

Step	Hyp	Ref	Expression
1		currysetlem2.def	$$⊢X=\left\{x|\left(x\in x\to \phi \right)\right\}$$
2	1	currysetlem2	$$⊢X\in V\to \left(X\in X\to \phi \right)$$
3	1	currysetlem1	$$⊢X\in V\to \left(X\in X\leftrightarrow \left(X\in X\to \phi \right)\right)$$
4	2 3	mpbird	$$⊢X\in V\to X\in X$$
5	1	currysetlem2	$$⊢X\in X\to \left(X\in X\to \phi \right)$$
6	5	pm2.43i	$$⊢X\in X\to \phi$$
7		ax-1	$$⊢\phi \to \left(x\in x\to \phi \right)$$
8	7	alrimiv	$$⊢\phi \to \forall x\left(x\in x\to \phi \right)$$
9		bj-abv	$$⊢\forall x\left(x\in x\to \phi \right)\to \left\{x|\left(x\in x\to \phi \right)\right\}=\mathrm{V}$$
10	1 9	syl5eq	$$⊢\forall x\left(x\in x\to \phi \right)\to X=\mathrm{V}$$
11	8 10	syl	$$⊢\phi \to X=\mathrm{V}$$
12		nvel	$$⊢\neg \mathrm{V}\in V$$
13		eleq1	$$⊢X=\mathrm{V}\to \left(X\in V\leftrightarrow \mathrm{V}\in V\right)$$
14	12 13	mtbiri	$$⊢X=\mathrm{V}\to \neg X\in V$$
15	4 6 11 14	4syl	$$⊢X\in V\to \neg X\in V$$
16	15	bj-pm2.01i	$$⊢\neg X\in V$$