Metamath Proof Explorer

Theorem axregnd

Description: A version of the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (Proof shortened by Wolf Lammen, 18-Aug-2019) (New usage is discouraged.)

Ref Expression
Assertion axregnd ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 axregndlem2 ⊢ ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ¬ 𝑤 ∈ 𝑦 ) ) )
2 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑧 𝑧 = 𝑥
3 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑧 𝑧 = 𝑦
4 2 3 nfan ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 )
5 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑧 𝑧 = 𝑥
6 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑧 𝑧 = 𝑦
7 5 6 nfan ⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 )
8 nfcvf ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑥 )
9 8 nfcrd ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑤 ∈ 𝑥 )
10 9 adantr ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 𝑤 ∈ 𝑥 )
11 nfcvf ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 𝑦 )
12 11 nfcrd ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 𝑤 ∈ 𝑦 )
13 12 nfnd ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 ¬ 𝑤 ∈ 𝑦 )
14 13 adantl ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 ¬ 𝑤 ∈ 𝑦 )
15 10 14 nfimd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 ( 𝑤 ∈ 𝑥 → ¬ 𝑤 ∈ 𝑦 ) )
16 elequ1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
17 elequ1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
18 17 notbid ⊢ ( 𝑤 = 𝑧 → ( ¬ 𝑤 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦 ) )
19 16 18 imbi12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ 𝑥 → ¬ 𝑤 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )
20 19 a1i ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ 𝑥 → ¬ 𝑤 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
21 7 15 20 cbvald ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ¬ 𝑤 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )
22 21 anbi2d ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ¬ 𝑤 ∈ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
23 4 22 exbid ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ¬ 𝑤 ∈ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
24 1 23 imbitrid ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
25 24 ex ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) ) )
26 axregndlem1 ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
27 26 aecoms ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
28 19.8a ⊢ ( 𝑥 ∈ 𝑦 → ∃ 𝑥 𝑥 ∈ 𝑦 )
29 nfae ⊢ Ⅎ 𝑥 ∀ 𝑧 𝑧 = 𝑦
30 elirrv ⊢ ¬ 𝑧 ∈ 𝑧
31 elequ2 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑧 ↔ 𝑧 ∈ 𝑦 ) )
32 30 31 mtbii ⊢ ( 𝑧 = 𝑦 → ¬ 𝑧 ∈ 𝑦 )
33 32 a1d ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) )
34 33 alimi ⊢ ( ∀ 𝑧 𝑧 = 𝑦 → ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) )
35 34 anim2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 𝑧 = 𝑦 ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )
36 35 expcom ⊢ ( ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑦 → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
37 29 36 eximd ⊢ ( ∀ 𝑧 𝑧 = 𝑦 → ( ∃ 𝑥 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
38 28 37 syl5 ⊢ ( ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
39 25 27 38 pm2.61ii ⊢ ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )