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

Theorem grothpw 7617
Description: Derive the Axiom of Power Sets ax-pow 3671 from the Tarksi-Grothendieck axiom ax-groth 7614. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 3671 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 7614 . . . 4
2 biid 225 . . . . . 6
3 dfss2 2764 . . . . . . . . 9
4 df-pw 3196 . . . . . . . . . . . 12
54abeq2i 2131 . . . . . . . . . . 11
65imbi1i 313 . . . . . . . . . 10
76albii 1462 . . . . . . . . 9
83, 7bitri 238 . . . . . . . 8
9 dfss2 2764 . . . . . . . . . 10
10 df-pw 3196 . . . . . . . . . . . . 13
1110abeq2i 2131 . . . . . . . . . . . 12
1211imbi1i 313 . . . . . . . . . . 11
1312albii 1462 . . . . . . . . . 10
149, 13bitri 238 . . . . . . . . 9
1514rexbii 2262 . . . . . . . 8
168, 15anbi12i 673 . . . . . . 7
1716ralbii 2261 . . . . . 6
18 df-ral 2243 . . . . . . 7
19 vex 2443 . . . . . . . . . 10
2019elpw 3200 . . . . . . . . 9
2120imbi1i 313 . . . . . . . 8
2221albii 1462 . . . . . . 7
2318, 22bitri 238 . . . . . 6
242, 17, 233anbi123i 1101 . . . . 5
2524exbii 1481 . . . 4
261, 25mpbir 198 . . 3
27 simpl 436 . . . . . . . . 9
2827ralimi 2305 . . . . . . . 8
29 pweq 3197 . . . . . . . . . 10
3029sseq1d 2798 . . . . . . . . 9
3130rcla4cv 2523 . . . . . . . 8
3228, 31syl 15 . . . . . . 7
3332anim2i 546 . . . . . 6
34333adant3 937 . . . . 5
35 pm3.35 564 . . . . 5
36 vex 2443 . . . . . 6
3736ssex 3644 . . . . 5
3834, 35, 373syl 18 . . . 4
3938exlimiv 1830 . . 3
4026, 39ax-mp 8 . 2
41 ssid 2790 . . . . . 6
42 elpwg 3201 . . . . . 6
4341, 42mpbiri 222 . . . . 5
44 pweq 3197 . . . . . . 7
4544eleq2d 2096 . . . . . 6
4645cla4egv 2511 . . . . 5
4743, 46mpd 14 . . . 4
48 elex 2448 . . . . 5
4948exlimiv 1830 . . . 4
5047, 49impbii 178 . . 3
5136elpw2 3653 . . . . 5
52 dfss2 2764 . . . . . 6
53 df-pw 3196 . . . . . . . . 9
5453abeq2i 2131 . . . . . . . 8
5554imbi1i 313 . . . . . . 7
5655albii 1462 . . . . . 6
5752, 56bitri 238 . . . . 5
58 dfss2 2764 . . . . . . 7
5958imbi1i 313 . . . . . 6
6059albii 1462 . . . . 5
6151, 57, 603bitri 260 . . . 4
6261exbii 1481 . . 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 1442  wex 1447   wceq 1526   wcel 1528  wral 2239  wrex 2240  cvv 2440   wss 2750  cpw 3194   class class class wbr 3531   cen 6117
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-sep 3626  ax-groth 7614
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1448  df-sb 1703  df-clab 2018  df-cleq 2023  df-clel 2026  df-ral 2243  df-rex 2244  df-v 2442  df-in 2757  df-ss 2761  df-pw 3196
Copyright terms: Public domain