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

Theorem grothpw 6816
Description: Derive the Axiom of Power Sets ax-pow 3499 from the Tarksi-Grothendieck axiom ax-groth 6813. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 3499 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 6813 . . . 4
2 biid 224 . . . . . 6
3 dfss2 2646 . . . . . . . . 9
4 df-pw 3062 . . . . . . . . . . . 12
54abeq2i 2018 . . . . . . . . . . 11
65imbi1i 312 . . . . . . . . . 10
76albii 1349 . . . . . . . . 9
83, 7bitri 237 . . . . . . . 8
9 dfss2 2646 . . . . . . . . . 10
10 df-pw 3062 . . . . . . . . . . . . 13
1110abeq2i 2018 . . . . . . . . . . . 12
1211imbi1i 312 . . . . . . . . . . 11
1312albii 1349 . . . . . . . . . 10
149, 13bitri 237 . . . . . . . . 9
1514rexbii 2148 . . . . . . . 8
168, 15anbi12i 672 . . . . . . 7
1716ralbii 2147 . . . . . 6
18 df-ral 2129 . . . . . . 7
19 vex 2325 . . . . . . . . . 10
2019elpw 3066 . . . . . . . . 9
2120imbi1i 312 . . . . . . . 8
2221albii 1349 . . . . . . 7
2318, 22bitri 237 . . . . . 6
242, 17, 233anbi123i 1100 . . . . 5
2524exbii 1368 . . . 4
261, 25mpbir 197 . . 3
27 simpl 435 . . . . . . . . 9
2827ralimi 2191 . . . . . . . 8
29 pweq 3063 . . . . . . . . . 10
3029sseq1d 2680 . . . . . . . . 9
3130rcla4cv 2405 . . . . . . . 8
3228, 31syl 14 . . . . . . 7
3332anim2i 545 . . . . . 6
34333adant3 936 . . . . 5
35 pm3.35 563 . . . . 5
36 vex 2325 . . . . . 6
3736ssex 3472 . . . . 5
3834, 35, 373syl 17 . . . 4
3938exlimiv 1717 . . 3
4026, 39ax-mp 8 . 2
41 ssid 2672 . . . . . 6
42 elpwg 3067 . . . . . 6
4341, 42mpbiri 221 . . . . 5
44 pweq 3063 . . . . . . 7
4544eleq2d 1983 . . . . . 6
4645cla4egv 2393 . . . . 5
4743, 46mpd 13 . . . 4
48 elex 2330 . . . . 5
4948exlimiv 1717 . . . 4
5047, 49impbii 177 . . 3
5136elpw2 3481 . . . . 5
52 dfss2 2646 . . . . . 6
53 df-pw 3062 . . . . . . . . 9
5453abeq2i 2018 . . . . . . . 8
5554imbi1i 312 . . . . . . 7
5655albii 1349 . . . . . 6
5752, 56bitri 237 . . . . 5
58 dfss2 2646 . . . . . . 7
5958imbi1i 312 . . . . . 6
6059albii 1349 . . . . 5
6151, 57, 603bitri 259 . . . 4
6261exbii 1368 . . 3
6350, 62bitri 237 . 2
6440, 63mpbi 196 1
Colors of variables: wff set class
Syntax hints:   wi 4   wo 355   wa 356   w3a 898  wal 1329  wex 1334   wceq 1413   wcel 1415  wral 2125  wrex 2126  cvv 2322   wss 2632  cpw 3060   class class class wbr 3358   cen 5746
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-sep 3454  ax-groth 6813
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3an 900  df-ex 1335  df-sb 1590  df-clab 1905  df-cleq 1910  df-clel 1913  df-ral 2129  df-rex 2130  df-v 2324  df-in 2639  df-ss 2641  df-pw 3062
Copyright terms: Public domain