MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax4 Unicode version

Theorem ax4 1691
Description: Theorem showing that ax-4 1692 can be derived from ax-5 1533, ax-gen 1536, ax-8 1623, ax-9 1684, ax-11 1624, and ax-17 1628 and is therefore redundant in a system including these axioms. The proof uses ideas from the proof of Lemma 21 of [Monk2] p. 114.

This theorem should not be referenced in any proof. Instead, we will use ax-4 1692 below so that explicit uses of ax-4 1692 can be more easily identified. In particular, this will more cleanly separate out the theorems of "pure" predicate calculus that don't involve equality or distinct variables. A beginner may wish to accept ax-4 1692 a priori, so that the proof of this theorem (ax4 1691), which involves equality as well as the distinct variable requirements of ax-17 1628, can be put off until those axioms are studied.

Note: All predicate calculus axioms introduced from this point forward are redundant. Immediately before their introduction, we prove them from earlier axioms to demonstrate their redundancy. Specifically, redundant axioms ax-4 1692, ax-5o 1694, ax-6o 1697, ax-9o 1815, ax-10o 1835, ax-11o 1940, ax-15 2102, and ax-16 1926 are proved by theorems ax4 1691, ax5o 1693, ax6o 1696, ax9o 1814, ax10o 1834, ax11o 1939, ax15 2101, and ax16 1925. Except for the ones suffixed with o (ax-5o 1694 etc.), we never reference those theorems directly. Instead, we use the axiom version that immediately follows it. This allow us to better isolate the uses of the redundant axioms for easier study of subsystems containing them.

Axioms ax-12o 1664, ax-10 1678, and ax-9 1684 should be referenced directly rather than theorems ax12o 1663, ax10 1677, and ax9 1683 that prove them from others. This will avoid the general use of ax-9v 1632, which is not an official axiom for us. (Contributed by NM, 21-May-2008.) (Proof shortened by Scott Fenton, 24-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion
Ref Expression
ax4  |-  ( A. x ph  ->  ph )

Proof of Theorem ax4
StepHypRef Expression
1 ax-9 1684 . 2  |-  -.  A. y  -.  y  =  x
2 ax-9 1684 . . . . . . . . . 10  |-  -.  A. x  -.  x  =  y
3 ax-8 1623 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
x  =  y  -> 
y  =  y ) )
43pm2.43i 45 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  y  =  y )
54con3i 129 . . . . . . . . . . . 12  |-  ( -.  y  =  y  ->  -.  x  =  y
)
65ax-gen 1536 . . . . . . . . . . 11  |-  A. x
( -.  y  =  y  ->  -.  x  =  y )
7 ax-17 1628 . . . . . . . . . . 11  |-  ( -.  y  =  y  ->  A. x  -.  y  =  y )
8 ax-5 1533 . . . . . . . . . . 11  |-  ( A. x ( -.  y  =  y  ->  -.  x  =  y )  -> 
( A. x  -.  y  =  y  ->  A. x  -.  x  =  y ) )
96, 7, 8mpsyl 61 . . . . . . . . . 10  |-  ( -.  y  =  y  ->  A. x  -.  x  =  y )
102, 9mt3 173 . . . . . . . . 9  |-  y  =  y
11 ax-8 1623 . . . . . . . . 9  |-  ( y  =  x  ->  (
y  =  y  ->  x  =  y )
)
1210, 11mpi 18 . . . . . . . 8  |-  ( y  =  x  ->  x  =  y )
13 ax-17 1628 . . . . . . . 8  |-  ( -. 
ph  ->  A. y  -.  ph )
14 ax-11 1624 . . . . . . . 8  |-  ( x  =  y  ->  ( A. y  -.  ph  ->  A. x ( x  =  y  ->  -.  ph )
) )
1512, 13, 14syl2im 36 . . . . . . 7  |-  ( y  =  x  ->  ( -.  ph  ->  A. x
( x  =  y  ->  -.  ph ) ) )
16 con2 110 . . . . . . . . . . 11  |-  ( ( x  =  y  ->  -.  ph )  ->  ( ph  ->  -.  x  =  y ) )
1716ax-gen 1536 . . . . . . . . . 10  |-  A. x
( ( x  =  y  ->  -.  ph )  ->  ( ph  ->  -.  x  =  y )
)
18 ax-5 1533 . . . . . . . . . 10  |-  ( A. x ( ( x  =  y  ->  -.  ph )  ->  ( ph  ->  -.  x  =  y ) )  ->  ( A. x ( x  =  y  ->  -.  ph )  ->  A. x ( ph  ->  -.  x  =  y ) ) )
1917, 18ax-mp 10 . . . . . . . . 9  |-  ( A. x ( x  =  y  ->  -.  ph )  ->  A. x ( ph  ->  -.  x  =  y ) )
20 ax-5 1533 . . . . . . . . 9  |-  ( A. x ( ph  ->  -.  x  =  y )  ->  ( A. x ph  ->  A. x  -.  x  =  y ) )
2119, 20syl 17 . . . . . . . 8  |-  ( A. x ( x  =  y  ->  -.  ph )  ->  ( A. x ph  ->  A. x  -.  x  =  y ) )
222, 21mtoi 171 . . . . . . 7  |-  ( A. x ( x  =  y  ->  -.  ph )  ->  -.  A. x ph )
2315, 22syl6 31 . . . . . 6  |-  ( y  =  x  ->  ( -.  ph  ->  -.  A. x ph ) )
2423con4d 99 . . . . 5  |-  ( y  =  x  ->  ( A. x ph  ->  ph )
)
2524con3i 129 . . . 4  |-  ( -.  ( A. x ph  ->  ph )  ->  -.  y  =  x )
2625ax-gen 1536 . . 3  |-  A. y
( -.  ( A. x ph  ->  ph )  ->  -.  y  =  x
)
27 ax-17 1628 . . 3  |-  ( -.  ( A. x ph  ->  ph )  ->  A. y  -.  ( A. x ph  ->  ph ) )
28 ax-5 1533 . . 3  |-  ( A. y ( -.  ( A. x ph  ->  ph )  ->  -.  y  =  x )  ->  ( A. y  -.  ( A. x ph  ->  ph )  ->  A. y  -.  y  =  x
) )
2926, 27, 28mpsyl 61 . 2  |-  ( -.  ( A. x ph  ->  ph )  ->  A. y  -.  y  =  x
)
301, 29mt3 173 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   A.wal 1532
This theorem is referenced by:  fiinopn  16479  relexpindlem  23207  fundmpss  23290  a9e2ndeq  27018  a9e2eqVD  27373  a9e2ndeqVD  27375  a9e2ndeqALT  27398
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-9 1684
  Copyright terms: Public domain W3C validator