HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem axacnd 6116
Description: A version of the Axiom of Choice with no distinct variable conditions.
Assertion
Ref Expression
axacnd |- E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w))
Proof of Theorem axacnd
StepHypRef Expression
1 axacndlem5 6115 . . . 4 |- E.xA.yA.v(A.x(y e. v /\ v e. w) -> E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w))
2 hbnae 1507 . . . . . 6 |- (-. A.z z = x -> A.x -. A.z z = x)
3 hbnae 1507 . . . . . . 7 |- (-. A.z z = y -> A.x -. A.z z = y)
4 hbnae 1507 . . . . . . 7 |- (-. A.z z = w -> A.x -. A.z z = w)
53, 4hban 1356 . . . . . 6 |- ((-. A.z z = y /\ -. A.z z = w) -> A.x(-. A.z z = y /\ -. A.z z = w))
62, 5hban 1356 . . . . 5 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> A.x(-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)))
7 hbnae 1507 . . . . . . 7 |- (-. A.z z = x -> A.y -. A.z z = x)
8 hbnae 1507 . . . . . . . 8 |- (-. A.z z = y -> A.y -. A.z z = y)
9 hbnae 1507 . . . . . . . 8 |- (-. A.z z = w -> A.y -. A.z z = w)
108, 9hban 1356 . . . . . . 7 |- ((-. A.z z = y /\ -. A.z z = w) -> A.y(-. A.z z = y /\ -. A.z z = w))
117, 10hban 1356 . . . . . 6 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> A.y(-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)))
12 hbnae 1507 . . . . . . . 8 |- (-. A.z z = x -> A.z -. A.z z = x)
13 hbnae 1507 . . . . . . . . 9 |- (-. A.z z = y -> A.z -. A.z z = y)
14 hbnae 1507 . . . . . . . . 9 |- (-. A.z z = w -> A.z -. A.z z = w)
1513, 14hban 1356 . . . . . . . 8 |- ((-. A.z z = y /\ -. A.z z = w) -> A.z(-. A.z z = y /\ -. A.z z = w))
1612, 15hban 1356 . . . . . . 7 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> A.z(-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)))
17 dveel1 1747 . . . . . . . . . . 11 |- (-. A.z z = y -> (y e. v -> A.z y e. v))
1817ad2antrl 442 . . . . . . . . . 10 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (y e. v -> A.z y e. v))
19 dveel2 1748 . . . . . . . . . . 11 |- (-. A.z z = w -> (v e. w -> A.z v e. w))
2019ad2antll 443 . . . . . . . . . 10 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (v e. w -> A.z v e. w))
2118, 20hband 1469 . . . . . . . . 9 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> ((y e. v /\ v e. w) -> A.z(y e. v /\ v e. w)))
226, 21hbald 1471 . . . . . . . 8 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (A.x(y e. v /\ v e. w) -> A.zA.x(y e. v /\ v e. w)))
23 hbnae 1507 . . . . . . . . . 10 |- (-. A.z z = x -> A.w -. A.z z = x)
24 hbnae 1507 . . . . . . . . . . 11 |- (-. A.z z = y -> A.w -. A.z z = y)
25 hbnae 1507 . . . . . . . . . . 11 |- (-. A.z z = w -> A.w -. A.z z = w)
2624, 25hban 1356 . . . . . . . . . 10 |- ((-. A.z z = y /\ -. A.z z = w) -> A.w(-. A.z z = y /\ -. A.z z = w))
2723, 26hban 1356 . . . . . . . . 9 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> A.w(-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)))
28 ax-15 1751 . . . . . . . . . . . . . . . 16 |- (-. A.z z = y -> (-. A.z z = w -> (y e. w -> A.z y e. w)))
2928imp 377 . . . . . . . . . . . . . . 15 |- ((-. A.z z = y /\ -. A.z z = w) -> (y e. w -> A.z y e. w))
3029adantl 424 . . . . . . . . . . . . . 14 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (y e. w -> A.z y e. w))
31 ax-15 1751 . . . . . . . . . . . . . . . 16 |- (-. A.z z = w -> (-. A.z z = x -> (w e. x -> A.z w e. x)))
3231impcom 378 . . . . . . . . . . . . . . 15 |- ((-. A.z z = x /\ -. A.z z = w) -> (w e. x -> A.z w e. x))
3332adantrl 430 . . . . . . . . . . . . . 14 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (w e. x -> A.z w e. x))
3430, 33hband 1469 . . . . . . . . . . . . 13 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> ((y e. w /\ w e. x) -> A.z(y e. w /\ w e. x)))
3521, 34hband 1469 . . . . . . . . . . . 12 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) -> A.z((y e. v /\ v e. w) /\ (y e. w /\ w e. x))))
3627, 35hbexd 1472 . . . . . . . . . . 11 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) -> A.zE.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x))))
37 ax-12 1310 . . . . . . . . . . . . 13 |- (-. A.z z = y -> (-. A.z z = w -> (y = w -> A.z y = w)))
3837imp 377 . . . . . . . . . . . 12 |- ((-. A.z z = y /\ -. A.z z = w) -> (y = w -> A.z y = w))
3938adantl 424 . . . . . . . . . . 11 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (y = w -> A.z y = w))
4016, 36, 39hbbid 1470 . . . . . . . . . 10 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> ((E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w) -> A.z(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
4111, 40hbald 1471 . . . . . . . . 9 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (A.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w) -> A.zA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
4227, 41hbexd 1472 . . . . . . . 8 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w) -> A.zE.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
4316, 22, 42hbimd 1468 . . . . . . 7 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> ((A.x(y e. v /\ v e. w) -> E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w)) -> A.z(A.x(y e. v /\ v e. w) -> E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w))))
44 nd5 6094 . . . . . . . . . . . 12 |- (-. A.z z = x -> (v = z -> A.x v = z))
4544imdistani 491 . . . . . . . . . . 11 |- ((-. A.z z = x /\ v = z) -> (-. A.z z = x /\ A.x v = z))
46 hba1 1350 . . . . . . . . . . . . 13 |- (A.x v = z -> A.xA.x v = z)
47 elequ2 1497 . . . . . . . . . . . . . . 15 |- (v = z -> (y e. v <-> y e. z))
48 elequ1 1496 . . . . . . . . . . . . . . 15 |- (v = z -> (v e. w <-> z e. w))
4947, 48anbi12d 690 . . . . . . . . . . . . . 14 |- (v = z -> ((y e. v /\ v e. w) <-> (y e. z /\ z e. w)))
5049a4s 1330 . . . . . . . . . . . . 13 |- (A.x v = z -> ((y e. v /\ v e. w) <-> (y e. z /\ z e. w)))
5146, 50albid 1459 . . . . . . . . . . . 12 |- (A.x v = z -> (A.x(y e. v /\ v e. w) <-> A.x(y e. z /\ z e. w)))
5251adantl 424 . . . . . . . . . . 11 |- ((-. A.z z = x /\ A.x v = z) -> (A.x(y e. v /\ v e. w) <-> A.x(y e. z /\ z e. w)))
5345, 52syl 12 . . . . . . . . . 10 |- ((-. A.z z = x /\ v = z) -> (A.x(y e. v /\ v e. w) <-> A.x(y e. z /\ z e. w)))
5453adantlr 429 . . . . . . . . 9 |- (((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) /\ v = z) -> (A.x(y e. v /\ v e. w) <-> A.x(y e. z /\ z e. w)))
55 nd5 6094 . . . . . . . . . . . . 13 |- (-. A.z z = y -> (v = z -> A.y v = z))
56 nd5 6094 . . . . . . . . . . . . . 14 |- (-. A.z z = w -> (v = z -> A.w v = z))
579, 56hbald 1471 . . . . . . . . . . . . 13 |- (-. A.z z = w -> (A.y v = z -> A.wA.y v = z))
5855, 57sylan9 517 . . . . . . . . . . . 12 |- ((-. A.z z = y /\ -. A.z z = w) -> (v = z -> A.wA.y v = z))
5958imdistani 491 . . . . . . . . . . 11 |- (((-. A.z z = y /\ -. A.z z = w) /\ v = z) -> ((-. A.z z = y /\ -. A.z z = w) /\ A.wA.y v = z))
60 hba1 1350 . . . . . . . . . . . . 13 |- (A.wA.y v = z -> A.wA.wA.y v = z)
61 hba2 1360 . . . . . . . . . . . . . 14 |- (A.wA.y v = z -> A.yA.wA.y v = z)
6249a4s 1330 . . . . . . . . . . . . . . . . . 18 |- (A.y v = z -> ((y e. v /\ v e. w) <-> (y e. z /\ z e. w)))
6362a4s 1330 . . . . . . . . . . . . . . . . 17 |- (A.wA.y v = z -> ((y e. v /\ v e. w) <-> (y e. z /\ z e. w)))
6463anbi1d 679 . . . . . . . . . . . . . . . 16 |- (A.wA.y v = z -> (((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> ((y e. z /\ z e. w) /\ (y e. w /\ w e. x))))
6560, 64exbid 1460 . . . . . . . . . . . . . . 15 |- (A.wA.y v = z -> (E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x))))
6665bibi1d 681 . . . . . . . . . . . . . 14 |- (A.wA.y v = z -> ((E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w) <-> (E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
6761, 66albid 1459 . . . . . . . . . . . . 13 |- (A.wA.y v = z -> (A.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w) <-> A.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
6860, 67exbid 1460 . . . . . . . . . . . 12 |- (A.wA.y v = z -> (E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w) <-> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
6968adantl 424 . . . . . . . . . . 11 |- (((-. A.z z = y /\ -. A.z z = w) /\ A.wA.y v = z) -> (E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w) <-> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
7059, 69syl 12 . . . . . . . . . 10 |- (((-. A.z z = y /\ -. A.z z = w) /\ v = z) -> (E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w) <-> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
7170adantll 428 . . . . . . . . 9 |- (((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) /\ v = z) -> (E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w) <-> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
7254, 71imbi12d 688 . . . . . . . 8 |- (((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) /\ v = z) -> ((A.x(y e. v /\ v e. w) -> E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w)) <-> (A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w))))
7372ex 402 . . . . . . 7 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (v = z -> ((A.x(y e. v /\ v e. w) -> E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w)) <-> (A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))))
7416, 43, 73cbvald 1702 . . . . . 6 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (A.v(A.x(y e. v /\ v e. w) -> E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w)) <-> A.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w))))
7511, 74albid 1459 . . . . 5 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (A.yA.v(A.x(y e. v /\ v e. w) -> E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w)) <-> A.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w))))
766, 75exbid 1460 . . . 4 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> (E.xA.yA.v(A.x(y e. v /\ v e. w) -> E.wA.y(E.w((y e. v /\ v e. w) /\ (y e. w /\ w e. x)) <-> y = w)) <-> E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w))))
771, 76mpbii 210 . . 3 |- ((-. A.z z = x /\ (-. A.z z = y /\ -. A.z z = w)) -> E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
7877exp32 408 . 2 |- (-. A.z z = x -> (-. A.z z = y -> (-. A.z z = w -> E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))))
79 axacndlem2 6112 . . 3 |- (A.x x = z -> E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
8079alequcoms 1503 . 2 |- (A.z z = x -> E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
81 axacndlem3 6113 . . 3 |- (A.y y = z -> E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
8281alequcoms 1503 . 2 |- (A.z z = y -> E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
83 hbae 1505 . . . 4 |- (A.z z = w -> A.yA.z z = w)
84 nd3 6092 . . . . . . 7 |- (A.z z = w -> -. A.x z e. w)
8584pm2.21d 94 . . . . . 6 |- (A.z z = w -> (A.x z e. w -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
86 simpr 350 . . . . . . 7 |- ((y e. z /\ z e. w) -> z e. w)
8786alimi 1338 . . . . . 6 |- (A.x(y e. z /\ z e. w) -> A.x z e. w)
8885, 87syl5 20 . . . . 5 |- (A.z z = w -> (A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
8988a5i 1335 . . . 4 |- (A.z z = w -> A.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
9083, 8919.21ai 1345 . . 3 |- (A.z z = w -> A.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
91 19.8a 1376 . . 3 |- (A.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)) -> E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
9290, 91syl 12 . 2 |- (A.z z = w -> E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w)))
9378, 80, 82, 92pm2.61iii 147 1 |- E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326
This theorem is referenced by:  zfcndac 6123  axacprim 13791
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-15 1751  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-reg 5695  ax-ac 5906
This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-eprel 3583  df-fr 3625
Copyright terms: Public domain