Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Theorem grothpw 7848
 Description: Derive the Axiom of Power Sets ax-pow 3759 from the Tarksi-Grothendieck axiom ax-groth 7845. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 3759 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 ax-groth 7845 . . . 4
2 biid 225 . . . . . 6
3 dfss2 2824 . . . . . . . . 9
4 df-pw 3260 . . . . . . . . . . . 12
54abeq2i 2183 . . . . . . . . . . 11
65imbi1i 313 . . . . . . . . . 10
76albii 1470 . . . . . . . . 9
83, 7bitri 238 . . . . . . . 8
9 dfss2 2824 . . . . . . . . . 10
10 df-pw 3260 . . . . . . . . . . . . 13
1110abeq2i 2183 . . . . . . . . . . . 12
1211imbi1i 313 . . . . . . . . . . 11
1312albii 1470 . . . . . . . . . 10
149, 13bitri 238 . . . . . . . . 9
1514rexbii 2314 . . . . . . . 8
168, 15anbi12i 673 . . . . . . 7
1716ralbii 2313 . . . . . 6
18 df-ral 2295 . . . . . . 7
19 vex 2495 . . . . . . . . . 10
2019elpw 3264 . . . . . . . . 9
2120imbi1i 313 . . . . . . . 8
2221albii 1470 . . . . . . 7
2318, 22bitri 238 . . . . . 6
242, 17, 233anbi123i 1108 . . . . 5
2524exbii 1491 . . . 4
261, 25mpbir 198 . . 3
27 simpl 437 . . . . . . . . 9
2827ralimi 2357 . . . . . . . 8
29 pweq 3261 . . . . . . . . . 10
3029sseq1d 2858 . . . . . . . . 9
3130rcla4cv 2575 . . . . . . . 8
3228, 31syl 15 . . . . . . 7
3332anim2i 547 . . . . . 6
34333adant3 941 . . . . 5
35 pm3.35 565 . . . . 5
36 vex 2495 . . . . . 6
3736ssex 3732 . . . . 5
3834, 35, 373syl 18 . . . 4
3938exlimiv 1885 . . 3
4026, 39ax-mp 8 . 2
41 ssid 2850 . . . . . 6
42 elpwg 3265 . . . . . 6
4341, 42mpbiri 222 . . . . 5
44 pweq 3261 . . . . . . 7
4544eleq2d 2148 . . . . . 6
4645cla4egv 2563 . . . . 5
4743, 46mpd 14 . . . 4
48 elex 2500 . . . . 5
4948exlimiv 1885 . . . 4
5047, 49impbii 178 . . 3
5136elpw2 3741 . . . . 5
52 dfss2 2824 . . . . . 6
53 df-pw 3260 . . . . . . . . 9
5453abeq2i 2183 . . . . . . . 8
5554imbi1i 313 . . . . . . 7
5655albii 1470 . . . . . 6
5752, 56bitri 238 . . . . 5
58 dfss2 2824 . . . . . . 7
5958imbi1i 313 . . . . . 6
6059albii 1470 . . . . 5
6151, 57, 603bitri 260 . . . 4
6261exbii 1491 . . 3
6350, 62bitri 238 . 2
6440, 63mpbi 197 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 356   wa 357   w3a 903  wal 1450  wex 1455   wceq 1536   wcel 1538  wral 2291  wrex 2292  cvv 2492   wss 2810  cpw 3258   class class class wbr 3600   cen 6285 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-sep 3715  ax-groth 7845 This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 905  df-ex 1456  df-sb 1754  df-clab 2070  df-cleq 2075  df-clel 2078  df-ral 2295  df-rex 2296  df-v 2494  df-in 2817  df-ss 2821  df-pw 3260