Description: Relative version of Russell's paradox ru (which corresponds to the case A = _V ).
Originally a subproof in pwnss . (Contributed by Stefan O'Rear, 22-Feb-2015) Avoid df-nel . (Revised by Steven Nguyen, 23-Nov-2022) Reduce axiom usage. (Revised by Gino Giotto, 30-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | rru | ⊢ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq12 | ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) ) | |
2 | 1 | anidms | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) ) |
3 | 2 | notbid | ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝑦 ∈ 𝑦 ) ) |
4 | 3 | cbvrabv | ⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } = { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝑦 } |
5 | 4 | eleq2i | ⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ↔ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝑦 } ) |
6 | elex | ⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝑦 } → { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ V ) | |
7 | elex | ⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ V ) | |
8 | 7 | adantr | ⊢ ( ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) → { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ V ) |
9 | eleq1 | ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) | |
10 | id | ⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 ) | |
11 | 10 10 | eleq12d | ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝑦 ↔ 𝑧 ∈ 𝑧 ) ) |
12 | 11 | notbid | ⊢ ( 𝑦 = 𝑧 → ( ¬ 𝑦 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑧 ) ) |
13 | 9 12 | anbi12d | ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑧 ) ) ) |
14 | eleq1 | ⊢ ( 𝑧 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } → ( 𝑧 ∈ 𝐴 ↔ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ) ) | |
15 | eleq12 | ⊢ ( ( 𝑧 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∧ 𝑧 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) → ( 𝑧 ∈ 𝑧 ↔ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) | |
16 | 15 | anidms | ⊢ ( 𝑧 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } → ( 𝑧 ∈ 𝑧 ↔ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) |
17 | 16 | notbid | ⊢ ( 𝑧 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } → ( ¬ 𝑧 ∈ 𝑧 ↔ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) |
18 | 14 17 | anbi12d | ⊢ ( 𝑧 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } → ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑧 ) ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) ) |
19 | df-rab | ⊢ { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝑦 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝑦 ) } | |
20 | 13 18 19 | elab2gw | ⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ V → ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝑦 } ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) ) |
21 | 6 8 20 | pm5.21nii | ⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝑦 } ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) |
22 | 5 21 | bitri | ⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) |
23 | pclem6 | ⊢ ( ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) → ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ) | |
24 | 22 23 | ax-mp | ⊢ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 |