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

Theorem ax10lem17ALT 29745
Description: Lemma for ax10 1897. Similar to dveeq2 1893, without using sp 1728, ax9 1902, or ax10 1897 but allowing ax9v 1645. Direct proof of dveeq2 1893, bypassing dvelimnf 1970 to investigate possible simplifications. Uses ax12o 1887. (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 1606 . . . . . 6  |-  ( z  =  y  ->  A. w  z  =  y )
21a1d 22 . . . . . 6  |-  ( z  =  y  ->  (
w  =  y  ->  A. w  z  =  y ) )
31, 2alrimih 1555 . . . . 5  |-  ( z  =  y  ->  A. w
( w  =  y  ->  A. w  z  =  y ) )
4 sp 1728 . . . . . . . 8  |-  ( A. w  z  =  y  ->  z  =  y )
5 equequ2 1669 . . . . . . . 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 1549 . . . . 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 1891 . . . . . . . 8  |-  ( A. w  w  =  x  ->  A. x  x  =  w )
1110con3i 127 . . . . . . 7  |-  ( -. 
A. x  x  =  w  ->  -.  A. w  w  =  x )
12 hbn1 1716 . . . . . . . 8  |-  ( -. 
A. w  w  =  x  ->  A. w  -.  A. w  w  =  x )
13 ax10lem3 1891 . . . . . . . . 9  |-  ( A. x  x  =  w  ->  A. w  w  =  x )
1413con3i 127 . . . . . . . 8  |-  ( -. 
A. w  w  =  x  ->  -.  A. x  x  =  w )
1512, 14alrimih 1555 . . . . . . 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 1606 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  A. w  -.  A. x  x  =  y )
1816, 17hban 1748 . . . . 5  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  A. w
( -.  A. x  x  =  w  /\  -.  A. x  x  =  y ) )
19 hbn1 1716 . . . . . . 7  |-  ( -. 
A. x  x  =  w  ->  A. x  -.  A. x  x  =  w )
20 hbn1 1716 . . . . . . 7  |-  ( -. 
A. x  x  =  y  ->  A. x  -.  A. x  x  =  y )
2119, 20hban 1748 . . . . . 6  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  A. x
( -.  A. x  x  =  w  /\  -.  A. x  x  =  y ) )
22 ax12o 1887 . . . . . . 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 1607 . . . . . 6  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  ( z  =  w  ->  A. x  z  =  w )
)
2521, 23, 24hbimd 1733 . . . . 5  |-  ( ( -.  A. x  x  =  w  /\  -.  A. x  x  =  y )  ->  ( (
w  =  y  -> 
z  =  w )  ->  A. x ( w  =  y  ->  z  =  w ) ) )
2618, 25hbald 1726 . . . 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 1549 . . . . . 6  |-  ( A. w ( w  =  y  ->  z  =  w )  ->  A. w
( w  =  y  ->  z  =  y ) )
30 ax9v 1645 . . . . . . 7  |-  -.  A. w  -.  w  =  y
31 con3 126 . . . . . . . 8  |-  ( ( w  =  y  -> 
z  =  y )  ->  ( -.  z  =  y  ->  -.  w  =  y ) )
3231al2imi 1551 . . . . . . 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 1606 . . . . . . 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 1549 . . . 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 1728 . . . 4  |-  ( A. x  x  =  w  ->  x  =  w )
41 ax-11 1727 . . . 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 1551 . . 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 1530
This theorem is referenced by:  ax10lem18ALT  29746
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-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
  Copyright terms: Public domain W3C validator