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

Theorem a12study 29754
Description: Rederivation of axiom ax12o 1887 from two shorter formulas, without using ax12o 1887. See a12lem1 29752 and a12lem2 29753 for the proofs of the hypotheses (using ax12o 1887). This is the only known breakdown of ax12o 1887 into shorter formulas. See a12studyALT 29755 for an alternate proof. Note 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, 15-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
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 imnan 411 . . . . . . 7  |-  ( ( x  =  z  ->  -.  z  =  y
)  <->  -.  ( x  =  z  /\  z  =  y ) )
2 equcomi 1664 . . . . . . . 8  |-  ( z  =  x  ->  x  =  z )
32imim1i 54 . . . . . . 7  |-  ( ( x  =  z  ->  -.  z  =  y
)  ->  ( z  =  x  ->  -.  z  =  y ) )
41, 3sylbir 204 . . . . . 6  |-  ( -.  ( x  =  z  /\  z  =  y )  ->  ( z  =  x  ->  -.  z  =  y ) )
54alimi 1549 . . . . 5  |-  ( A. z  -.  ( x  =  z  /\  z  =  y )  ->  A. z
( z  =  x  ->  -.  z  =  y ) )
6 a12study.2 . . . . 5  |-  ( A. z ( z  =  x  ->  -.  z  =  y )  ->  -.  x  =  y
)
75, 6syl 15 . . . 4  |-  ( A. z  -.  ( x  =  z  /\  z  =  y )  ->  -.  x  =  y )
87con2i 112 . . 3  |-  ( x  =  y  ->  -.  A. z  -.  ( x  =  z  /\  z  =  y ) )
9 df-ex 1532 . . 3  |-  ( E. z ( x  =  z  /\  z  =  y )  <->  -.  A. z  -.  ( x  =  z  /\  z  =  y ) )
108, 9sylibr 203 . 2  |-  ( x  =  y  ->  E. z
( x  =  z  /\  z  =  y ) )
11 nfa1 1768 . . . . . 6  |-  F/ z A. z  z  =  x
1211nfn 1777 . . . . 5  |-  F/ z  -.  A. z  z  =  x
13 nfa1 1768 . . . . . 6  |-  F/ z A. z  z  =  y
1413nfn 1777 . . . . 5  |-  F/ z  -.  A. z  z  =  y
1512, 14nfan 1783 . . . 4  |-  F/ z ( -.  A. z 
z  =  x  /\  -.  A. z  z  =  y )
16 nfa1 1768 . . . 4  |-  F/ z A. z  x  =  y
17 equcomi 1664 . . . . . . 7  |-  ( x  =  z  ->  z  =  x )
18 ax11o 1947 . . . . . . 7  |-  ( -. 
A. z  z  =  x  ->  ( z  =  x  ->  ( z  =  y  ->  A. z
( z  =  x  ->  z  =  y ) ) ) )
1917, 18syl5 28 . . . . . 6  |-  ( -. 
A. z  z  =  x  ->  ( x  =  z  ->  ( z  =  y  ->  A. z
( z  =  x  ->  z  =  y ) ) ) )
2019imp3a 420 . . . . 5  |-  ( -. 
A. z  z  =  x  ->  ( (
x  =  z  /\  z  =  y )  ->  A. z ( z  =  x  ->  z  =  y ) ) )
21 nfa1 1768 . . . . . 6  |-  F/ z A. z ( z  =  x  ->  z  =  y )
22 a12study.1 . . . . . 6  |-  ( -. 
A. z  z  =  y  ->  ( A. z ( z  =  x  ->  z  =  y )  ->  x  =  y ) )
2314, 21, 22alrimd 1761 . . . . 5  |-  ( -. 
A. z  z  =  y  ->  ( A. z ( z  =  x  ->  z  =  y )  ->  A. z  x  =  y )
)
2420, 23sylan9 638 . . . 4  |-  ( ( -.  A. z  z  =  x  /\  -.  A. z  z  =  y )  ->  ( (
x  =  z  /\  z  =  y )  ->  A. z  x  =  y ) )
2515, 16, 24exlimd 1815 . . 3  |-  ( ( -.  A. z  z  =  x  /\  -.  A. z  z  =  y )  ->  ( E. z ( x  =  z  /\  z  =  y )  ->  A. z  x  =  y )
)
2625ex 423 . 2  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( E. z
( x  =  z  /\  z  =  y )  ->  A. z  x  =  y )
) )
2710, 26syl7 63 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    /\ wa 358   A.wal 1530   E.wex 1531    = wceq 1632
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-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator