Metamath Proof Explorer

Theorem axregndlem2

Description: Lemma for 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 Mario Carneiro, 10-Dec-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axreg2 ⊢ ( 𝑤 ∈ 𝑦 → ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) )
2 1 ax-gen ⊢ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) )
3 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
4 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑧
5 3 4 nfan ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
6 nfcvd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑤 )
7 nfcvf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
8 7 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑦 )
9 6 8 nfeld ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑤 ∈ 𝑦 )
10 nfv ⊢ Ⅎ 𝑤 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
11 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦
12 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑧
13 11 12 nfan ⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
14 nfcvf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑧 )
15 14 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑧 )
16 15 6 nfeld ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑧 ∈ 𝑤 )
17 15 8 nfeld ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑧 ∈ 𝑦 )
18 17 nfnd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ¬ 𝑧 ∈ 𝑦 )
19 16 18 nfimd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) )
20 13 19 nfald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) )
21 9 20 nfand ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) )
22 10 21 nfexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) )
23 9 22 nfimd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( 𝑤 ∈ 𝑦 → ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
24 simpr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → 𝑤 = 𝑥 )
25 24 eleq1d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( 𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
26 nfcvd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑧 𝑤 )
27 nfcvf2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑧 𝑥 )
28 27 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑧 𝑥 )
29 26 28 nfeqd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑧 𝑤 = 𝑥 )
30 13 29 nfan1 ⊢ Ⅎ 𝑧 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 )
31 24 eleq2d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥 ) )
32 31 imbi1d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )
33 30 32 albid ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )
34 25 33 anbi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
35 34 ex ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑤 = 𝑥 → ( ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) ) )
36 5 21 35 cbvexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
37 36 adantr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
38 25 37 imbi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( 𝑤 ∈ 𝑦 → ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) ) )
39 38 ex ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑤 = 𝑥 → ( ( 𝑤 ∈ 𝑦 → ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) ) ) )
40 5 23 39 cbvald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ¬ 𝑧 ∈ 𝑦 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) ) )
41 2 40 mpbii ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
42 41 19.21bi ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
43 42 ex ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) ) )
44 elirrv ⊢ ¬ 𝑥 ∈ 𝑥
45 elequ2 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑥 ∈ 𝑦 ) )
46 44 45 mtbii ⊢ ( 𝑥 = 𝑦 → ¬ 𝑥 ∈ 𝑦 )
47 46 sps ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ¬ 𝑥 ∈ 𝑦 )
48 47 pm2.21d ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
49 axregndlem1 ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
50 43 48 49 pm2.61ii ⊢ ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )