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	⊢ 𝑋 = { 𝑥 ∣ ( 𝑥 ∈ 𝑥 → 𝜑 ) }
Assertion	currysetlem3	⊢ ¬ 𝑋 ∈ 𝑉

Proof

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