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

Theorem a12study4 29117
Description: Experiment to study ax12o 1875. The first hypothesis is a conjectured ax12o 1875 replacement (see ax12 2095 for its derivation from ax12o 1875). The second hypothesis needs to be proved without using ax12o 1875, if that is possible. (Contributed by NM, 7-Nov-1015.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
a12study4.1  |-  ( -.  z  =  y  -> 
( y  =  x  ->  A. z  y  =  x ) )
a12study4.2  |-  ( -. 
A. z  z  =  y  ->  ( (
z  =  y  /\  y  =  x )  ->  A. z ( -.  z  =  x  -> 
y  =  x ) ) )
Assertion
Ref Expression
a12study4  |-  ( -. 
A. z  z  =  y  ->  ( y  =  x  ->  A. z 
y  =  x ) )
Distinct variable groups:    x, y    x, z

Proof of Theorem a12study4
StepHypRef Expression
1 equequ2 1649 . . . . . . . . 9  |-  ( y  =  x  ->  (
z  =  y  <->  z  =  x ) )
21biimpac 472 . . . . . . . 8  |-  ( ( z  =  y  /\  y  =  x )  ->  z  =  x )
3 simpl 443 . . . . . . . 8  |-  ( ( z  =  y  /\  y  =  x )  ->  z  =  y )
4 ax-17 1603 . . . . . . . . 9  |-  ( z  =  y  ->  A. x  z  =  y )
5 ax-11 1715 . . . . . . . . 9  |-  ( z  =  x  ->  ( A. x  z  =  y  ->  A. z ( z  =  x  ->  z  =  y ) ) )
64, 5syl5 28 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =  y  ->  A. z ( z  =  x  ->  z  =  y ) ) )
72, 3, 6sylc 56 . . . . . . 7  |-  ( ( z  =  y  /\  y  =  x )  ->  A. z ( z  =  x  ->  z  =  y ) )
873adant1 973 . . . . . 6  |-  ( ( -.  A. z  z  =  y  /\  z  =  y  /\  y  =  x )  ->  A. z
( z  =  x  ->  z  =  y ) )
9 equequ1 1648 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =  x  <->  y  =  x ) )
109biimpcd 215 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =  y  -> 
y  =  x ) )
1110a2i 12 . . . . . . 7  |-  ( ( z  =  x  -> 
z  =  y )  ->  ( z  =  x  ->  y  =  x ) )
1211alimi 1546 . . . . . 6  |-  ( A. z ( z  =  x  ->  z  =  y )  ->  A. z
( z  =  x  ->  y  =  x ) )
138, 12syl 15 . . . . 5  |-  ( ( -.  A. z  z  =  y  /\  z  =  y  /\  y  =  x )  ->  A. z
( z  =  x  ->  y  =  x ) )
14 a12study4.2 . . . . . 6  |-  ( -. 
A. z  z  =  y  ->  ( (
z  =  y  /\  y  =  x )  ->  A. z ( -.  z  =  x  -> 
y  =  x ) ) )
15143impib 1149 . . . . 5  |-  ( ( -.  A. z  z  =  y  /\  z  =  y  /\  y  =  x )  ->  A. z
( -.  z  =  x  ->  y  =  x ) )
1613, 15jca 518 . . . 4  |-  ( ( -.  A. z  z  =  y  /\  z  =  y  /\  y  =  x )  ->  ( A. z ( z  =  x  ->  y  =  x )  /\  A. z ( -.  z  =  x  ->  y  =  x ) ) )
17 exmid 404 . . . . . . . 8  |-  ( z  =  x  \/  -.  z  =  x )
1817a1bi 327 . . . . . . 7  |-  ( y  =  x  <->  ( (
z  =  x  \/ 
-.  z  =  x )  ->  y  =  x ) )
19 jaob 758 . . . . . . 7  |-  ( ( ( z  =  x  \/  -.  z  =  x )  ->  y  =  x )  <->  ( (
z  =  x  -> 
y  =  x )  /\  ( -.  z  =  x  ->  y  =  x ) ) )
2018, 19bitri 240 . . . . . 6  |-  ( y  =  x  <->  ( (
z  =  x  -> 
y  =  x )  /\  ( -.  z  =  x  ->  y  =  x ) ) )
2120albii 1553 . . . . 5  |-  ( A. z  y  =  x  <->  A. z ( ( z  =  x  ->  y  =  x )  /\  ( -.  z  =  x  ->  y  =  x ) ) )
22 19.26 1580 . . . . 5  |-  ( A. z ( ( z  =  x  ->  y  =  x )  /\  ( -.  z  =  x  ->  y  =  x ) )  <->  ( A. z
( z  =  x  ->  y  =  x )  /\  A. z
( -.  z  =  x  ->  y  =  x ) ) )
2321, 22bitr2i 241 . . . 4  |-  ( ( A. z ( z  =  x  ->  y  =  x )  /\  A. z ( -.  z  =  x  ->  y  =  x ) )  <->  A. z 
y  =  x )
2416, 23sylib 188 . . 3  |-  ( ( -.  A. z  z  =  y  /\  z  =  y  /\  y  =  x )  ->  A. z 
y  =  x )
25243exp 1150 . 2  |-  ( -. 
A. z  z  =  y  ->  ( z  =  y  ->  ( y  =  x  ->  A. z 
y  =  x ) ) )
26 a12study4.1 . 2  |-  ( -.  z  =  y  -> 
( y  =  x  ->  A. z  y  =  x ) )
2725, 26pm2.61d1 151 1  |-  ( -. 
A. z  z  =  y  ->  ( y  =  x  ->  A. z 
y  =  x ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357    /\ wa 358    /\ w3a 934   A.wal 1527
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-11 1715
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator