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

Theorem grothpw 6731
Description: Derive the Axiom of Power Sets ax-pow 3503 from the Tarksi-Grothendieck axiom ax-groth 6728. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 3503 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 6728 . . . 4
2 biid 226 . . . . . 6
3 dfss2 2652 . . . . . . . . 9
4 df-pw 3067 . . . . . . . . . . . 12
54abeq2i 2030 . . . . . . . . . . 11
65imbi1i 315 . . . . . . . . . 10
76albii 1361 . . . . . . . . 9
83, 7bitri 239 . . . . . . . 8
9 dfss2 2652 . . . . . . . . . 10
10 df-pw 3067 . . . . . . . . . . . . 13
1110abeq2i 2030 . . . . . . . . . . . 12
1211imbi1i 315 . . . . . . . . . . 11
1312albii 1361 . . . . . . . . . 10
149, 13bitri 239 . . . . . . . . 9
1514rexbii 2161 . . . . . . . 8
168, 15anbi12i 679 . . . . . . 7
1716ralbii 2160 . . . . . 6
18 df-ral 2142 . . . . . . 7
19 vex 2338 . . . . . . . . . 10
2019elpw 3071 . . . . . . . . 9
2120imbi1i 315 . . . . . . . 8
2221albii 1361 . . . . . . 7
2318, 22bitri 239 . . . . . 6
242, 17, 233anbi123i 1112 . . . . 5
2524exbii 1380 . . . 4
261, 25mpbir 198 . . 3
27 simpl 440 . . . . . . . . 9
2827ralimi 2204 . . . . . . . 8
29 pweq 3068 . . . . . . . . . 10
3029sseq1d 2686 . . . . . . . . 9
3130rcla4cv 2418 . . . . . . . 8
3228, 31syl 14 . . . . . . 7
3332anim2i 550 . . . . . 6
34333adant3 950 . . . . 5
35 pm3.35 568 . . . . 5
36 vex 2338 . . . . . 6
3736ssex 3476 . . . . 5
3834, 35, 373syl 17 . . . 4
3938exlimiv 1729 . . 3
4026, 39ax-mp 8 . 2
41 ssid 2678 . . . . . 6
42 elpwg 3072 . . . . . 6
4341, 42mpbiri 223 . . . . 5
44 pweq 3068 . . . . . . 7
4544eleq2d 1995 . . . . . 6
4645cla4egv 2406 . . . . 5
4743, 46mpd 13 . . . 4
48 elex 2343 . . . . 5
4948exlimiv 1729 . . . 4
5047, 49impbii 178 . . 3
5136elpw2 3485 . . . . 5
52 dfss2 2652 . . . . . 6
53 df-pw 3067 . . . . . . . . 9
5453abeq2i 2030 . . . . . . . 8
5554imbi1i 315 . . . . . . 7
5655albii 1361 . . . . . 6
5752, 56bitri 239 . . . . 5
58 dfss2 2652 . . . . . . 7
5958imbi1i 315 . . . . . 6
6059albii 1361 . . . . 5
6151, 57, 603bitri 262 . . . 4
6261exbii 1380 . . 3
6350, 62bitri 239 . 2
6440, 63mpbi 197 1
Colors of variables: wff set class
Syntax hints:   wi 4   wo 359   wa 360   w3a 912  wal 1341  wex 1346   wceq 1425   wcel 1427  wral 2138  wrex 2139  cvv 2335   wss 2638  cpw 3065   class class class wbr 3362   cen 5691
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-sep 3458  ax-groth 6728
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3an 914  df-ex 1347  df-sb 1602  df-clab 1917  df-cleq 1922  df-clel 1925  df-ral 2142  df-rex 2143  df-v 2337  df-in 2645  df-ss 2647  df-pw 3067
Copyright terms: Public domain