This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elirrv

Description: The membership relation is irreflexive: no set is a member of itself. Theorem 105 of Suppes p. 54. This is trivial to prove from zfregfr and efrirr (see elirrvALT ), but this proof is direct from ax-reg . (Contributed by NM, 19-Aug-1993) Reduce axiom dependencies and make use of ax-reg directly. (Revised by BTernaryTau, 27-Dec-2025)

Ref Expression
Assertion elirrv ¬ 𝑥 ∈ 𝑥

Proof

Step Hyp Ref Expression
1 biimpr ⊢ ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 ) )
2 1 alimi ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ∀ 𝑦 ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 ) )
3 elequ1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤 ) )
4 3 equsalvw ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 ) ↔ 𝑥 ∈ 𝑤 )
5 2 4 sylib ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → 𝑥 ∈ 𝑤 )
6 3 equsexvw ⊢ ( ∃ 𝑦 ( 𝑦 = 𝑥 ∧ 𝑦 ∈ 𝑤 ) ↔ 𝑥 ∈ 𝑤 )
7 exsimpr ⊢ ( ∃ 𝑦 ( 𝑦 = 𝑥 ∧ 𝑦 ∈ 𝑤 ) → ∃ 𝑦 𝑦 ∈ 𝑤 )
8 6 7 sylbir ⊢ ( 𝑥 ∈ 𝑤 → ∃ 𝑦 𝑦 ∈ 𝑤 )
9 ax-reg ⊢ ( ∃ 𝑦 𝑦 ∈ 𝑤 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) )
10 8 9 syl ⊢ ( 𝑥 ∈ 𝑤 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) )
11 elequ1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
12 elequ1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤 ) )
13 12 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑧 ∈ 𝑤 ↔ ¬ 𝑥 ∈ 𝑤 ) )
14 11 13 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ↔ ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) ) )
15 14 spvv ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) → ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) )
16 con2 ⊢ ( ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) → ( 𝑥 ∈ 𝑤 → ¬ 𝑥 ∈ 𝑦 ) )
17 16 com12 ⊢ ( 𝑥 ∈ 𝑤 → ( ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) → ¬ 𝑥 ∈ 𝑦 ) )
18 17 anim2d ⊢ ( 𝑥 ∈ 𝑤 → ( ( 𝑦 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑤 ) ) → ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
19 15 18 sylan2i ⊢ ( 𝑥 ∈ 𝑤 → ( ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) → ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
20 19 eximdv ⊢ ( 𝑥 ∈ 𝑤 → ( ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤 ) ) → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
21 10 20 mpd ⊢ ( 𝑥 ∈ 𝑤 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) )
22 19.29 ⊢ ( ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) → ∃ 𝑦 ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
23 biimp ⊢ ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ( 𝑦 ∈ 𝑤 → 𝑦 = 𝑥 ) )
24 23 anim1d ⊢ ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ( ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) → ( 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝑦 ) ) )
25 ax9v2 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 → 𝑥 ∈ 𝑦 ) )
26 25 equcoms ⊢ ( 𝑦 = 𝑥 → ( 𝑥 ∈ 𝑥 → 𝑥 ∈ 𝑦 ) )
27 26 con3dimp ⊢ ( ( 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝑦 ) → ¬ 𝑥 ∈ 𝑥 )
28 24 27 syl6 ⊢ ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ( ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) → ¬ 𝑥 ∈ 𝑥 ) )
29 28 imp ⊢ ( ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) → ¬ 𝑥 ∈ 𝑥 )
30 29 exlimiv ⊢ ( ∃ 𝑦 ( ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) → ¬ 𝑥 ∈ 𝑥 )
31 22 30 syl ⊢ ( ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑦 ) ) → ¬ 𝑥 ∈ 𝑥 )
32 21 31 sylan2 ⊢ ( ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) ∧ 𝑥 ∈ 𝑤 ) → ¬ 𝑥 ∈ 𝑥 )
33 5 32 mpdan ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 ) → ¬ 𝑥 ∈ 𝑥 )
34 el ⊢ ∃ 𝑤 𝑥 ∈ 𝑤
35 4 biimpri ⊢ ( 𝑥 ∈ 𝑤 → ∀ 𝑦 ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 ) )
36 34 35 eximii ⊢ ∃ 𝑤 ∀ 𝑦 ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑤 )
37 36 sepexi ⊢ ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝑦 = 𝑥 )
38 33 37 exlimiiv ⊢ ¬ 𝑥 ∈ 𝑥