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

Theorem ax10lem17ALT 29123
Description: Lemma for ax10 1884. Similar to dveeq2 1880, without using sp 1716, ax9 1889, or ax10 1884 but allowing ax9v 1636. Direct proof of dveeq2 1880, bypassing dvelimnf 1957 to investigate possible simplifications. Uses ax12o 1875. (Contributed by NM, 20-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax10lem17ALT  |-  ( -. 
A. x  x  =  y  ->  ( z  =  y  ->  A. x  z  =  y )
)
Distinct variable group:    x, z

Proof of Theorem ax10lem17ALT
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 ax-17 1603 . . . . . 6  |-  ( z  =  y  ->  A. w  z  =  y )
21a1d 22 . . . . . 6  |-  ( z  =  y  ->  (
w  =  y  ->  A. w  z  =  y ) )
31, 2alrimih 1552 . . . . 5  |-  ( z  =  y  ->  A. w
( w  =  y  ->  A. w  z  =  y ) )
4 sp 1716 . . . . . . . 8  |-  ( A. w  z  =  y  ->  z  =  y )
5 equequ2 1649 . . . . . . . 8  |-  ( w  =  y  ->  (
z  =  w  <->  z  =  y ) )
64, 5syl5ibr 212 . . . . . . 7  |-  ( w  =  y  ->  ( A. w  z  =  y  ->  z  =  w ) )
76a2i 12 . . . . . 6  |-  ( ( w  =  y  ->  A. w  z  =  y )  ->  (
w  =  y  -> 
z  =  w ) )
87alimi 1546 . . . . 5  |-  ( A. w ( w  =  y  ->  A. w  z  =  y )  ->  A. w ( w  =  y  ->  z  =  w ) )
93, 8syl 15 . . . 4  |-  ( z  =  y  ->  A. w
( w  =  y  ->  z  =  w ) )
10 ax10lem3 1878 . . . . . . . 8  |-  ( A. w  w  =  x  ->  A. x  x  =  w )
1110con3i 127 . . . . . . 7  |-  ( -. 
A. x  x  =  w  ->  -.  A. w  w  =  x )
12 hbn1 1704 . . . . . . . 8  |-  ( -. 
A. w  w  =  x  ->  A. w  -.  A. w  w  =  x )
13 ax10lem3 1878 . . . . . . . . 9  |-  ( A. x  x  =  w  ->  A. w  w  =  x )
1413con3i 127 . . . . . . . 8  |-  ( -. 
A. w  w  =  x  ->  -.  A. x  x  =  w )
1512, 14alrimih 1552 . . . . . . 7  |-  ( -. 
A. w  w  =  x  ->  A. w  -.  A. x  x  =  w )
1611, 15syl 15 . . . . . 6  |-  ( -. 
A. x  x  =  w  ->  A. w  -.  A. x  x  =  w )
17 ax-17 1603 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  A. w  -.  A. x  x  =  y )
1816, 17hban 1736 . . . . 5  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  A. w
( -.  A. x  x  =  w  /\  -.  A. x  x  =  y ) )
19 hbn1 1704 . . . . . . 7  |-  ( -. 
A. x  x  =  w  ->  A. x  -.  A. x  x  =  w )
20 hbn1 1704 . . . . . . 7  |-  ( -. 
A. x  x  =  y  ->  A. x  -.  A. x  x  =  y )
2119, 20hban 1736 . . . . . 6  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  A. x
( -.  A. x  x  =  w  /\  -.  A. x  x  =  y ) )
22 ax12o 1875 . . . . . . 7  |-  ( -. 
A. x  x  =  w  ->  ( -.  A. x  x  =  y  ->  ( w  =  y  ->  A. x  w  =  y )
) )
2322imp 418 . . . . . 6  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  ( w  =  y  ->  A. x  w  =  y )
)
24 a17d 1604 . . . . . 6  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  ( z  =  w  ->  A. x  z  =  w )
)
2521, 23, 24hbimd 1721 . . . . 5  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  ( (
w  =  y  -> 
z  =  w )  ->  A. x ( w  =  y  ->  z  =  w ) ) )
2618, 25hbald 1714 . . . 4  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  ( A. w ( w  =  y  ->  z  =  w )  ->  A. x A. w ( w  =  y  ->  z  =  w ) ) )
275biimpd 198 . . . . . . . 8  |-  ( w  =  y  ->  (
z  =  w  -> 
z  =  y ) )
2827a2i 12 . . . . . . 7  |-  ( ( w  =  y  -> 
z  =  w )  ->  ( w  =  y  ->  z  =  y ) )
2928alimi 1546 . . . . . 6  |-  ( A. w ( w  =  y  ->  z  =  w )  ->  A. w
( w  =  y  ->  z  =  y ) )
30 ax9v 1636 . . . . . . 7  |-  -.  A. w  -.  w  =  y
31 con3 126 . . . . . . . 8  |-  ( ( w  =  y  -> 
z  =  y )  ->  ( -.  z  =  y  ->  -.  w  =  y ) )
3231al2imi 1548 . . . . . . 7  |-  ( A. w ( w  =  y  ->  z  =  y )  ->  ( A. w  -.  z  =  y  ->  A. w  -.  w  =  y
) )
3330, 32mtoi 169 . . . . . 6  |-  ( A. w ( w  =  y  ->  z  =  y )  ->  -.  A. w  -.  z  =  y )
34 ax-17 1603 . . . . . . 7  |-  ( -.  z  =  y  ->  A. w  -.  z  =  y )
3534con1i 121 . . . . . 6  |-  ( -. 
A. w  -.  z  =  y  ->  z  =  y )
3629, 33, 353syl 18 . . . . 5  |-  ( A. w ( w  =  y  ->  z  =  w )  ->  z  =  y )
3736alimi 1546 . . . 4  |-  ( A. x A. w ( w  =  y  ->  z  =  w )  ->  A. x  z  =  y )
389, 26, 37syl56 30 . . 3  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  ( z  =  y  ->  A. x  z  =  y )
)
3938expcom 424 . 2  |-  ( -. 
A. x  x  =  y  ->  ( -.  A. x  x  =  w  ->  ( z  =  y  ->  A. x  z  =  y )
) )
40 sp 1716 . . . 4  |-  ( A. x  x  =  w  ->  x  =  w )
41 ax-11 1715 . . . 4  |-  ( x  =  w  ->  ( A. w  z  =  y  ->  A. x ( x  =  w  ->  z  =  y ) ) )
4240, 1, 41syl2im 34 . . 3  |-  ( A. x  x  =  w  ->  ( z  =  y  ->  A. x ( x  =  w  ->  z  =  y ) ) )
43 pm2.27 35 . . . 4  |-  ( x  =  w  ->  (
( x  =  w  ->  z  =  y )  ->  z  =  y ) )
4443al2imi 1548 . . 3  |-  ( A. x  x  =  w  ->  ( A. x ( x  =  w  -> 
z  =  y )  ->  A. x  z  =  y ) )
4542, 44syld 40 . 2  |-  ( A. x  x  =  w  ->  ( z  =  y  ->  A. x  z  =  y ) )
4639, 45pm2.61d2 152 1  |-  ( -. 
A. x  x  =  y  ->  ( z  =  y  ->  A. x  z  =  y )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   A.wal 1527
This theorem is referenced by:  ax10lem18ALT  29124
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-ex 1529
  Copyright terms: Public domain W3C validator