Metamath Proof Explorer

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 ∈ x → φ ∈ V

Proof

Step Hyp Ref Expression
1 currysetlem ⊢ x | x ∈ x → φ ∈ x | x ∈ x → φ → x | x ∈ x → φ ∈ x | x ∈ x → φ ↔ x | x ∈ x → φ ∈ x | x ∈ x → φ → φ
2 1 ibi ⊢ x | x ∈ x → φ ∈ x | x ∈ x → φ → x | x ∈ x → φ ∈ x | x ∈ x → φ → φ
3 2 pm2.43i ⊢ x | x ∈ x → φ ∈ x | x ∈ x → φ → φ
4 currysetlem ⊢ x | x ∈ x → φ ∈ V → x | x ∈ x → φ ∈ x | x ∈ x → φ ↔ x | x ∈ x → φ ∈ x | x ∈ x → φ → φ
5 3 4 mpbiri ⊢ x | x ∈ x → φ ∈ V → x | x ∈ x → φ ∈ x | x ∈ x → φ
6 ax-1 ⊢ φ → x ∈ x → φ
7 6 alrimiv ⊢ φ → ∀ x x ∈ x → φ
8 bj-abv ⊢ ∀ x x ∈ x → φ → x | x ∈ x → φ = V
9 7 8 syl ⊢ φ → x | x ∈ x → φ = V
10 nvel ⊢ ¬ V ∈ V
11 eleq1 ⊢ x | x ∈ x → φ = V → x | x ∈ x → φ ∈ V ↔ V ∈ V
12 10 11 mtbiri ⊢ x | x ∈ x → φ = V → ¬ x | x ∈ x → φ ∈ V
13 5 3 9 12 4syl ⊢ x | x ∈ x → φ ∈ V → ¬ x | x ∈ x → φ ∈ V
14 13 bj-pm2.01i ⊢ ¬ x | x ∈ x → φ ∈ V