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

Theorem grothpw 6789
Description: Derive the Axiom of Power Sets ax-pow 3655 from the Tarksi-Grothendieck axiom ax-groth 6786. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 3655 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.)
Assertion
Ref Expression
grothpw |- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
Distinct variable group:   x,y,z,w

Proof of Theorem grothpw
StepHypRef Expression
1 ax-groth 6786 . . . 4 |- E.y(x e. y /\ A.z e. y (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)) /\ A.z(z C_ y -> (z ~~ y \/ z e. y)))
2 biid 273 . . . . . 6 |- (x e. y <-> x e. y)
3 dfss2 2815 . . . . . . . . 9 |- (~Pz C_ y <-> A.w(w e. ~Pz -> w e. y))
4 df-pw 3222 . . . . . . . . . . . 12 |- ~Pz = {w | w C_ z}
54abeq2i 2201 . . . . . . . . . . 11 |- (w e. ~Pz <-> w C_ z)
65imbi1i 369 . . . . . . . . . 10 |- ((w e. ~Pz -> w e. y) <-> (w C_ z -> w e. y))
76albii 1535 . . . . . . . . 9 |- (A.w(w e. ~Pz -> w e. y) <-> A.w(w C_ z -> w e. y))
83, 7bitri 286 . . . . . . . 8 |- (~Pz C_ y <-> A.w(w C_ z -> w e. y))
9 dfss2 2815 . . . . . . . . . 10 |- (~Pz C_ w <-> A.v(v e. ~Pz -> v e. w))
10 df-pw 3222 . . . . . . . . . . . . 13 |- ~Pz = {v | v C_ z}
1110abeq2i 2201 . . . . . . . . . . . 12 |- (v e. ~Pz <-> v C_ z)
1211imbi1i 369 . . . . . . . . . . 11 |- ((v e. ~Pz -> v e. w) <-> (v C_ z -> v e. w))
1312albii 1535 . . . . . . . . . 10 |- (A.v(v e. ~Pz -> v e. w) <-> A.v(v C_ z -> v e. w))
149, 13bitri 286 . . . . . . . . 9 |- (~Pz C_ w <-> A.v(v C_ z -> v e. w))
1514rexbii 2333 . . . . . . . 8 |- (E.w e. y ~Pz C_ w <-> E.w e. y A.v(v C_ z -> v e. w))
168, 15anbi12i 789 . . . . . . 7 |- ((~Pz C_ y /\ E.w e. y ~Pz C_ w) <-> (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)))
1716ralbii 2332 . . . . . 6 |- (A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) <-> A.z e. y (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)))
18 df-ral 2314 . . . . . . 7 |- (A.z e. ~P y(z ~~ y \/ z e. y) <-> A.z(z e. ~Py -> (z ~~ y \/ z e. y)))
19 visset 2502 . . . . . . . . . 10 |- z e. _V
2019elpw 3226 . . . . . . . . 9 |- (z e. ~Py <-> z C_ y)
2120imbi1i 369 . . . . . . . 8 |- ((z e. ~Py -> (z ~~ y \/ z e. y)) <-> (z C_ y -> (z ~~ y \/ z e. y)))
2221albii 1535 . . . . . . 7 |- (A.z(z e. ~Py -> (z ~~ y \/ z e. y)) <-> A.z(z C_ y -> (z ~~ y \/ z e. y)))
2318, 22bitri 286 . . . . . 6 |- (A.z e. ~P y(z ~~ y \/ z e. y) <-> A.z(z C_ y -> (z ~~ y \/ z e. y)))
242, 17, 233anbi123i 1235 . . . . 5 |- ((x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) <-> (x e. y /\ A.z e. y (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)) /\ A.z(z C_ y -> (z ~~ y \/ z e. y))))
2524exbii 1553 . . . 4 |- (E.y(x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) <-> E.y(x e. y /\ A.z e. y (A.w(w C_ z -> w e. y) /\ E.w e. y A.v(v C_ z -> v e. w)) /\ A.z(z C_ y -> (z ~~ y \/ z e. y))))
261, 25mpbir 238 . . 3 |- E.y(x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y))
27 simpl 507 . . . . . . . . 9 |- ((~Pz C_ y /\ E.w e. y ~Pz C_ w) -> ~Pz C_ y)
2827ralimi 2373 . . . . . . . 8 |- (A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) -> A.z e. y ~Pz C_ y)
29 pweq 3223 . . . . . . . . . 10 |- (z = x -> ~Pz = ~Px)
3029sseq1d 2847 . . . . . . . . 9 |- (z = x -> (~Pz C_ y <-> ~Px C_ y))
3130rcla4cv 2588 . . . . . . . 8 |- (A.z e. y ~Pz C_ y -> (x e. y -> ~Px C_ y))
3228, 31syl 13 . . . . . . 7 |- (A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) -> (x e. y -> ~Px C_ y))
3332anim2i 639 . . . . . 6 |- ((x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w)) -> (x e. y /\ (x e. y -> ~Px C_ y)))
34333adant3 1075 . . . . 5 |- ((x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) -> (x e. y /\ (x e. y -> ~Px C_ y)))
35 pm3.35 660 . . . . 5 |- ((x e. y /\ (x e. y -> ~Px C_ y)) -> ~Px C_ y)
36 visset 2502 . . . . . 6 |- y e. _V
3736ssex 3628 . . . . 5 |- (~Px C_ y -> ~Px e. _V)
3834, 35, 373syl 17 . . . 4 |- ((x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) -> ~Px e. _V)
3938exlimiv 1892 . . 3 |- (E.y(x e. y /\ A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) /\ A.z e. ~P y(z ~~ y \/ z e. y)) -> ~Px e. _V)
4026, 39ax-mp 7 . 2 |- ~Px e. _V
41 ssid 2839 . . . . . 6 |- ~Px C_ ~Px
42 elpwg 3227 . . . . . 6 |- (~Px e. _V -> (~Px e. ~P~Px <-> ~Px C_ ~Px))
4341, 42mpbiri 270 . . . . 5 |- (~Px e. _V -> ~Px e. ~P~Px)
44 pweq 3223 . . . . . . 7 |- (y = ~Px -> ~Py = ~P~Px)
4544eleq2d 2162 . . . . . 6 |- (y = ~Px -> (~Px e. ~Py <-> ~Px e. ~P~Px))
4645cla4egv 2576 . . . . 5 |- (~Px e. _V -> (~Px e. ~P~Px -> E.y~Px e. ~Py))
4743, 46mpd 12 . . . 4 |- (~Px e. _V -> E.y~Px e. ~Py)
48 elisset 2508 . . . . 5 |- (~Px e. ~Py -> ~Px e. _V)
4948exlimiv 1892 . . . 4 |- (E.y~Px e. ~Py -> ~Px e. _V)
5047, 49impbii 213 . . 3 |- (~Px e. _V <-> E.y~Px e. ~Py)
5136elpw2 3637 . . . . 5 |- (~Px e. ~Py <-> ~Px C_ y)
52 dfss2 2815 . . . . . 6 |- (~Px C_ y <-> A.z(z e. ~Px -> z e. y))
53 df-pw 3222 . . . . . . . . 9 |- ~Px = {z | z C_ x}
5453abeq2i 2201 . . . . . . . 8 |- (z e. ~Px <-> z C_ x)
5554imbi1i 369 . . . . . . 7 |- ((z e. ~Px -> z e. y) <-> (z C_ x -> z e. y))
5655albii 1535 . . . . . 6 |- (A.z(z e. ~Px -> z e. y) <-> A.z(z C_ x -> z e. y))
5752, 56bitri 286 . . . . 5 |- (~Px C_ y <-> A.z(z C_ x -> z e. y))
58 dfss2 2815 . . . . . . 7 |- (z C_ x <-> A.w(w e. z -> w e. x))
5958imbi1i 369 . . . . . 6 |- ((z C_ x -> z e. y) <-> (A.w(w e. z -> w e. x) -> z e. y))
6059albii 1535 . . . . 5 |- (A.z(z C_ x -> z e. y) <-> A.z(A.w(w e. z -> w e. x) -> z e. y))
6151, 57, 603bitri 314 . . . 4 |- (~Px e. ~Py <-> A.z(A.w(w e. z -> w e. x) -> z e. y))
6261exbii 1553 . . 3 |- (E.y~Px e. ~Py <-> E.yA.z(A.w(w e. z -> w e. x) -> z e. y))
6350, 62bitri 286 . 2 |- (~Px e. _V <-> E.yA.z(A.w(w e. z -> w e. x) -> z e. y))
6440, 63mpbi 237 1 |- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
Colors of variables: wff set class
Syntax hints:   -> wi 3   \/ wo 417   /\ wa 418   /\ w3a 1037  A.wal 1515  E.wex 1520   = wceq 1592   e. wcel 1594  A.wral 2310  E.wrex 2311  _Vcvv 2499   C_ wss 2801  ~Pcpw 3220   class class class wbr 3509   ~~ cen 5748
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-sep 3609  ax-groth 6786
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3an 1039  df-ex 1521  df-sb 1765  df-clab 2080  df-cleq 2085  df-clel 2088  df-ral 2314  df-rex 2315  df-v 2501  df-in 2808  df-ss 2810  df-pw 3222
Copyright terms: Public domain