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

Theorem zfcndinf 10615
Description: Axiom of Infinity ax-inf 9635, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5437 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.)
Assertion
Ref Expression
zfcndinf 𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)))
Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Proof of Theorem zfcndinf
StepHypRef Expression
1 el 5437 . . 3 𝑤 𝑥𝑤
2 nfv 1917 . . . . . 6 𝑤 𝑥𝑦
3 nfe1 2147 . . . . . . . 8 𝑤𝑤(𝑥𝑤𝑤𝑦)
42, 3nfim 1899 . . . . . . 7 𝑤(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))
54nfal 2316 . . . . . 6 𝑤𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))
62, 5nfan 1902 . . . . 5 𝑤(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
76nfex 2317 . . . 4 𝑤𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
8 axinfnd 10603 . . . . 5 𝑦(𝑥𝑤 → (𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
9819.37iv 1952 . . . 4 (𝑥𝑤 → ∃𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
107, 9exlimi 2210 . . 3 (∃𝑤 𝑥𝑤 → ∃𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
111, 10ax-mp 5 . 2 𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
12 elequ1 2113 . . . . . 6 (𝑧 = 𝑥 → (𝑧𝑦𝑥𝑦))
13 elequ1 2113 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧𝑤𝑥𝑤))
1413anbi1d 630 . . . . . . 7 (𝑧 = 𝑥 → ((𝑧𝑤𝑤𝑦) ↔ (𝑥𝑤𝑤𝑦)))
1514exbidv 1924 . . . . . 6 (𝑧 = 𝑥 → (∃𝑤(𝑧𝑤𝑤𝑦) ↔ ∃𝑤(𝑥𝑤𝑤𝑦)))
1612, 15imbi12d 344 . . . . 5 (𝑧 = 𝑥 → ((𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ (𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
1716cbvalvw 2039 . . . 4 (∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
1817anbi2i 623 . . 3 ((𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))) ↔ (𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
1918exbii 1850 . 2 (∃𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))) ↔ ∃𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
2011, 19mpbir 230 1 𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1539   = wceq 1541  wex 1781  wcel 2106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2371  ax-ext 2703  ax-sep 5299  ax-pr 5427  ax-reg 9589  ax-inf 9635
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-v 3476  df-un 3953  df-sn 4629  df-pr 4631
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator