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

Theorem zfcndinf 10661
Description: Axiom of Infinity ax-inf 9681, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5443 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 5443 . . 3 𝑤 𝑥𝑤
2 nfv 1910 . . . . . 6 𝑤 𝑥𝑦
3 nfe1 2140 . . . . . . . 8 𝑤𝑤(𝑥𝑤𝑤𝑦)
42, 3nfim 1892 . . . . . . 7 𝑤(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))
54nfal 2312 . . . . . 6 𝑤𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))
62, 5nfan 1895 . . . . 5 𝑤(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
76nfex 2313 . . . 4 𝑤𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
8 axinfnd 10649 . . . . 5 𝑦(𝑥𝑤 → (𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
9819.37iv 1945 . . . 4 (𝑥𝑤 → ∃𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
107, 9exlimi 2206 . . 3 (∃𝑤 𝑥𝑤 → ∃𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
111, 10ax-mp 5 . 2 𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
12 elequ1 2106 . . . . . 6 (𝑧 = 𝑥 → (𝑧𝑦𝑥𝑦))
13 elequ1 2106 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧𝑤𝑥𝑤))
1413anbi1d 629 . . . . . . 7 (𝑧 = 𝑥 → ((𝑧𝑤𝑤𝑦) ↔ (𝑥𝑤𝑤𝑦)))
1514exbidv 1917 . . . . . 6 (𝑧 = 𝑥 → (∃𝑤(𝑧𝑤𝑤𝑦) ↔ ∃𝑤(𝑥𝑤𝑤𝑦)))
1612, 15imbi12d 343 . . . . 5 (𝑧 = 𝑥 → ((𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ (𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
1716cbvalvw 2032 . . . 4 (∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦)))
1817anbi2i 621 . . 3 ((𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))) ↔ (𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
1918exbii 1843 . 2 (∃𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))) ↔ ∃𝑦(𝑥𝑦 ∧ ∀𝑥(𝑥𝑦 → ∃𝑤(𝑥𝑤𝑤𝑦))))
2011, 19mpbir 230 1 𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1532   = wceq 1534  wex 1774  wcel 2099
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-13 2366  ax-ext 2697  ax-sep 5304  ax-pr 5433  ax-reg 9635  ax-inf 9681
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-v 3464  df-un 3952  df-sn 4634  df-pr 4636
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator