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

Theorem ax9vax9 28288
Description: Derive ax-9 1684 (which has no distinct variable requirement) from a weaker version that requires that its two variables be distinct. The weaker version is axiom scheme B7 of [Tarski] p. 75. The hypotheses are the instances of the weaker version that we need. Neither ax-9 1684 nor ax-4 1692 (which can be derived from ax-9 1684) is used by the proof.

Revised on 7-Aug-2015 to remove the dependence on ax-10 1678.

See also the remarks for ax-9v 1632 and ax9 1683. This theorem does not actually use ax-9v 1632 so that other paths to ax-9 1684 can be demonstrated (such as in ax9sep 28290). Theorem ax9 1683 uses this one to make the derivation from ax-9v 1632. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 7-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
Ref Expression
ax9vax9.a  |-  -.  A. t  -.  t  =  u
ax9vax9.b  |-  -.  A. t  -.  t  =  z
ax9vax9.e  |-  -.  A. u  -.  u  =  x
ax9vax9.f  |-  -.  A. u  -.  u  =  w
ax9vax9.i  |-  -.  A. z  -.  z  =  x
ax9vax9.j  |-  -.  A. z  -.  z  =  w
ax9vax9.k  |-  -.  A. x  -.  x  =  t
ax9vax9.m  |-  -.  A. x  -.  x  =  z
ax9vax9.p  |-  -.  A. w  -.  w  =  t
ax9vax9.r  |-  -.  A. w  -.  w  =  z
ax9vax9.t  |-  -.  A. w  -.  w  =  y
ax9vax9.y  |-  -.  A. x  -.  x  =  v
ax9vax9.z  |-  -.  A. v  -.  v  =  y
Assertion
Ref Expression
ax9vax9  |-  -.  A. x  -.  x  =  y
Distinct variable groups:    u, t, w, x, v, z    y, u, w, v, z

Proof of Theorem ax9vax9
StepHypRef Expression
1 ax9vax9.i . . . 4  |-  -.  A. z  -.  z  =  x
2 ax9vax9.m . . . 4  |-  -.  A. x  -.  x  =  z
31, 2ax9lem3 28272 . . 3  |-  ( A. x  -.  x  =  y  ->  -.  x  =  y )
41, 2ax9lem3 28272 . . 3  |-  ( A. x  x  =  y  ->  x  =  y )
53, 4nsyl3 113 . 2  |-  ( A. x  x  =  y  ->  -.  A. x  -.  x  =  y )
6 ax9vax9.z . . 3  |-  -.  A. v  -.  v  =  y
7 ax-17 1628 . . . 4  |-  ( -.  ( -.  A. x  x  =  y  ->  -. 
A. x  -.  x  =  y )  ->  A. v  -.  ( -.  A. x  x  =  y  ->  -.  A. x  -.  x  =  y
) )
8 ax9vax9.a . . . . . . 7  |-  -.  A. t  -.  t  =  u
9 ax9vax9.b . . . . . . 7  |-  -.  A. t  -.  t  =  z
10 ax9vax9.e . . . . . . 7  |-  -.  A. u  -.  u  =  x
11 ax9vax9.f . . . . . . 7  |-  -.  A. u  -.  u  =  w
12 ax9vax9.j . . . . . . 7  |-  -.  A. z  -.  z  =  w
13 ax9vax9.k . . . . . . 7  |-  -.  A. x  -.  x  =  t
14 ax9vax9.p . . . . . . 7  |-  -.  A. w  -.  w  =  t
15 ax9vax9.r . . . . . . 7  |-  -.  A. w  -.  w  =  z
16 ax9vax9.t . . . . . . 7  |-  -.  A. w  -.  w  =  y
17 ax9vax9.y . . . . . . . 8  |-  -.  A. x  -.  x  =  v
1815, 12, 1, 17ax9lem6 28275 . . . . . . 7  |-  -.  A. z  -.  z  =  v
198, 9, 10, 11, 1, 12, 13, 2, 14, 15, 16, 18ax9lem18 28287 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  ( v  =  y  ->  A. x  v  =  y )
)
201, 2ax9lem7 28276 . . . . . . . . 9  |-  ( A. x  v  =  y  ->  A. x A. x  v  =  y )
211, 2ax9lem3 28272 . . . . . . . . . 10  |-  ( A. x  v  =  y  ->  v  =  y )
221ax9lem1 28270 . . . . . . . . . . . . 13  |-  ( x  =  v  ->  v  =  x )
23 ax-8 1623 . . . . . . . . . . . . 13  |-  ( v  =  x  ->  (
v  =  y  ->  x  =  y )
)
2422, 23syl 17 . . . . . . . . . . . 12  |-  ( x  =  v  ->  (
v  =  y  ->  x  =  y )
)
2524com12 29 . . . . . . . . . . 11  |-  ( v  =  y  ->  (
x  =  v  ->  x  =  y )
)
2625con3d 127 . . . . . . . . . 10  |-  ( v  =  y  ->  ( -.  x  =  y  ->  -.  x  =  v ) )
2721, 26syl 17 . . . . . . . . 9  |-  ( A. x  v  =  y  ->  ( -.  x  =  y  ->  -.  x  =  v ) )
2820, 27alimdh 1551 . . . . . . . 8  |-  ( A. x  v  =  y  ->  ( A. x  -.  x  =  y  ->  A. x  -.  x  =  v ) )
2928con3d 127 . . . . . . 7  |-  ( A. x  v  =  y  ->  ( -.  A. x  -.  x  =  v  ->  -.  A. x  -.  x  =  y )
)
3017, 29mpi 18 . . . . . 6  |-  ( A. x  v  =  y  ->  -.  A. x  -.  x  =  y )
3119, 30syl6com 33 . . . . 5  |-  ( v  =  y  ->  ( -.  A. x  x  =  y  ->  -.  A. x  -.  x  =  y
) )
3231con3i 129 . . . 4  |-  ( -.  ( -.  A. x  x  =  y  ->  -. 
A. x  -.  x  =  y )  ->  -.  v  =  y
)
337, 32alrimih 1553 . . 3  |-  ( -.  ( -.  A. x  x  =  y  ->  -. 
A. x  -.  x  =  y )  ->  A. v  -.  v  =  y )
346, 33mt3 173 . 2  |-  ( -. 
A. x  x  =  y  ->  -.  A. x  -.  x  =  y
)
355, 34pm2.61i 158 1  |-  -.  A. x  -.  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   A.wal 1532
This theorem is referenced by:  ax9OLD  28289  ax9sep  28290
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538
  Copyright terms: Public domain W3C validator