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

Theorem a12study 1769
Description: Rederivation of axiom ax-12 1310 from two shorter formulas, without using ax-12 1310. See a12lem1 1767 and a12lem2 1768 for the proofs of the hypotheses (using ax-12 1310). This is the only known breakdown of ax-12 1310 into shorter formulas. See a12studyALT 1770 for an alternate proof. Note that the proof depends on ax-11o 1588, whose proof ax11o 1587 depends on ax-12 1310, meaning that we would have to replace ax-11 1309 with ax-11o 1588 in an axiomatization that uses the hypotheses in place of ax-12 1310. Whether this can be avoided is an open problem.
Hypotheses
Ref Expression
a12study.1 |- (-. A.z z = y -> (A.z(z = x -> z = y) -> x = y))
a12study.2 |- (A.z(z = x -> -. z = y) -> -. x = y)
Assertion
Ref Expression
a12study |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))

Proof of Theorem a12study
StepHypRef Expression
1 hbn1 1362 . . . . 5 |- (-. A.z z = x -> A.z -. A.z z = x)
2 hbn1 1362 . . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
31, 2hban 1356 . . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> A.z(-. A.z z = x /\ -. A.z z = y))
4 hba1 1350 . . . 4 |- (A.z x = y -> A.zA.z x = y)
5 ax-11o 1588 . . . . . . 7 |- (-. A.z z = x -> (z = x -> (z = y -> A.z(z = x -> z = y))))
6 equid1 1646 . . . . . . . 8 |- x = x
7 ax-8 1306 . . . . . . . 8 |- (x = z -> (x = x -> z = x))
86, 7mpi 55 . . . . . . 7 |- (x = z -> z = x)
95, 8syl5 20 . . . . . 6 |- (-. A.z z = x -> (x = z -> (z = y -> A.z(z = x -> z = y))))
109imp3a 388 . . . . 5 |- (-. A.z z = x -> ((x = z /\ z = y) -> A.z(z = x -> z = y)))
11 hba1 1350 . . . . . 6 |- (A.z(z = x -> z = y) -> A.zA.z(z = x -> z = y))
12 a12study.1 . . . . . 6 |- (-. A.z z = y -> (A.z(z = x -> z = y) -> x = y))
132, 11, 1219.21ad 1406 . . . . 5 |- (-. A.z z = y -> (A.z(z = x -> z = y) -> A.z x = y))
1410, 13sylan9 517 . . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> ((x = z /\ z = y) -> A.z x = y))
153, 4, 1419.23ad 1415 . . 3 |- ((-. A.z z = x /\ -. A.z z = y) -> (E.z(x = z /\ z = y) -> A.z x = y))
1615ex 402 . 2 |- (-. A.z z = x -> (-. A.z z = y -> (E.z(x = z /\ z = y) -> A.z x = y)))
17 imnan 261 . . . . . . 7 |- ((x = z -> -. z = y) <-> -. (x = z /\ z = y))
18 equid1 1646 . . . . . . . . 9 |- z = z
19 ax-8 1306 . . . . . . . . 9 |- (z = x -> (z = z -> x = z))
2018, 19mpi 55 . . . . . . . 8 |- (z = x -> x = z)
2120imim1i 19 . . . . . . 7 |- ((x = z -> -. z = y) -> (z = x -> -. z = y))
2217, 21sylbir 218 . . . . . 6 |- (-. (x = z /\ z = y) -> (z = x -> -. z = y))
2322alimi 1338 . . . . 5 |- (A.z -. (x = z /\ z = y) -> A.z(z = x -> -. z = y))
24 a12study.2 . . . . 5 |- (A.z(z = x -> -. z = y) -> -. x = y)
2523, 24syl 12 . . . 4 |- (A.z -. (x = z /\ z = y) -> -. x = y)
2625con2i 113 . . 3 |- (x = y -> -. A.z -. (x = z /\ z = y))
27 df-ex 1327 . . 3 |- (E.z(x = z /\ z = y) <-> -. A.z -. (x = z /\ z = y))
2826, 27sylibr 217 . 2 |- (x = y -> E.z(x = z /\ z = y))
2916, 28syl7 26 1 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298  E.wex 1326
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-8 1306  ax-9 1307  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-11o 1588
This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327
Copyright terms: Public domain