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

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

Note also that the proof depends on ax11o 1934, whose proof ax11o 1934 depends on ax12o 1875, meaning that we would have to replace ax-11 1715 with ax11o 1934 in an axiomatization that uses the hypotheses in place of ax12o 1875. 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 1704 . . . . . . 7  |-  ( -. 
A. z  z  =  x  ->  A. z  -.  A. z  z  =  x )
3 hba1 1719 . . . . . . 7  |-  ( A. z ( z  =  x  ->  z  =  y )  ->  A. z A. z ( z  =  x  ->  z  =  y ) )
4 equcomi 1646 . . . . . . . . 9  |-  ( x  =  z  ->  z  =  x )
5 ax11o 1934 . . . . . . . . 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 1804 . . . . . 6  |-  ( -. 
A. z  z  =  x  ->  ( E. z ( x  =  z  /\  z  =  y )  ->  A. z
( z  =  x  ->  z  =  y ) ) )
9 hbn1 1704 . . . . . . 7  |-  ( -. 
A. z  z  =  y  ->  A. z  -.  A. z  z  =  y )
10 hba1 1719 . . . . . . 7  |-  ( A. z ( z  =  y  ->  z  =  x )  ->  A. z A. z ( z  =  y  ->  z  =  x ) )
11 ax11o 1934 . . . . . . . . . 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 1804 . . . . . 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 1598 . . . 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 1758 . . 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 1527   E.wex 1528
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator