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 | |- -. { x e. A | -. x e. x } e. A |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq12 | |- ( ( x = y /\ x = y ) -> ( x e. x <-> y e. y ) ) |
|
2 | 1 | anidms | |- ( x = y -> ( x e. x <-> y e. y ) ) |
3 | 2 | notbid | |- ( x = y -> ( -. x e. x <-> -. y e. y ) ) |
4 | 3 | cbvrabv | |- { x e. A | -. x e. x } = { y e. A | -. y e. y } |
5 | 4 | eleq2i | |- ( { x e. A | -. x e. x } e. { x e. A | -. x e. x } <-> { x e. A | -. x e. x } e. { y e. A | -. y e. y } ) |
6 | elex | |- ( { x e. A | -. x e. x } e. { y e. A | -. y e. y } -> { x e. A | -. x e. x } e. _V ) |
|
7 | elex | |- ( { x e. A | -. x e. x } e. A -> { x e. A | -. x e. x } e. _V ) |
|
8 | 7 | adantr | |- ( ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) -> { x e. A | -. x e. x } e. _V ) |
9 | eleq1 | |- ( y = z -> ( y e. A <-> z e. A ) ) |
|
10 | id | |- ( y = z -> y = z ) |
|
11 | 10 10 | eleq12d | |- ( y = z -> ( y e. y <-> z e. z ) ) |
12 | 11 | notbid | |- ( y = z -> ( -. y e. y <-> -. z e. z ) ) |
13 | 9 12 | anbi12d | |- ( y = z -> ( ( y e. A /\ -. y e. y ) <-> ( z e. A /\ -. z e. z ) ) ) |
14 | eleq1 | |- ( z = { x e. A | -. x e. x } -> ( z e. A <-> { x e. A | -. x e. x } e. A ) ) |
|
15 | eleq12 | |- ( ( z = { x e. A | -. x e. x } /\ z = { x e. A | -. x e. x } ) -> ( z e. z <-> { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
|
16 | 15 | anidms | |- ( z = { x e. A | -. x e. x } -> ( z e. z <-> { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
17 | 16 | notbid | |- ( z = { x e. A | -. x e. x } -> ( -. z e. z <-> -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
18 | 14 17 | anbi12d | |- ( z = { x e. A | -. x e. x } -> ( ( z e. A /\ -. z e. z ) <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) ) |
19 | df-rab | |- { y e. A | -. y e. y } = { y | ( y e. A /\ -. y e. y ) } |
|
20 | 13 18 19 | elab2gw | |- ( { x e. A | -. x e. x } e. _V -> ( { x e. A | -. x e. x } e. { y e. A | -. y e. y } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) ) |
21 | 6 8 20 | pm5.21nii | |- ( { x e. A | -. x e. x } e. { y e. A | -. y e. y } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
22 | 5 21 | bitri | |- ( { x e. A | -. x e. x } e. { x e. A | -. x e. x } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
23 | pclem6 | |- ( ( { x e. A | -. x e. x } e. { x e. A | -. x e. x } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) -> -. { x e. A | -. x e. x } e. A ) |
|
24 | 22 23 | ax-mp | |- -. { x e. A | -. x e. x } e. A |