Metamath Proof Explorer

Theorem rru

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 ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴

Proof

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 ⊢ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴