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

Theorem axrepndlem2 10093
Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (New usage is discouraged.)
Assertion
Ref Expression
axrepndlem2 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))

Proof of Theorem axrepndlem2
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 axrepndlem1 10092 . . 3 (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑤(∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))))
2 nfnae 2434 . . . . 5 𝑥 ¬ ∀𝑥 𝑥 = 𝑦
3 nfnae 2434 . . . . 5 𝑥 ¬ ∀𝑥 𝑥 = 𝑧
42, 3nfan 1906 . . . 4 𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
5 nfnae 2434 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑦
6 nfnae 2434 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑧
75, 6nfan 1906 . . . . . 6 𝑦(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
8 nfnae 2434 . . . . . . . 8 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
9 nfnae 2434 . . . . . . . 8 𝑧 ¬ ∀𝑥 𝑥 = 𝑧
108, 9nfan 1906 . . . . . . 7 𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
11 nfs1v 2161 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
1211a1i 11 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥[𝑤 / 𝑥]𝜑)
13 nfcvf 2928 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑧𝑥𝑧)
1413adantl 485 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑥𝑧)
15 nfcvf 2928 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
1615adantr 484 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑥𝑦)
1714, 16nfeqd 2909 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧 = 𝑦)
1812, 17nfimd 1901 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥([𝑤 / 𝑥]𝜑𝑧 = 𝑦))
1910, 18nfald 2330 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦))
207, 19nfexd 2331 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦))
21 nfcvd 2900 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑥𝑤)
2214, 21nfeld 2910 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧𝑤)
23 nfv 1921 . . . . . . . 8 𝑤(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
2421, 16nfeld 2910 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤𝑦)
257, 12nfald 2330 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦[𝑤 / 𝑥]𝜑)
2624, 25nfand 1904 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))
2723, 26nfexd 2331 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))
2822, 27nfbid 1909 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))
2910, 28nfald 2330 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))
3020, 29nfimd 1901 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))))
31 nfcvd 2900 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑦𝑤)
32 nfcvf2 2929 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
3332adantr 484 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑦𝑥)
3431, 33nfeqd 2909 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥)
357, 34nfan1 2202 . . . . . . 7 𝑦((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
36 nfcvd 2900 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑧𝑤)
37 nfcvf2 2929 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑥)
3837adantl 485 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑧𝑥)
3936, 38nfeqd 2909 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑥)
4010, 39nfan1 2202 . . . . . . . 8 𝑧((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
41 sbequ12r 2254 . . . . . . . . . 10 (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑𝜑))
4241imbi1d 345 . . . . . . . . 9 (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ (𝜑𝑧 = 𝑦)))
4342adantl 485 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ (𝜑𝑧 = 𝑦)))
4440, 43albid 2224 . . . . . . 7 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ ∀𝑧(𝜑𝑧 = 𝑦)))
4535, 44exbid 2225 . . . . . 6 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ ∃𝑦𝑧(𝜑𝑧 = 𝑦)))
46 elequ2 2129 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑧𝑤𝑧𝑥))
4746adantl 485 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑧𝑤𝑧𝑥))
48 elequ1 2121 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤𝑦𝑥𝑦))
4948adantl 485 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑤𝑦𝑥𝑦))
5041adantl 485 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ([𝑤 / 𝑥]𝜑𝜑))
5135, 50albid 2224 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦[𝑤 / 𝑥]𝜑 ↔ ∀𝑦𝜑))
5249, 51anbi12d 634 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥𝑦 ∧ ∀𝑦𝜑)))
5352ex 416 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥𝑦 ∧ ∀𝑦𝜑))))
544, 26, 53cbvexd 2408 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))
5554adantr 484 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))
5647, 55bibi12d 349 . . . . . . 7 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ (𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))
5740, 56albid 2224 . . . . . 6 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))
5845, 57imbi12d 348 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))))
5958ex 416 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))))
604, 30, 59cbvexd 2408 . . 3 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))))
611, 60syl5ib 247 . 2 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))))
6261imp 410 1 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1540  wex 1786  wnf 1790  [wsb 2074  wnfc 2879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-13 2372  ax-ext 2710  ax-rep 5154
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-cleq 2730  df-clel 2811  df-nfc 2881
This theorem is referenced by:  axrepnd  10094
  Copyright terms: Public domain W3C validator