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

Theorem axrepndlem2 10004
 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 10003 . . 3 (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑤(∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))))
2 nfnae 2453 . . . . 5 𝑥 ¬ ∀𝑥 𝑥 = 𝑦
3 nfnae 2453 . . . . 5 𝑥 ¬ ∀𝑥 𝑥 = 𝑧
42, 3nfan 1893 . . . 4 𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
5 nfnae 2453 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑦
6 nfnae 2453 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑧
75, 6nfan 1893 . . . . . 6 𝑦(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
8 nfnae 2453 . . . . . . . 8 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
9 nfnae 2453 . . . . . . . 8 𝑧 ¬ ∀𝑥 𝑥 = 𝑧
108, 9nfan 1893 . . . . . . 7 𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
11 nfs1v 2267 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
1211a1i 11 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥[𝑤 / 𝑥]𝜑)
13 nfcvf 3012 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑧𝑥𝑧)
1413adantl 482 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑥𝑧)
15 nfcvf 3012 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
1615adantr 481 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑥𝑦)
1714, 16nfeqd 2993 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧 = 𝑦)
1812, 17nfimd 1888 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥([𝑤 / 𝑥]𝜑𝑧 = 𝑦))
1910, 18nfald 2341 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦))
207, 19nfexd 2342 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦))
21 nfcvd 2983 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑥𝑤)
2214, 21nfeld 2994 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧𝑤)
23 nfv 1908 . . . . . . . 8 𝑤(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
2421, 16nfeld 2994 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤𝑦)
257, 12nfald 2341 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦[𝑤 / 𝑥]𝜑)
2624, 25nfand 1891 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))
2723, 26nfexd 2342 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))
2822, 27nfbid 1896 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))
2910, 28nfald 2341 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))
3020, 29nfimd 1888 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))))
31 nfcvd 2983 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑦𝑤)
32 nfcvf2 3013 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
3332adantr 481 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑦𝑥)
3431, 33nfeqd 2993 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥)
357, 34nfan1 2193 . . . . . . 7 𝑦((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
36 nfcvd 2983 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑧𝑤)
37 nfcvf2 3013 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑥)
3837adantl 482 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → 𝑧𝑥)
3936, 38nfeqd 2993 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑥)
4010, 39nfan1 2193 . . . . . . . 8 𝑧((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
41 sbequ12r 2247 . . . . . . . . . 10 (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑𝜑))
4241imbi1d 343 . . . . . . . . 9 (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ (𝜑𝑧 = 𝑦)))
4342adantl 482 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ (𝜑𝑧 = 𝑦)))
4440, 43albid 2217 . . . . . . 7 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ ∀𝑧(𝜑𝑧 = 𝑦)))
4535, 44exbid 2218 . . . . . 6 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) ↔ ∃𝑦𝑧(𝜑𝑧 = 𝑦)))
46 elequ2 2122 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑧𝑤𝑧𝑥))
4746adantl 482 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑧𝑤𝑧𝑥))
48 elequ1 2114 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤𝑦𝑥𝑦))
4948adantl 482 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑤𝑦𝑥𝑦))
5041adantl 482 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ([𝑤 / 𝑥]𝜑𝜑))
5135, 50albid 2217 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦[𝑤 / 𝑥]𝜑 ↔ ∀𝑦𝜑))
5249, 51anbi12d 630 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥𝑦 ∧ ∀𝑦𝜑)))
5352ex 413 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥𝑦 ∧ ∀𝑦𝜑))))
544, 26, 53cbvexd 2425 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))
5554adantr 481 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))
5647, 55bibi12d 347 . . . . . . 7 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ (𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))
5740, 56albid 2217 . . . . . 6 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))
5845, 57imbi12d 346 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))))
5958ex 413 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))))
604, 30, 59cbvexd 2425 . . 3 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(∃𝑦𝑧([𝑤 / 𝑥]𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑤 ↔ ∃𝑤(𝑤𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))))
611, 60syl5ib 245 . 2 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑)))))
6261imp 407 1 (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦𝑧(𝜑𝑧 = 𝑦) → ∀𝑧(𝑧𝑥 ↔ ∃𝑥(𝑥𝑦 ∧ ∀𝑦𝜑))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1528  ∃wex 1773  Ⅎwnf 1777  [wsb 2062  Ⅎwnfc 2966 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798  ax-rep 5187 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-cleq 2819  df-clel 2898  df-nfc 2968 This theorem is referenced by:  axrepnd  10005
 Copyright terms: Public domain W3C validator