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

Theorem grothpw 7772
Description: Derive the Axiom of Power Sets ax-pow 3732 from the Tarksi-Grothendieck axiom ax-groth 7769. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 3732 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 7769 . . . 4
2 biid 225 . . . . . 6
3 dfss2 2824 . . . . . . . . 9
4 df-pw 3256 . . . . . . . . . . . 12
54abeq2i 2191 . . . . . . . . . . 11
65imbi1i 313 . . . . . . . . . 10
76albii 1465 . . . . . . . . 9
83, 7bitri 238 . . . . . . . 8
9 dfss2 2824 . . . . . . . . . 10
10 df-pw 3256 . . . . . . . . . . . . 13
1110abeq2i 2191 . . . . . . . . . . . 12
1211imbi1i 313 . . . . . . . . . . 11
1312albii 1465 . . . . . . . . . 10
149, 13bitri 238 . . . . . . . . 9
1514rexbii 2322 . . . . . . . 8
168, 15anbi12i 673 . . . . . . 7
1716ralbii 2321 . . . . . 6
18 df-ral 2303 . . . . . . 7
19 vex 2503 . . . . . . . . . 10
2019elpw 3260 . . . . . . . . 9
2120imbi1i 313 . . . . . . . 8
2221albii 1465 . . . . . . 7
2318, 22bitri 238 . . . . . 6
242, 17, 233anbi123i 1104 . . . . 5
2524exbii 1486 . . . 4
261, 25mpbir 198 . . 3
27 simpl 436 . . . . . . . . 9
2827ralimi 2365 . . . . . . . 8
29 pweq 3257 . . . . . . . . . 10
3029sseq1d 2858 . . . . . . . . 9
3130rcla4cv 2583 . . . . . . . 8
3228, 31syl 15 . . . . . . 7
3332anim2i 546 . . . . . 6
34333adant3 937 . . . . 5
35 pm3.35 564 . . . . 5
36 vex 2503 . . . . . 6
3736ssex 3705 . . . . 5
3834, 35, 373syl 18 . . . 4
3938exlimiv 1883 . . 3
4026, 39ax-mp 8 . 2
41 ssid 2850 . . . . . 6
42 elpwg 3261 . . . . . 6
4341, 42mpbiri 222 . . . . 5
44 pweq 3257 . . . . . . 7
4544eleq2d 2156 . . . . . 6
4645cla4egv 2571 . . . . 5
4743, 46mpd 14 . . . 4
48 elex 2508 . . . . 5
4948exlimiv 1883 . . . 4
5047, 49impbii 178 . . 3
5136elpw2 3714 . . . . 5
52 dfss2 2824 . . . . . 6
53 df-pw 3256 . . . . . . . . 9
5453abeq2i 2191 . . . . . . . 8
5554imbi1i 313 . . . . . . 7
5655albii 1465 . . . . . 6
5752, 56bitri 238 . . . . 5
58 dfss2 2824 . . . . . . 7
5958imbi1i 313 . . . . . 6
6059albii 1465 . . . . 5
6151, 57, 603bitri 260 . . . 4
6261exbii 1486 . . 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 1445  wex 1450   wceq 1531   wcel 1533  wral 2299  wrex 2300  cvv 2500   wss 2810  cpw 3254   class class class wbr 3591   cen 6245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-groth 7769
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1451  df-sb 1751  df-clab 2078  df-cleq 2083  df-clel 2086  df-ral 2303  df-rex 2304  df-v 2502  df-in 2817  df-ss 2821  df-pw 3256
Copyright terms: Public domain