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

Theorem a12study 29132
Description: Rederivation of axiom ax12o 1875 from two shorter formulas, without using ax12o 1875. See a12lem1 29130 and a12lem2 29131 for the proofs of the hypotheses (using ax12o 1875). This is the only known breakdown of ax12o 1875 into shorter formulas. See a12studyALT 29133 for an alternate proof. Note 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, 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 1646 . . . . . . . 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 1546 . . . . 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 1529 . . 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 1756 . . . . . 6  |-  F/ z A. z  z  =  x
1211nfn 1765 . . . . 5  |-  F/ z  -.  A. z  z  =  x
13 nfa1 1756 . . . . . 6  |-  F/ z A. z  z  =  y
1413nfn 1765 . . . . 5  |-  F/ z  -.  A. z  z  =  y
1512, 14nfan 1771 . . . 4  |-  F/ z ( -.  A. z 
z  =  x  /\  -.  A. z  z  =  y )
16 nfa1 1756 . . . 4  |-  F/ z A. z  x  =  y
17 equcomi 1646 . . . . . . 7  |-  ( x  =  z  ->  z  =  x )
18 ax11o 1934 . . . . . . 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 1756 . . . . . 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 1749 . . . . 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 1803 . . 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 1527   E.wex 1528    = wceq 1623
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-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator