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

Theorem grothomex 9339
Description: The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 8233). Note that our proof depends on neither the Axiom of Infinity nor Regularity. (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
grothomex ω ∈ V

Proof of Theorem grothomex
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r111 8331 . . . 4 𝑅1:On–1-1→V
2 omsson 6773 . . . 4 ω ⊆ On
3 f1ores 5888 . . . 4 ((𝑅1:On–1-1→V ∧ ω ⊆ On) → (𝑅1 ↾ ω):ω–1-1-onto→(𝑅1 “ ω))
41, 2, 3mp2an 695 . . 3 (𝑅1 ↾ ω):ω–1-1-onto→(𝑅1 “ ω)
5 f1of1 5873 . . 3 ((𝑅1 ↾ ω):ω–1-1-onto→(𝑅1 “ ω) → (𝑅1 ↾ ω):ω–1-1→(𝑅1 “ ω))
64, 5ax-mp 5 . 2 (𝑅1 ↾ ω):ω–1-1→(𝑅1 “ ω)
7 r1fnon 8323 . . . . . . . 8 𝑅1 Fn On
8 fvelimab 5987 . . . . . . . 8 ((𝑅1 Fn On ∧ ω ⊆ On) → (𝑤 ∈ (𝑅1 “ ω) ↔ ∃𝑥 ∈ ω (𝑅1𝑥) = 𝑤))
97, 2, 8mp2an 695 . . . . . . 7 (𝑤 ∈ (𝑅1 “ ω) ↔ ∃𝑥 ∈ ω (𝑅1𝑥) = 𝑤)
10 fveq2 5927 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑅1𝑥) = (𝑅1‘∅))
1110eleq1d 2567 . . . . . . . . . 10 (𝑥 = ∅ → ((𝑅1𝑥) ∈ 𝑦 ↔ (𝑅1‘∅) ∈ 𝑦))
12 fveq2 5927 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑅1𝑥) = (𝑅1𝑤))
1312eleq1d 2567 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝑅1𝑥) ∈ 𝑦 ↔ (𝑅1𝑤) ∈ 𝑦))
14 fveq2 5927 . . . . . . . . . . 11 (𝑥 = suc 𝑤 → (𝑅1𝑥) = (𝑅1‘suc 𝑤))
1514eleq1d 2567 . . . . . . . . . 10 (𝑥 = suc 𝑤 → ((𝑅1𝑥) ∈ 𝑦 ↔ (𝑅1‘suc 𝑤) ∈ 𝑦))
16 r10 8324 . . . . . . . . . . . . 13 (𝑅1‘∅) = ∅
1716eleq1i 2574 . . . . . . . . . . . 12 ((𝑅1‘∅) ∈ 𝑦 ↔ ∅ ∈ 𝑦)
1817biimpri 213 . . . . . . . . . . 11 (∅ ∈ 𝑦 → (𝑅1‘∅) ∈ 𝑦)
1918adantr 474 . . . . . . . . . 10 ((∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) → (𝑅1‘∅) ∈ 𝑦)
20 pweq 3981 . . . . . . . . . . . . . . 15 (𝑧 = (𝑅1𝑤) → 𝒫 𝑧 = 𝒫 (𝑅1𝑤))
2120eleq1d 2567 . . . . . . . . . . . . . 14 (𝑧 = (𝑅1𝑤) → (𝒫 𝑧𝑦 ↔ 𝒫 (𝑅1𝑤) ∈ 𝑦))
2221rspccv 3168 . . . . . . . . . . . . 13 (∀𝑧𝑦 𝒫 𝑧𝑦 → ((𝑅1𝑤) ∈ 𝑦 → 𝒫 (𝑅1𝑤) ∈ 𝑦))
23 nnon 6775 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ω → 𝑤 ∈ On)
24 r1suc 8326 . . . . . . . . . . . . . . . 16 (𝑤 ∈ On → (𝑅1‘suc 𝑤) = 𝒫 (𝑅1𝑤))
2523, 24syl 17 . . . . . . . . . . . . . . 15 (𝑤 ∈ ω → (𝑅1‘suc 𝑤) = 𝒫 (𝑅1𝑤))
2625eleq1d 2567 . . . . . . . . . . . . . 14 (𝑤 ∈ ω → ((𝑅1‘suc 𝑤) ∈ 𝑦 ↔ 𝒫 (𝑅1𝑤) ∈ 𝑦))
2726biimprcd 235 . . . . . . . . . . . . 13 (𝒫 (𝑅1𝑤) ∈ 𝑦 → (𝑤 ∈ ω → (𝑅1‘suc 𝑤) ∈ 𝑦))
2822, 27syl6 34 . . . . . . . . . . . 12 (∀𝑧𝑦 𝒫 𝑧𝑦 → ((𝑅1𝑤) ∈ 𝑦 → (𝑤 ∈ ω → (𝑅1‘suc 𝑤) ∈ 𝑦)))
2928com3r 83 . . . . . . . . . . 11 (𝑤 ∈ ω → (∀𝑧𝑦 𝒫 𝑧𝑦 → ((𝑅1𝑤) ∈ 𝑦 → (𝑅1‘suc 𝑤) ∈ 𝑦)))
3029adantld 476 . . . . . . . . . 10 (𝑤 ∈ ω → ((∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) → ((𝑅1𝑤) ∈ 𝑦 → (𝑅1‘suc 𝑤) ∈ 𝑦)))
3111, 13, 15, 19, 30finds2 6798 . . . . . . . . 9 (𝑥 ∈ ω → ((∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) → (𝑅1𝑥) ∈ 𝑦))
32 eleq1 2571 . . . . . . . . . 10 ((𝑅1𝑥) = 𝑤 → ((𝑅1𝑥) ∈ 𝑦𝑤𝑦))
3332biimpd 214 . . . . . . . . 9 ((𝑅1𝑥) = 𝑤 → ((𝑅1𝑥) ∈ 𝑦𝑤𝑦))
3431, 33syl9 74 . . . . . . . 8 (𝑥 ∈ ω → ((𝑅1𝑥) = 𝑤 → ((∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) → 𝑤𝑦)))
3534rexlimiv 2902 . . . . . . 7 (∃𝑥 ∈ ω (𝑅1𝑥) = 𝑤 → ((∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) → 𝑤𝑦))
369, 35sylbi 202 . . . . . 6 (𝑤 ∈ (𝑅1 “ ω) → ((∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) → 𝑤𝑦))
3736com12 32 . . . . 5 ((∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) → (𝑤 ∈ (𝑅1 “ ω) → 𝑤𝑦))
3837ssrdv 3460 . . . 4 ((∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) → (𝑅1 “ ω) ⊆ 𝑦)
39 vex 3069 . . . . 5 𝑦 ∈ V
4039ssex 4580 . . . 4 ((𝑅1 “ ω) ⊆ 𝑦 → (𝑅1 “ ω) ∈ V)
4138, 40syl 17 . . 3 ((∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) → (𝑅1 “ ω) ∈ V)
42 0ex 4568 . . . 4 ∅ ∈ V
43 eleq1 2571 . . . . . 6 (𝑥 = ∅ → (𝑥𝑦 ↔ ∅ ∈ 𝑦))
4443anbi1d 728 . . . . 5 (𝑥 = ∅ → ((𝑥𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) ↔ (∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦)))
4544exbidv 1799 . . . 4 (𝑥 = ∅ → (∃𝑦(𝑥𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) ↔ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦)))
46 axgroth6 9338 . . . . 5 𝑦(𝑥𝑦 ∧ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))
47 simpr 470 . . . . . . . 8 ((𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦) → 𝒫 𝑧𝑦)
4847ralimi 2831 . . . . . . 7 (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦) → ∀𝑧𝑦 𝒫 𝑧𝑦)
4948anim2i 585 . . . . . 6 ((𝑥𝑦 ∧ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦)) → (𝑥𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦))
50493adant3 1064 . . . . 5 ((𝑥𝑦 ∧ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦)) → (𝑥𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦))
5146, 50eximii 1740 . . . 4 𝑦(𝑥𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦)
5242, 45, 51vtocl 3121 . . 3 𝑦(∅ ∈ 𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦)
5341, 52exlimiiv 1808 . 2 (𝑅1 “ ω) ∈ V
54 f1dmex 6840 . 2 (((𝑅1 ↾ ω):ω–1-1→(𝑅1 “ ω) ∧ (𝑅1 “ ω) ∈ V) → ω ∈ V)
556, 53, 54mp2an 695 1 ω ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191  wa 378  w3a 1021   = wceq 1468  wex 1692  wcel 1937  wral 2791  wrex 2792  Vcvv 3066  wss 3426  c0 3757  𝒫 cpw 3978   class class class wbr 4434  cres 4882  cima 4883  Oncon0 5474  suc csuc 5476   Fn wfn 5628  1-1wf1 5630  1-1-ontowf1o 5632  cfv 5633  ωcom 6769  csdm 7651  𝑅1cr1 8318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-rep 4548  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659  ax-groth 9333
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-iun 4309  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-om 6770  df-wrecs 7105  df-recs 7167  df-rdg 7205  df-er 7440  df-en 7653  df-dom 7654  df-sdom 7655  df-r1 8320
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator