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

Theorem grothpw 6966
Description: Derive the Axiom of Power Sets ax-pow 3536 from the Tarksi-Grothendieck axiom ax-groth 6963. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 3536 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 6963 . . . 4
2 biid 225 . . . . . 6
3 dfss2 2651 . . . . . . . . 9
4 df-pw 3075 . . . . . . . . . . . 12
54abeq2i 2019 . . . . . . . . . . 11
65imbi1i 313 . . . . . . . . . 10
76albii 1350 . . . . . . . . 9
83, 7bitri 238 . . . . . . . 8
9 dfss2 2651 . . . . . . . . . 10
10 df-pw 3075 . . . . . . . . . . . . 13
1110abeq2i 2019 . . . . . . . . . . . 12
1211imbi1i 313 . . . . . . . . . . 11
1312albii 1350 . . . . . . . . . 10
149, 13bitri 238 . . . . . . . . 9
1514rexbii 2150 . . . . . . . 8
168, 15anbi12i 673 . . . . . . 7
1716ralbii 2149 . . . . . 6
18 df-ral 2131 . . . . . . 7
19 vex 2330 . . . . . . . . . 10
2019elpw 3079 . . . . . . . . 9
2120imbi1i 313 . . . . . . . 8
2221albii 1350 . . . . . . 7
2318, 22bitri 238 . . . . . 6
242, 17, 233anbi123i 1101 . . . . 5
2524exbii 1369 . . . 4
261, 25mpbir 198 . . 3
27 simpl 436 . . . . . . . . 9
2827ralimi 2193 . . . . . . . 8
29 pweq 3076 . . . . . . . . . 10
3029sseq1d 2685 . . . . . . . . 9
3130rcla4cv 2410 . . . . . . . 8
3228, 31syl 15 . . . . . . 7
3332anim2i 546 . . . . . 6
34333adant3 937 . . . . 5
35 pm3.35 564 . . . . 5
36 vex 2330 . . . . . 6
3736ssex 3509 . . . . 5
3834, 35, 373syl 18 . . . 4
3938exlimiv 1718 . . 3
4026, 39ax-mp 8 . 2
41 ssid 2677 . . . . . 6
42 elpwg 3080 . . . . . 6
4341, 42mpbiri 222 . . . . 5
44 pweq 3076 . . . . . . 7
4544eleq2d 1984 . . . . . 6
4645cla4egv 2398 . . . . 5
4743, 46mpd 14 . . . 4
48 elex 2335 . . . . 5
4948exlimiv 1718 . . . 4
5047, 49impbii 178 . . 3
5136elpw2 3518 . . . . 5
52 dfss2 2651 . . . . . 6
53 df-pw 3075 . . . . . . . . 9
5453abeq2i 2019 . . . . . . . 8
5554imbi1i 313 . . . . . . 7
5655albii 1350 . . . . . 6
5752, 56bitri 238 . . . . 5
58 dfss2 2651 . . . . . . 7
5958imbi1i 313 . . . . . 6
6059albii 1350 . . . . 5
6151, 57, 603bitri 260 . . . 4
6261exbii 1369 . . 3
6350, 62bitri 238 . 2
6440, 63mpbi 197 1
Colors of variables: wff set class
Syntax hints:   wi 4   wo 356   wa 357   w3a 899  wal 1330  wex 1335   wceq 1414   wcel 1416  wral 2127  wrex 2128  cvv 2327   wss 2637  cpw 3073   class class class wbr 3396   cen 5865
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-sep 3491  ax-groth 6963
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1336  df-sb 1591  df-clab 1906  df-cleq 1911  df-clel 1914  df-ral 2131  df-rex 2132  df-v 2329  df-in 2644  df-ss 2648  df-pw 3075
Copyright terms: Public domain