Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  grothpw Unicode version

Theorem grothpw 8328
 Description: Derive the Axiom of Power Sets ax-pow 4082 from the Tarksi-Grothendieck axiom ax-groth 8325. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 4082 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.)
Assertion
Ref Expression
grothpw
Distinct variable group:   ,,,

Proof of Theorem grothpw
StepHypRef Expression
1 axgroth5 8326 . . 3
2 simpl 445 . . . . . . . . 9
32ralimi 2580 . . . . . . . 8
4 pweq 3533 . . . . . . . . . 10
54sseq1d 3126 . . . . . . . . 9
65rcla4cv 2818 . . . . . . . 8
73, 6syl 17 . . . . . . 7
87anim2i 555 . . . . . 6
983adant3 980 . . . . 5
10 pm3.35 573 . . . . 5
11 vex 2730 . . . . . 6
1211ssex 4055 . . . . 5
139, 10, 123syl 20 . . . 4
1413exlimiv 2023 . . 3
151, 14ax-mp 10 . 2
16 pwidg 3541 . . . . 5
17 pweq 3533 . . . . . . 7
1817eleq2d 2320 . . . . . 6
1918cla4egv 2806 . . . . 5
2016, 19mpd 16 . . . 4
21 elex 2735 . . . . 5
2221exlimiv 2023 . . . 4
2320, 22impbii 182 . . 3
2411elpw2 4064 . . . . 5
25 pwss 3543 . . . . . 6
26 dfss2 3092 . . . . . . . 8
2726imbi1i 317 . . . . . . 7
2827albii 1554 . . . . . 6
2925, 28bitri 242 . . . . 5
3024, 29bitri 242 . . . 4
3130exbii 1580 . . 3
3223, 31bitri 242 . 2
3315, 32mpbi 201 1
 Colors of variables: wff set class Syntax hints:   wi 6   wo 359   wa 360   w3a 939  wal 1532  wex 1537   wceq 1619   wcel 1621  wral 2509  wrex 2510  cvv 2727   wss 3078  cpw 3530   class class class wbr 3920   cen 6746 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-groth 8325 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ral 2513  df-rex 2514  df-v 2729  df-in 3085  df-ss 3089  df-pw 3532
 Copyright terms: Public domain W3C validator