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

Theorem grothpw 6701
Description: Derive the Axiom of Power Sets ax-pow 3503 from the Tarksi-Grothendieck axiom ax-groth 6698. 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 |- 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 6698 . . . 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 226 . . . . . 6 |- (x e. y <-> x e. y)
3 dfss2 2656 . . . . . . . . 9 |- (~Pz C_ y <-> A.w(w e. ~Pz -> w e. y))
4 df-pw 3067 . . . . . . . . . . . 12 |- ~Pz = {w | w C_ z}
54abeq2i 2039 . . . . . . . . . . 11 |- (w e. ~Pz <-> w C_ z)
65imbi1i 315 . . . . . . . . . 10 |- ((w e. ~Pz -> w e. y) <-> (w C_ z -> w e. y))
76albii 1370 . . . . . . . . 9 |- (A.w(w e. ~Pz -> w e. y) <-> A.w(w C_ z -> w e. y))
83, 7bitri 239 . . . . . . . 8 |- (~Pz C_ y <-> A.w(w C_ z -> w e. y))
9 dfss2 2656 . . . . . . . . . 10 |- (~Pz C_ w <-> A.v(v e. ~Pz -> v e. w))
10 df-pw 3067 . . . . . . . . . . . . 13 |- ~Pz = {v | v C_ z}
1110abeq2i 2039 . . . . . . . . . . . 12 |- (v e. ~Pz <-> v C_ z)
1211imbi1i 315 . . . . . . . . . . 11 |- ((v e. ~Pz -> v e. w) <-> (v C_ z -> v e. w))
1312albii 1370 . . . . . . . . . 10 |- (A.v(v e. ~Pz -> v e. w) <-> A.v(v C_ z -> v e. w))
149, 13bitri 239 . . . . . . . . 9 |- (~Pz C_ w <-> A.v(v C_ z -> v e. w))
1514rexbii 2170 . . . . . . . 8 |- (E.w e. y ~Pz C_ w <-> E.w e. y A.v(v C_ z -> v e. w))
168, 15anbi12i 683 . . . . . . 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 2169 . . . . . 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 2151 . . . . . . 7 |- (A.z e. ~P y(z ~~ y \/ z e. y) <-> A.z(z e. ~Py -> (z ~~ y \/ z e. y)))
19 vex 2346 . . . . . . . . . 10 |- z e. _V
2019elpw 3071 . . . . . . . . 9 |- (z e. ~Py <-> z C_ y)
2120imbi1i 315 . . . . . . . 8 |- ((z e. ~Py -> (z ~~ y \/ z e. y)) <-> (z C_ y -> (z ~~ y \/ z e. y)))
2221albii 1370 . . . . . . 7 |- (A.z(z e. ~Py -> (z ~~ y \/ z e. y)) <-> A.z(z C_ y -> (z ~~ y \/ z e. y)))
2318, 22bitri 239 . . . . . 6 |- (A.z e. ~P y(z ~~ y \/ z e. y) <-> A.z(z C_ y -> (z ~~ y \/ z e. y)))
242, 17, 233anbi123i 1121 . . . . 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 1389 . . . 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 198 . . 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 443 . . . . . . . . 9 |- ((~Pz C_ y /\ E.w e. y ~Pz C_ w) -> ~Pz C_ y)
2827ralimi 2212 . . . . . . . 8 |- (A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) -> A.z e. y ~Pz C_ y)
29 pweq 3068 . . . . . . . . . 10 |- (z = x -> ~Pz = ~Px)
3029sseq1d 2690 . . . . . . . . 9 |- (z = x -> (~Pz C_ y <-> ~Px C_ y))
3130rcla4cv 2426 . . . . . . . 8 |- (A.z e. y ~Pz C_ y -> (x e. y -> ~Px C_ y))
3228, 31syl 14 . . . . . . 7 |- (A.z e. y (~Pz C_ y /\ E.w e. y ~Pz C_ w) -> (x e. y -> ~Px C_ y))
3332anim2i 554 . . . . . 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 959 . . . . 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 572 . . . . 5 |- ((x e. y /\ (x e. y -> ~Px C_ y)) -> ~Px C_ y)
36 vex 2346 . . . . . 6 |- y e. _V
3736ssex 3476 . . . . 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 1738 . . 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 8 . 2 |- ~Px e. _V
41 ssid 2682 . . . . . 6 |- ~Px C_ ~Px
42 elpwg 3072 . . . . . 6 |- (~Px e. _V -> (~Px e. ~P~Px <-> ~Px C_ ~Px))
4341, 42mpbiri 223 . . . . 5 |- (~Px e. _V -> ~Px e. ~P~Px)
44 pweq 3068 . . . . . . 7 |- (y = ~Px -> ~Py = ~P~Px)
4544eleq2d 2004 . . . . . 6 |- (y = ~Px -> (~Px e. ~Py <-> ~Px e. ~P~Px))
4645cla4egv 2414 . . . . 5 |- (~Px e. _V -> (~Px e. ~P~Px -> E.y~Px e. ~Py))
4743, 46mpd 13 . . . 4 |- (~Px e. _V -> E.y~Px e. ~Py)
48 elex 2351 . . . . 5 |- (~Px e. ~Py -> ~Px e. _V)
4948exlimiv 1738 . . . 4 |- (E.y~Px e. ~Py -> ~Px e. _V)
5047, 49impbii 178 . . 3 |- (~Px e. _V <-> E.y~Px e. ~Py)
5136elpw2 3485 . . . . 5 |- (~Px e. ~Py <-> ~Px C_ y)
52 dfss2 2656 . . . . . 6 |- (~Px C_ y <-> A.z(z e. ~Px -> z e. y))
53 df-pw 3067 . . . . . . . . 9 |- ~Px = {z | z C_ x}
5453abeq2i 2039 . . . . . . . 8 |- (z e. ~Px <-> z C_ x)
5554imbi1i 315 . . . . . . 7 |- ((z e. ~Px -> z e. y) <-> (z C_ x -> z e. y))
5655albii 1370 . . . . . 6 |- (A.z(z e. ~Px -> z e. y) <-> A.z(z C_ x -> z e. y))
5752, 56bitri 239 . . . . 5 |- (~Px C_ y <-> A.z(z C_ x -> z e. y))
58 dfss2 2656 . . . . . . 7 |- (z C_ x <-> A.w(w e. z -> w e. x))
5958imbi1i 315 . . . . . 6 |- ((z C_ x -> z e. y) <-> (A.w(w e. z -> w e. x) -> z e. y))
6059albii 1370 . . . . 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 262 . . . 4 |- (~Px e. ~Py <-> A.z(A.w(w e. z -> w e. x) -> z e. y))
6261exbii 1389 . . 3 |- (E.y~Px e. ~Py <-> E.yA.z(A.w(w e. z -> w e. x) -> z e. y))
6350, 62bitri 239 . 2 |- (~Px e. _V <-> E.yA.z(A.w(w e. z -> w e. x) -> z e. y))
6440, 63mpbi 197 1 |- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
Colors of variables: wff set class
Syntax hints:   -> wi 4   \/ wo 360   /\ wa 361   /\ w3a 921  A.wal 1350  E.wex 1355   = wceq 1434   e. wcel 1436  A.wral 2147  E.wrex 2148  _Vcvv 2343   C_ wss 2642  ~Pcpw 3065   class class class wbr 3362   ~~ cen 5664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-sep 3458  ax-groth 6698
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-3an 923  df-ex 1356  df-sb 1611  df-clab 1926  df-cleq 1931  df-clel 1934  df-ral 2151  df-rex 2152  df-v 2345  df-in 2649  df-ss 2651  df-pw 3067
Copyright terms: Public domain