Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  a12study3 Unicode version

Theorem a12study3 29757
Description: Rederivation of axiom ax12o 1887 from two other formulas, without using ax12o 1887. See equvini 1940 and equveli 1941 for the proofs of the hypotheses (using ax12o 1887). Although the second hypothesis (when expanded to primitives) is longer than ax12o 1887, an open problem is whether it can be derived without ax12o 1887 or from a simpler axiom.

Note also that the proof depends on ax11o 1947, whose proof ax11o 1947 depends on ax12o 1887, meaning that we would have to replace ax-11 1727 with ax11o 1947 in an axiomatization that uses the hypotheses in place of ax12o 1887. Whether this can be avoided is an open problem. (Contributed by NM, 1-Mar-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
Ref Expression
a12study3.1  |-  ( x  =  y  ->  E. z
( x  =  z  /\  z  =  y ) )
a12study3.2  |-  ( A. z ( z  =  x  <->  z  =  y )  ->  x  =  y )
Assertion
Ref Expression
a12study3  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  =  y  ->  A. z  x  =  y )
) )

Proof of Theorem a12study3
StepHypRef Expression
1 a12study3.1 . . . . 5  |-  ( x  =  y  ->  E. z
( x  =  z  /\  z  =  y ) )
2 hbn1 1716 . . . . . . 7  |-  ( -. 
A. z  z  =  x  ->  A. z  -.  A. z  z  =  x )
3 hba1 1731 . . . . . . 7  |-  ( A. z ( z  =  x  ->  z  =  y )  ->  A. z A. z ( z  =  x  ->  z  =  y ) )
4 equcomi 1664 . . . . . . . . 9  |-  ( x  =  z  ->  z  =  x )
5 ax11o 1947 . . . . . . . . 9  |-  ( -. 
A. z  z  =  x  ->  ( z  =  x  ->  ( z  =  y  ->  A. z
( z  =  x  ->  z  =  y ) ) ) )
64, 5syl5 28 . . . . . . . 8  |-  ( -. 
A. z  z  =  x  ->  ( x  =  z  ->  ( z  =  y  ->  A. z
( z  =  x  ->  z  =  y ) ) ) )
76imp3a 420 . . . . . . 7  |-  ( -. 
A. z  z  =  x  ->  ( (
x  =  z  /\  z  =  y )  ->  A. z ( z  =  x  ->  z  =  y ) ) )
82, 3, 7exlimdh 1816 . . . . . 6  |-  ( -. 
A. z  z  =  x  ->  ( E. z ( x  =  z  /\  z  =  y )  ->  A. z
( z  =  x  ->  z  =  y ) ) )
9 hbn1 1716 . . . . . . 7  |-  ( -. 
A. z  z  =  y  ->  A. z  -.  A. z  z  =  y )
10 hba1 1731 . . . . . . 7  |-  ( A. z ( z  =  y  ->  z  =  x )  ->  A. z A. z ( z  =  y  ->  z  =  x ) )
11 ax11o 1947 . . . . . . . . . 10  |-  ( -. 
A. z  z  =  y  ->  ( z  =  y  ->  ( z  =  x  ->  A. z
( z  =  y  ->  z  =  x ) ) ) )
124, 11syl7 63 . . . . . . . . 9  |-  ( -. 
A. z  z  =  y  ->  ( z  =  y  ->  ( x  =  z  ->  A. z
( z  =  y  ->  z  =  x ) ) ) )
1312imp3a 420 . . . . . . . 8  |-  ( -. 
A. z  z  =  y  ->  ( (
z  =  y  /\  x  =  z )  ->  A. z ( z  =  y  ->  z  =  x ) ) )
1413ancomsd 440 . . . . . . 7  |-  ( -. 
A. z  z  =  y  ->  ( (
x  =  z  /\  z  =  y )  ->  A. z ( z  =  y  ->  z  =  x ) ) )
159, 10, 14exlimdh 1816 . . . . . 6  |-  ( -. 
A. z  z  =  y  ->  ( E. z ( x  =  z  /\  z  =  y )  ->  A. z
( z  =  y  ->  z  =  x ) ) )
168, 15anim12ii 553 . . . . 5  |-  ( ( -.  A. z  z  =  x  /\  -.  A. z  z  =  y )  ->  ( E. z ( x  =  z  /\  z  =  y )  ->  ( A. z ( z  =  x  ->  z  =  y )  /\  A. z ( z  =  y  ->  z  =  x ) ) ) )
171, 16syl5 28 . . . 4  |-  ( ( -.  A. z  z  =  x  /\  -.  A. z  z  =  y )  ->  ( x  =  y  ->  ( A. z ( z  =  x  ->  z  =  y )  /\  A. z ( z  =  y  ->  z  =  x ) ) ) )
18 albiim 1601 . . . 4  |-  ( A. z ( z  =  x  <->  z  =  y )  <->  ( A. z
( z  =  x  ->  z  =  y )  /\  A. z
( z  =  y  ->  z  =  x ) ) )
1917, 18syl6ibr 218 . . 3  |-  ( ( -.  A. z  z  =  x  /\  -.  A. z  z  =  y )  ->  ( x  =  y  ->  A. z
( z  =  x  <-> 
z  =  y ) ) )
20 a12study3.2 . . . 4  |-  ( A. z ( z  =  x  <->  z  =  y )  ->  x  =  y )
2120a5i 1770 . . 3  |-  ( A. z ( z  =  x  <->  z  =  y )  ->  A. z  x  =  y )
2219, 21syl6 29 . 2  |-  ( ( -.  A. z  z  =  x  /\  -.  A. z  z  =  y )  ->  ( x  =  y  ->  A. z  x  =  y )
)
2322ex 423 1  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  =  y  ->  A. z  x  =  y )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530   E.wex 1531
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator