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

Theorem zfcndinf 10512
Description: Axiom of Infinity ax-inf 9532, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5392 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 5392 . . 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 10500 . . . . 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 2370  ax-ext 2707  ax-sep 5254  ax-pr 5382  ax-reg 9486  ax-inf 9532
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 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-v 3445  df-un 3913  df-sn 4585  df-pr 4587
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator