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

Theorem ax9lem17 29156
Description: Lemma for ax9 1889. Similar to dvelim 1956 with first hypothesis replaced by distinct variable condition, without using sp 1716, ax9 1889, or ax10 1884. We used ax9lem6 29145 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 1603 . . . . . 6  |-  ( ps 
->  A. z ps )
21a1d 22 . . . . . 6  |-  ( ps 
->  ( z  =  y  ->  A. z ps )
)
31, 2alrimih 1552 . . . . 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 29142 . . . . . . . 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 1546 . . . . 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 29145 . . . . . 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 29145 . . . . . . . . 9  |-  -.  A. w  -.  w  =  u
20 ax9lem17.m . . . . . . . . . 10  |-  -.  A. x  -.  x  =  w
2117, 20, 18, 14ax9lem6 29145 . . . . . . . . 9  |-  -.  A. x  -.  x  =  v
22 ax9lem17.b . . . . . . . . 9  |-  -.  A. u  -.  u  =  w
2312, 16, 4, 19, 5, 13, 21, 20, 14, 22ax9lem16 29155 . . . . . . . 8  |-  ( A. z  z  =  x  ->  A. x  x  =  z )
2423con3i 127 . . . . . . 7  |-  ( -. 
A. x  x  =  z  ->  -.  A. z 
z  =  x )
25 hbn1 1704 . . . . . . . 8  |-  ( -. 
A. z  z  =  x  ->  A. z  -.  A. z  z  =  x )
2616, 12, 17, 19, 20, 18, 15, 5, 14, 22ax9lem16 29155 . . . . . . . . 9  |-  ( A. x  x  =  z  ->  A. z  z  =  x )
2726con3i 127 . . . . . . . 8  |-  ( -. 
A. z  z  =  x  ->  -.  A. x  x  =  z )
2825, 27alrimih 1552 . . . . . . 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 1603 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  A. z  -.  A. x  x  =  y )
3112, 15, 29, 30ax9lem10 29149 . . . . 5  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  A. z
( -.  A. x  x  =  z  /\  -.  A. x  x  =  y ) )
32 hbn1 1704 . . . . . . 7  |-  ( -. 
A. x  x  =  z  ->  A. x  -.  A. x  x  =  z )
33 hbn1 1704 . . . . . . 7  |-  ( -. 
A. x  x  =  y  ->  A. x  -.  A. x  x  =  y )
3416, 21, 32, 33ax9lem10 29149 . . . . . 6  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  A. x
( -.  A. x  x  =  z  /\  -.  A. x  x  =  y ) )
35 ax12o 1875 . . . . . . 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 1604 . . . . . 6  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  ( ph  ->  A. x ph )
)
3816, 21, 34, 36, 37ax9lem9 29148 . . . . 5  |-  ( ( -.  A. x  x  =  z  /\  -.  A. x  x  =  y )  ->  ( (
z  =  y  ->  ph )  ->  A. x
( z  =  y  ->  ph ) ) )
3931, 38hbald 1714 . . . 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 1546 . . . . . 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 1548 . . . . . . 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 1603 . . . . . . 7  |-  ( -. 
ps  ->  A. z  -.  ps )
4847con1i 121 . . . . . 6  |-  ( -. 
A. z  -.  ps  ->  ps )
4942, 46, 483syl 18 . . . . 5  |-  ( A. z ( z  =  y  ->  ph )  ->  ps )
5049alimi 1546 . . . 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 29142 . . . 4  |-  ( A. x  x  =  z  ->  x  =  z )
54 ax-11 1715 . . . 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 1548 . . 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 1527
This theorem is referenced by:  ax9lem18  29157
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