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

Theorem dcomex 9667
Description: The Axiom of Dependent Choice implies Infinity, the way we have stated it. Thus, we have Inf+AC implies DC and DC implies Inf, but AC does not imply Inf. (Contributed by Mario Carneiro, 25-Jan-2013.)
Assertion
Ref Expression
dcomex ω ∈ V

Proof of Theorem dcomex
Dummy variables 𝑡 𝑠 𝑥 𝑓 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1n0 7921 . . . . . . 7 1o ≠ ∅
2 df-br 4930 . . . . . . . 8 ((𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛) ↔ ⟨(𝑓𝑛), (𝑓‘suc 𝑛)⟩ ∈ {⟨1o, 1o⟩})
3 elsni 4458 . . . . . . . . 9 (⟨(𝑓𝑛), (𝑓‘suc 𝑛)⟩ ∈ {⟨1o, 1o⟩} → ⟨(𝑓𝑛), (𝑓‘suc 𝑛)⟩ = ⟨1o, 1o⟩)
4 fvex 6512 . . . . . . . . . 10 (𝑓𝑛) ∈ V
5 fvex 6512 . . . . . . . . . 10 (𝑓‘suc 𝑛) ∈ V
64, 5opth1 5224 . . . . . . . . 9 (⟨(𝑓𝑛), (𝑓‘suc 𝑛)⟩ = ⟨1o, 1o⟩ → (𝑓𝑛) = 1o)
73, 6syl 17 . . . . . . . 8 (⟨(𝑓𝑛), (𝑓‘suc 𝑛)⟩ ∈ {⟨1o, 1o⟩} → (𝑓𝑛) = 1o)
82, 7sylbi 209 . . . . . . 7 ((𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛) → (𝑓𝑛) = 1o)
9 tz6.12i 6525 . . . . . . 7 (1o ≠ ∅ → ((𝑓𝑛) = 1o𝑛𝑓1o))
101, 8, 9mpsyl 68 . . . . . 6 ((𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛) → 𝑛𝑓1o)
11 vex 3418 . . . . . . 7 𝑛 ∈ V
12 1oex 7913 . . . . . . 7 1o ∈ V
1311, 12breldm 5627 . . . . . 6 (𝑛𝑓1o𝑛 ∈ dom 𝑓)
1410, 13syl 17 . . . . 5 ((𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛) → 𝑛 ∈ dom 𝑓)
1514ralimi 3110 . . . 4 (∀𝑛 ∈ ω (𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛) → ∀𝑛 ∈ ω 𝑛 ∈ dom 𝑓)
16 dfss3 3847 . . . 4 (ω ⊆ dom 𝑓 ↔ ∀𝑛 ∈ ω 𝑛 ∈ dom 𝑓)
1715, 16sylibr 226 . . 3 (∀𝑛 ∈ ω (𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛) → ω ⊆ dom 𝑓)
18 vex 3418 . . . . 5 𝑓 ∈ V
1918dmex 7431 . . . 4 dom 𝑓 ∈ V
2019ssex 5081 . . 3 (ω ⊆ dom 𝑓 → ω ∈ V)
2117, 20syl 17 . 2 (∀𝑛 ∈ ω (𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛) → ω ∈ V)
22 snex 5188 . . 3 {⟨1o, 1o⟩} ∈ V
2312, 12fvsn 6766 . . . . . . . 8 ({⟨1o, 1o⟩}‘1o) = 1o
2412, 12funsn 6240 . . . . . . . . 9 Fun {⟨1o, 1o⟩}
2512snid 4473 . . . . . . . . . 10 1o ∈ {1o}
2612dmsnop 5912 . . . . . . . . . 10 dom {⟨1o, 1o⟩} = {1o}
2725, 26eleqtrri 2865 . . . . . . . . 9 1o ∈ dom {⟨1o, 1o⟩}
28 funbrfvb 6550 . . . . . . . . 9 ((Fun {⟨1o, 1o⟩} ∧ 1o ∈ dom {⟨1o, 1o⟩}) → (({⟨1o, 1o⟩}‘1o) = 1o ↔ 1o{⟨1o, 1o⟩}1o))
2924, 27, 28mp2an 679 . . . . . . . 8 (({⟨1o, 1o⟩}‘1o) = 1o ↔ 1o{⟨1o, 1o⟩}1o)
3023, 29mpbi 222 . . . . . . 7 1o{⟨1o, 1o⟩}1o
31 breq12 4934 . . . . . . . 8 ((𝑠 = 1o𝑡 = 1o) → (𝑠{⟨1o, 1o⟩}𝑡 ↔ 1o{⟨1o, 1o⟩}1o))
3212, 12, 31spc2ev 3526 . . . . . . 7 (1o{⟨1o, 1o⟩}1o → ∃𝑠𝑡 𝑠{⟨1o, 1o⟩}𝑡)
3330, 32ax-mp 5 . . . . . 6 𝑠𝑡 𝑠{⟨1o, 1o⟩}𝑡
34 breq 4931 . . . . . . 7 (𝑥 = {⟨1o, 1o⟩} → (𝑠𝑥𝑡𝑠{⟨1o, 1o⟩}𝑡))
35342exbidv 1883 . . . . . 6 (𝑥 = {⟨1o, 1o⟩} → (∃𝑠𝑡 𝑠𝑥𝑡 ↔ ∃𝑠𝑡 𝑠{⟨1o, 1o⟩}𝑡))
3633, 35mpbiri 250 . . . . 5 (𝑥 = {⟨1o, 1o⟩} → ∃𝑠𝑡 𝑠𝑥𝑡)
37 ssid 3879 . . . . . . 7 {1o} ⊆ {1o}
3812rnsnop 5920 . . . . . . 7 ran {⟨1o, 1o⟩} = {1o}
3937, 38, 263sstr4i 3900 . . . . . 6 ran {⟨1o, 1o⟩} ⊆ dom {⟨1o, 1o⟩}
40 rneq 5649 . . . . . . 7 (𝑥 = {⟨1o, 1o⟩} → ran 𝑥 = ran {⟨1o, 1o⟩})
41 dmeq 5622 . . . . . . 7 (𝑥 = {⟨1o, 1o⟩} → dom 𝑥 = dom {⟨1o, 1o⟩})
4240, 41sseq12d 3890 . . . . . 6 (𝑥 = {⟨1o, 1o⟩} → (ran 𝑥 ⊆ dom 𝑥 ↔ ran {⟨1o, 1o⟩} ⊆ dom {⟨1o, 1o⟩}))
4339, 42mpbiri 250 . . . . 5 (𝑥 = {⟨1o, 1o⟩} → ran 𝑥 ⊆ dom 𝑥)
44 pm5.5 354 . . . . 5 ((∃𝑠𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → (((∃𝑠𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛)))
4536, 43, 44syl2anc 576 . . . 4 (𝑥 = {⟨1o, 1o⟩} → (((∃𝑠𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛)))
46 breq 4931 . . . . . 6 (𝑥 = {⟨1o, 1o⟩} → ((𝑓𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛)))
4746ralbidv 3147 . . . . 5 (𝑥 = {⟨1o, 1o⟩} → (∀𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛)))
4847exbidv 1880 . . . 4 (𝑥 = {⟨1o, 1o⟩} → (∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∃𝑓𝑛 ∈ ω (𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛)))
4945, 48bitrd 271 . . 3 (𝑥 = {⟨1o, 1o⟩} → (((∃𝑠𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓𝑛 ∈ ω (𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛)))
50 ax-dc 9666 . . 3 ((∃𝑠𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛))
5122, 49, 50vtocl 3478 . 2 𝑓𝑛 ∈ ω (𝑓𝑛){⟨1o, 1o⟩} (𝑓‘suc 𝑛)
5221, 51exlimiiv 1890 1 ω ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wex 1742  wcel 2050  wne 2967  wral 3088  Vcvv 3415  wss 3829  c0 4178  {csn 4441  cop 4447   class class class wbr 4929  dom cdm 5407  ran crn 5408  suc csuc 6031  Fun wfun 6182  cfv 6188  ωcom 7396  1oc1o 7898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186  ax-un 7279  ax-dc 9666
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-ord 6032  df-on 6033  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-fv 6196  df-1o 7905
This theorem is referenced by:  axdc2lem  9668  axdc3lem  9670  axdc4lem  9675  axcclem  9677
  Copyright terms: Public domain W3C validator