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

Theorem a12study4 29739
Description: Experiment to study ax12o 1887. The first hypothesis is a conjectured ax12o 1887 replacement (see ax12 1888 for its derivation from ax12o 1887). The second hypothesis needs to be proved without using ax12o 1887, 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 1669 . . . . . . . . 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 1606 . . . . . . . . 9  |-  ( z  =  y  ->  A. x  z  =  y )
5 ax-11 1727 . . . . . . . . 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 1667 . . . . . . . . 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 1549 . . . . . 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 1556 . . . . 5  |-  ( A. z  y  =  x  <->  A. z ( ( z  =  x  ->  y  =  x )  /\  ( -.  z  =  x  ->  y  =  x ) ) )
22 19.26 1583 . . . . 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 1530
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-11 1727
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator