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

Theorem zfcndinf 10658
Description: Axiom of Infinity ax-inf 9678, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5442 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 5442 . . 3 𝑤 𝑥𝑤
2 nfv 1914 . . . . . 6 𝑤 𝑥𝑦
3 nfe1 2150 . . . . . . . 8 𝑤𝑤(𝑥𝑤𝑤𝑦)
42, 3nfim 1896 . . . . . . 7 𝑤(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))
54nfal 2323 . . . . . 6 𝑤𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))
62, 5nfan 1899 . . . . 5 𝑤(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
76nfex 2324 . . . 4 𝑤𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
8 axinfnd 10646 . . . . 5 𝑦(𝑥𝑤 → (𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
9819.37iv 1948 . . . 4 (𝑥𝑤 → ∃𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
107, 9exlimi 2217 . . 3 (∃𝑤 𝑥𝑤 → ∃𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
111, 10ax-mp 5 . 2 𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
12 elequ1 2115 . . . . . 6 (𝑧 = 𝑥 → (𝑧𝑦𝑥𝑦))
13 elequ1 2115 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧𝑤𝑥𝑤))
1413anbi1d 631 . . . . . . 7 (𝑧 = 𝑥 → ((𝑧𝑤𝑤𝑦) ↔ (𝑥𝑤𝑤𝑦)))
1514exbidv 1921 . . . . . 6 (𝑧 = 𝑥 → (∃𝑤(𝑧𝑤𝑤𝑦) ↔ ∃𝑤(𝑥𝑤𝑤𝑦)))
1612, 15imbi12d 344 . . . . 5 (𝑧 = 𝑥 → ((𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ (𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
1716cbvalvw 2035 . . . 4 (∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
1817anbi2i 623 . . 3 ((𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))) ↔ (𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
1918exbii 1848 . 2 (∃𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))) ↔ ∃𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
2011, 19mpbir 231 1 𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1538   = wceq 1540  wex 1779  wcel 2108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-13 2377  ax-ext 2708  ax-sep 5296  ax-pr 5432  ax-reg 9632  ax-inf 9678
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator