Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axrepndlem2 Structured version   Visualization version   GIF version

Theorem axrepndlem2 9294
 Description: Lemma for the Axiom of Replacement with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
Assertion
Ref Expression
axrepndlem2 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))

Proof of Theorem axrepndlem2
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 axrepndlem1 9293 . . 3 (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑤(∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))))
2 nfnae 2306 . . . . 5 𝑥 ¬ ∀𝑥 𝑥 = 𝑦
3 nfnae 2306 . . . . 5 𝑥 ¬ ∀𝑥 𝑥 = 𝑧
42, 3nfan 1816 . . . 4 𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
5 nfnae 2306 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑦
6 nfnae 2306 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑧
75, 6nfan 1816 . . . . . 6 𝑦(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
8 nfnae 2306 . . . . . . . 8 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
9 nfnae 2306 . . . . . . . 8 𝑧 ¬ ∀𝑥 𝑥 = 𝑧
108, 9nfan 1816 . . . . . . 7 𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
11 nfs1v 2425 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
1211a1i 11 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥[𝑤 / 𝑥]𝜑)
13 nfcvf 2774 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑧𝑥𝑧)
1413adantl 481 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑥𝑧)
15 nfcvf 2774 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
1615adantr 480 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑥𝑦)
1714, 16nfeqd 2758 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧 = 𝑦)
1812, 17nfimd 1812 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥([𝑤 / 𝑥]𝜑𝑧 = 𝑦))
1910, 18nfald 2151 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦))
207, 19nfexd 2153 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦))
21 nfcvd 2752 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑥𝑤)
2214, 21nfeld 2759 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧𝑤)
23 nfv 1830 . . . . . . . 8 𝑤(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
2421, 16nfeld 2759 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤𝑦)
257, 12nfald 2151 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦[𝑤 / 𝑥]𝜑)
2624, 25nfand 1814 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))
2723, 26nfexd 2153 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))
2822, 27nfbid 1820 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))
2910, 28nfald 2151 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))
3020, 29nfimd 1812 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))))
31 nfcvd 2752 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑦𝑤)
32 nfcvf2 2775 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
3332adantr 480 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑦𝑥)
3431, 33nfeqd 2758 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥)
357, 34nfan1 2056 . . . . . . 7 𝑦((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
36 nfcvd 2752 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑧𝑤)
37 nfcvf2 2775 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑥)
3837adantl 481 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑧𝑥)
3936, 38nfeqd 2758 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑥)
4010, 39nfan1 2056 . . . . . . . 8 𝑧((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
41 sbequ12r 2098 . . . . . . . . . 10 (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑𝜑))
4241imbi1d 330 . . . . . . . . 9 (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ (𝜑𝑧 = 𝑦)))
4342adantl 481 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ (𝜑𝑧 = 𝑦)))
4440, 43albid 2077 . . . . . . 7 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ ∀𝑧(𝜑𝑧 = 𝑦)))
4535, 44exbid 2078 . . . . . 6 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ ∃𝑦𝑧(𝜑𝑧 = 𝑦)))
46 elequ2 1991 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑧𝑤𝑧𝑥))
4746adantl 481 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑧𝑤𝑧𝑥))
48 elequ1 1984 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤𝑦𝑥𝑦))
4948adantl 481 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑤𝑦𝑥𝑦))
5041adantl 481 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ([𝑤 / 𝑥]𝜑𝜑))
5135, 50albid 2077 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦[𝑤 / 𝑥]𝜑 ↔ ∀𝑦𝜑))
5249, 51anbi12d 743 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥𝑦 ∧ ∀𝑦𝜑)))
5352ex 449 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥𝑦 ∧ ∀𝑦𝜑))))
544, 26, 53cbvexd 2266 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))
5554adantr 480 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))
5647, 55bibi12d 334 . . . . . . 7 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ (𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))
5740, 56albid 2077 . . . . . 6 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))
5845, 57imbi12d 333 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))))
5958ex 449 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))))
604, 30, 59cbvexd 2266 . . 3 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))))
611, 60syl5ib 233 . 2 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))))
6261imp 444 1 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695  Ⅎwnf 1699  [wsb 1867  Ⅎwnfc 2738 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-cleq 2603  df-clel 2606  df-nfc 2740 This theorem is referenced by:  axrepnd  9295
 Copyright terms: Public domain W3C validator