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

Theorem ax9lem17 29215
Description: Lemma for ax9 1962. Similar to dvelim 2029 with first hypothesis replaced by distinct variable condition, without using sp 1753, ax9 1962, or ax10 1957. We used ax9lem6 29204 to eliminate 3 hypotheses that would otherwise be needed. (Contributed by NM, 7-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
ax9lem17.a  |-  -.  A. u  -.  u  =  v
ax9lem17.b  |-  -.  A. u  -.  u  =  w
ax9lem17.e  |-  -.  A. v  -.  v  =  x
ax9lem17.f  |-  -.  A. v  -.  v  =  z
ax9lem17.i  |-  -.  A. w  -.  w  =  x
ax9lem17.j  |-  -.  A. w  -.  w  =  z
ax9lem17.k  |-  -.  A. x  -.  x  =  u
ax9lem17.m  |-  -.  A. x  -.  x  =  w
ax9lem17.p  |-  -.  A. z  -.  z  =  u
ax9lem17.r  |-  -.  A. z  -.  z  =  w
ax9lem17.t  |-  -.  A. z  -.  z  =  y
ax9lem17.1  |-  ( z  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ax9lem17  |-  ( -. 
A. x  x  =  y  ->  ( ps  ->  A. x ps )
)
Distinct variable groups:    v, u, w, x, z    y, v, z    ps, z, w    ph, x
Allowed substitution hints:    ph( y, z, w, v, u)    ps( x, y, v, u)

Proof of Theorem ax9lem17
StepHypRef Expression
1 ax-17 1621 . . . . . 6  |-  ( ps 
->  A. z ps )
21a1d 22 . . . . . 6  |-  ( ps 
->  ( z  =  y  ->  A. z ps )
)
31, 2alrimih 1570 . . . . 5  |-  ( ps 
->  A. z ( z  =  y  ->  A. z ps ) )
4 ax9lem17.j . . . . . . . . 9  |-  -.  A. w  -.  w  =  z
5 ax9lem17.r . . . . . . . . 9  |-  -.  A. z  -.  z  =  w
64, 5ax9lem3 29201 . . . . . . . 8  |-  ( A. z ps  ->  ps )
7 ax9lem17.1 . . . . . . . 8  |-  ( z  =  y  ->  ( ph 
<->  ps ) )
86, 7syl5ibr 212 . . . . . . 7  |-  ( z  =  y  ->  ( A. z ps  ->  ph )
)
98a2i 12 . . . . . 6  |-  ( ( z  =  y  ->  A. z ps )  -> 
( z  =  y  ->  ph ) )
109alimi 1564 . . . . 5  |-  ( A. z ( z  =  y  ->  A. z ps )  ->  A. z
( z  =  y  ->  ph ) )
113, 10syl 15 . . . 4  |-  ( ps 
->  A. z ( z  =  y  ->  ph )
)
12 ax9lem17.f . . . . . 6  |-  -.  A. v  -.  v  =  z
13 ax9lem17.p . . . . . . 7  |-  -.  A. z  -.  z  =  u
14 ax9lem17.a . . . . . . 7  |-  -.  A. u  -.  u  =  v
154, 5, 13, 14ax9lem6 29204 . . . . . 6  |-  -.  A. z  -.  z  =  v
16 ax9lem17.e . . . . . . . . 9  |-  -.  A. v  -.  v  =  x
17 ax9lem17.i . . . . . . . . . 10  |-  -.  A. w  -.  w  =  x
18 ax9lem17.k . . . . . . . . . 10  |-  -.  A. x  -.  x  =  u
195, 4, 17, 18ax9lem6 29204 . . . . . . . . 9  |-  -.  A. w  -.  w  =  u
20 ax9lem17.m . . . . . . . . . 10  |-  -.  A. x  -.  x  =  w
2117, 20, 18, 14ax9lem6 29204 . . . . . . . . 9  |-  -.  A. x  -.  x  =  v
22 ax9lem17.b . . . . . . . . 9  |-  -.  A. u  -.  u  =  w
2312, 16, 4, 19, 5, 13, 21, 20, 14, 22ax9lem16 29214 . . . . . . . 8  |-  ( A. z  z  =  x  ->  A. x  x  =  z )
2423con3i 127 . . . . . . 7  |-  ( -. 
A. x  x  =  z  ->  -.  A. z 
z  =  x )
25 hbn1 1735 . . . . . . . 8  |-  ( -. 
A. z  z  =  x  ->  A. z  -.  A. z  z  =  x )
2616, 12, 17, 19, 20, 18, 15, 5, 14, 22ax9lem16 29214 . . . . . . . . 9  |-  ( A. x  x  =  z  ->  A. z  z  =  x )
2726con3i 127 . . . . . . . 8  |-  ( -. 
A. z  z  =  x  ->  -.  A. x  x  =  z )
2825, 27alrimih 1570 . . . . . . 7  |-  ( -. 
A. z  z  =  x  ->  A. z  -.  A. x  x  =  z )
2924, 28syl 15 . . . . . 6  |-  ( -. 
A. x  x  =  z  ->  A. z  -.  A. x  x  =  z )
30 ax-17 1621 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  A. z  -.  A. x  x  =  y )
3112, 15, 29, 30ax9lem10 29208 . . . . 5  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  A. z
( -.  A. x  x  =  z  /\  -.  A. x  x  =  y ) )
32 hbn1 1735 . . . . . . 7  |-  ( -. 
A. x  x  =  z  ->  A. x  -.  A. x  x  =  z )
33 hbn1 1735 . . . . . . 7  |-  ( -. 
A. x  x  =  y  ->  A. x  -.  A. x  x  =  y )
3416, 21, 32, 33ax9lem10 29208 . . . . . 6  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  A. x
( -.  A. x  x  =  z  /\  -.  A. x  x  =  y ) )
35 ax12o 1947 . . . . . . 7  |-  ( -. 
A. x  x  =  z  ->  ( -.  A. x  x  =  y  ->  ( z  =  y  ->  A. x  z  =  y )
) )
3635imp 418 . . . . . 6  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  ( z  =  y  ->  A. x  z  =  y )
)
37 a17d 1622 . . . . . 6  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  ( ph  ->  A. x ph )
)
3816, 21, 34, 36, 37ax9lem9 29207 . . . . 5  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  ( (
z  =  y  ->  ph )  ->  A. x
( z  =  y  ->  ph ) ) )
3931, 38hbald 1745 . . . 4  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  ( A. z ( z  =  y  ->  ph )  ->  A. x A. z ( z  =  y  ->  ph ) ) )
407biimpd 198 . . . . . . . 8  |-  ( z  =  y  ->  ( ph  ->  ps ) )
4140a2i 12 . . . . . . 7  |-  ( ( z  =  y  ->  ph )  ->  ( z  =  y  ->  ps ) )
4241alimi 1564 . . . . . 6  |-  ( A. z ( z  =  y  ->  ph )  ->  A. z ( z  =  y  ->  ps )
)
43 ax9lem17.t . . . . . . 7  |-  -.  A. z  -.  z  =  y
44 con3 126 . . . . . . . 8  |-  ( ( z  =  y  ->  ps )  ->  ( -. 
ps  ->  -.  z  =  y ) )
4544al2imi 1566 . . . . . . 7  |-  ( A. z ( z  =  y  ->  ps )  ->  ( A. z  -. 
ps  ->  A. z  -.  z  =  y ) )
4643, 45mtoi 169 . . . . . 6  |-  ( A. z ( z  =  y  ->  ps )  ->  -.  A. z  -. 
ps )
47 ax-17 1621 . . . . . . 7  |-  ( -. 
ps  ->  A. z  -.  ps )
4847con1i 121 . . . . . 6  |-  ( -. 
A. z  -.  ps  ->  ps )
4942, 46, 483syl 18 . . . . 5  |-  ( A. z ( z  =  y  ->  ph )  ->  ps )
5049alimi 1564 . . . 4  |-  ( A. x A. z ( z  =  y  ->  ph )  ->  A. x ps )
5111, 39, 50syl56 30 . . 3  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  ( ps  ->  A. x ps )
)
5251expcom 424 . 2  |-  ( -. 
A. x  x  =  y  ->  ( -.  A. x  x  =  z  ->  ( ps  ->  A. x ps ) ) )
5316, 21ax9lem3 29201 . . . 4  |-  ( A. x  x  =  z  ->  x  =  z )
54 ax-11 1751 . . . 4  |-  ( x  =  z  ->  ( A. z ps  ->  A. x
( x  =  z  ->  ps ) ) )
5553, 1, 54syl2im 34 . . 3  |-  ( A. x  x  =  z  ->  ( ps  ->  A. x
( x  =  z  ->  ps ) ) )
56 pm2.27 35 . . . 4  |-  ( x  =  z  ->  (
( x  =  z  ->  ps )  ->  ps ) )
5756al2imi 1566 . . 3  |-  ( A. x  x  =  z  ->  ( A. x ( x  =  z  ->  ps )  ->  A. x ps ) )
5855, 57syld 40 . 2  |-  ( A. x  x  =  z  ->  ( ps  ->  A. x ps ) )
5952, 58pm2.61d2 152 1  |-  ( -. 
A. x  x  =  y  ->  ( ps  ->  A. x ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1545
This theorem is referenced by:  ax9lem18  29216
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-nf 1550
  Copyright terms: Public domain W3C validator