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

Theorem grothpw 6715
Description: Derive the Axiom of Power Sets ax-pow 3499 from the Tarksi-Grothendieck axiom ax-groth 6712. 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 6712 . . . 4
2 biid 226 . . . . . 6
3 dfss2 2648 . . . . . . . . 9
4 df-pw 3063 . . . . . . . . . . . 12
54abeq2i 2030 . . . . . . . . . . 11
65imbi1i 315 . . . . . . . . . 10
76albii 1361 . . . . . . . . 9
83, 7bitri 239 . . . . . . . 8
9 dfss2 2648 . . . . . . . . . 10
10 df-pw 3063 . . . . . . . . . . . . 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 3067 . . . . . . . . 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 3064 . . . . . . . . . 10
3029sseq1d 2682 . . . . . . . . 9
3130rcla4cv 2418 . . . . . . . 8
3228, 31syl 14 . . . . . . 7
3332anim2i 550 . . . . . 6
34333adant3 950 . . . . 5
35 pm3.35 568 . . . . 5
36 vex 2338 . . . . . 6
3736ssex 3472 . . . . 5
3834, 35, 373syl 17 . . . 4
3938exlimiv 1729 . . 3
4026, 39ax-mp 8 . 2
41 ssid 2674 . . . . . 6
42 elpwg 3068 . . . . . 6
4341, 42mpbiri 223 . . . . 5
44 pweq 3064 . . . . . . 7
4544eleq2d 1995 . . . . . 6
4645cla4egv 2406 . . . . 5
4743, 46mpd 13 . . . 4
48 elex 2343 . . . . 5
4948exlimiv 1729 . . . 4
5047, 49impbii 178 . . 3
5136elpw2 3481 . . . . 5
52 dfss2 2648 . . . . . 6
53 df-pw 3063 . . . . . . . . 9
5453abeq2i 2030 . . . . . . . 8
5554imbi1i 315 . . . . . . 7
5655albii 1361 . . . . . 6
5752, 56bitri 239 . . . . 5
58 dfss2 2648 . . . . . . 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 2634  cpw 3061   class class class wbr 3358   cen 5678
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 3454  ax-groth 6712
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 2641  df-ss 2643  df-pw 3063
Copyright terms: Public domain