Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  a9e2ndeqVD Structured version   Unicode version

Theorem a9e2ndeqVD 29021
Description: The following User's Proof is a Virtual Deduction proof (see: wvd1 28660) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. a9e2eq 28644 is a9e2ndeqVD 29021 without virtual deductions and was automatically derived from a9e2ndeqVD 29021. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. u  =/=  v  ->.  u  =/=  v ).
2::  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  (  x  =  u  /\  y  =  v ) ).
3:2:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =  u ).
4:1,3:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  v ).
5:2:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  y  =  v ).
6:4,5:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  y ).
7::  |-  ( A. x x  =  y  ->  x  =  y )
8:7:  |-  ( -.  x  =  y  ->  -.  A. x x  =  y )
9::  |-  ( -.  x  =  y  <->  x  =/=  y )
10:8,9:  |-  ( x  =/=  y  ->  -.  A. x x  =  y )
11:6,10:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  -.  A. x x  =  y ).
12:11:  |-  (. u  =/=  v  ->.  ( ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
13:12:  |-  (. u  =/=  v  ->.  A. x ( ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
14:13:  |-  (. u  =/=  v  ->.  ( E. x ( x  =  u  /\  y  =  v )  ->  E. x -.  A. x x  =  y ) ).
15::  |-  ( -.  A. x x  =  y  ->  A. x -.  A. x x  =  y  )
19:15:  |-  ( E. x -.  A. x x  =  y  <->  -.  A. x x  =  y )
20:14,19:  |-  (. u  =/=  v  ->.  ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
21:20:  |-  (. u  =/=  v  ->.  A. y ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
22:21:  |-  (. u  =/=  v  ->.  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y -.  A. x x  =  y ) ).
23::  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  <->  E.  y E. x ( x  =  u  /\  y  =  v ) )
24:22,23:  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y -.  A. x x  =  y ) ).
25::  |-  ( -.  A. x x  =  y  ->  A. y -.  A. x x  =  y  )
26:25:  |-  ( E. y -.  A. x x  =  y  ->  E. y A. y -.  A. x x  =  y )
260::  |-  ( A. y -.  A. x x  =  y  ->  A. y A. y -.  A. x x  =  y )
27:260:  |-  ( E. y A. y -.  A. x x  =  y  <->  A. y -.  A. x x  =  y )
270:26,27:  |-  ( E. y -.  A. x x  =  y  ->  A. y -.  A. x  x  =  y )
28::  |-  ( A. y -.  A. x x  =  y  ->  -.  A. x x  =  y  )
29:270,28:  |-  ( E. y -.  A. x x  =  y  ->  -.  A. x x  =  y  )
30:24,29:  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
31:30:  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) ).
32:31:  |-  ( u  =/=  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) )
33::  |-  (. u  =  v  ->.  u  =  v ).
34:33:  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  u  =  v ) ).
35:34:  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) ).
36:35:  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) )
37::  |-  ( u  =  v  \/  u  =/=  v )
38:32,36,37:  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  (  -.  A. x x  =  y  \/  u  =  v ) )
39::  |-  ( A. x x  =  y  ->  ( u  =  v  ->  E. x E. y  ( x  =  u  /\  y  =  v ) ) )
40::  |-  ( -.  A. x x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
41:40:  |-  ( -.  A. x x  =  y  ->  ( u  =  v  ->  E. x E.  y ( x  =  u  /\  y  =  v ) ) )
42::  |-  ( A. x x  =  y  \/  -.  A. x x  =  y )
43:39,41,42:  |-  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v  ) )
44:40,43:  |-  ( ( -.  A. x x  =  y  \/  u  =  v )  ->  E. x  E. y ( x  =  u  /\  y  =  v ) )
qed:38,44:  |-  ( ( -.  A. x x  =  y  \/  u  =  v )  <->  E. x  E. y ( x  =  u  /\  y  =  v ) )
Assertion
Ref Expression
a9e2ndeqVD  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  <->  E. x E. y ( x  =  u  /\  y  =  v ) )
Distinct variable groups:    x, u    y, u    x, v    y,
v

Proof of Theorem a9e2ndeqVD
StepHypRef Expression
1 a9e2nd 28645 . . 3  |-  ( -. 
A. x  x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
2 a9e2eq 28644 . . . 4  |-  ( A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y
( x  =  u  /\  y  =  v ) ) )
31a1d 23 . . . 4  |-  ( -. 
A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) )
4 exmid 405 . . . 4  |-  ( A. x  x  =  y  \/  -.  A. x  x  =  y )
5 jao 499 . . . 4  |-  ( ( A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) )  ->  ( ( -. 
A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) )  ->  ( ( A. x  x  =  y  \/  -.  A. x  x  =  y )  -> 
( u  =  v  ->  E. x E. y
( x  =  u  /\  y  =  v ) ) ) ) )
62, 3, 4, 5e000 28879 . . 3  |-  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
71, 6jaoi 369 . 2  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  ->  E. x E. y ( x  =  u  /\  y  =  v )
)
8 idn1 28665 . . . . . . . . . . . . . . . 16  |-  (. u  =/=  v  ->.  u  =/=  v ).
9 idn2 28714 . . . . . . . . . . . . . . . . 17  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  ( x  =  u  /\  y  =  v ) ).
10 simpl 444 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
119, 10e2 28732 . . . . . . . . . . . . . . . 16  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =  u ).
12 neeq1 2609 . . . . . . . . . . . . . . . . 17  |-  ( x  =  u  ->  (
x  =/=  v  <->  u  =/=  v ) )
1312biimprcd 217 . . . . . . . . . . . . . . . 16  |-  ( u  =/=  v  ->  (
x  =  u  ->  x  =/=  v ) )
148, 11, 13e12 28836 . . . . . . . . . . . . . . 15  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  v ).
15 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
169, 15e2 28732 . . . . . . . . . . . . . . 15  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  y  =  v ).
17 neeq2 2610 . . . . . . . . . . . . . . . 16  |-  ( y  =  v  ->  (
x  =/=  y  <->  x  =/=  v ) )
1817biimprcd 217 . . . . . . . . . . . . . . 15  |-  ( x  =/=  v  ->  (
y  =  v  ->  x  =/=  y ) )
1914, 16, 18e22 28772 . . . . . . . . . . . . . 14  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  y ).
20 df-ne 2601 . . . . . . . . . . . . . . . 16  |-  ( x  =/=  y  <->  -.  x  =  y )
2120bicomi 194 . . . . . . . . . . . . . . 15  |-  ( -.  x  =  y  <->  x  =/=  y )
22 sp 1763 . . . . . . . . . . . . . . . 16  |-  ( A. x  x  =  y  ->  x  =  y )
2322con3i 129 . . . . . . . . . . . . . . 15  |-  ( -.  x  =  y  ->  -.  A. x  x  =  y )
2421, 23sylbir 205 . . . . . . . . . . . . . 14  |-  ( x  =/=  y  ->  -.  A. x  x  =  y )
2519, 24e2 28732 . . . . . . . . . . . . 13  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  -.  A. x  x  =  y ).
2625in2 28706 . . . . . . . . . . . 12  |-  (. u  =/=  v  ->.  ( ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
2726gen11 28717 . . . . . . . . . . 11  |-  (. u  =/=  v  ->.  A. x ( ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
28 exim 1584 . . . . . . . . . . 11  |-  ( A. x ( ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y )  ->  ( E. x ( x  =  u  /\  y  =  v )  ->  E. x  -.  A. x  x  =  y ) )
2927, 28e1_ 28728 . . . . . . . . . 10  |-  (. u  =/=  v  ->.  ( E. x
( x  =  u  /\  y  =  v )  ->  E. x  -.  A. x  x  =  y ) ).
30 nfnae 2044 . . . . . . . . . . 11  |-  F/ x  -.  A. x  x  =  y
313019.9 1797 . . . . . . . . . 10  |-  ( E. x  -.  A. x  x  =  y  <->  -.  A. x  x  =  y )
32 imbi2 315 . . . . . . . . . . 11  |-  ( ( E. x  -.  A. x  x  =  y  <->  -. 
A. x  x  =  y )  ->  (
( E. x ( x  =  u  /\  y  =  v )  ->  E. x  -.  A. x  x  =  y
)  <->  ( E. x
( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y )
) )
3332biimpcd 216 . . . . . . . . . 10  |-  ( ( E. x ( x  =  u  /\  y  =  v )  ->  E. x  -.  A. x  x  =  y )  ->  ( ( E. x  -.  A. x  x  =  y  <->  -.  A. x  x  =  y )  ->  ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ) )
3429, 31, 33e10 28795 . . . . . . . . 9  |-  (. u  =/=  v  ->.  ( E. x
( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
3534gen11 28717 . . . . . . . 8  |-  (. u  =/=  v  ->.  A. y ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
36 exim 1584 . . . . . . . 8  |-  ( A. y ( E. x
( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y )  ->  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) )
3735, 36e1_ 28728 . . . . . . 7  |-  (. u  =/=  v  ->.  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) ).
38 excom 1756 . . . . . . 7  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  <->  E. y E. x ( x  =  u  /\  y  =  v )
)
39 imbi1 314 . . . . . . . 8  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  <->  E. y E. x
( x  =  u  /\  y  =  v ) )  ->  (
( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y )  <->  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y )
) )
4039biimprcd 217 . . . . . . 7  |-  ( ( E. y E. x
( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y )  ->  (
( E. x E. y ( x  =  u  /\  y  =  v )  <->  E. y E. x ( x  =  u  /\  y  =  v ) )  -> 
( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) ) )
4137, 38, 40e10 28795 . . . . . 6  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) ).
42 hbnae 2043 . . . . . . . . 9  |-  ( -. 
A. x  x  =  y  ->  A. y  -.  A. x  x  =  y )
4342eximi 1585 . . . . . . . 8  |-  ( E. y  -.  A. x  x  =  y  ->  E. y A. y  -. 
A. x  x  =  y )
44 nfa1 1806 . . . . . . . . 9  |-  F/ y A. y  -.  A. x  x  =  y
454419.9 1797 . . . . . . . 8  |-  ( E. y A. y  -. 
A. x  x  =  y  <->  A. y  -.  A. x  x  =  y
)
4643, 45sylib 189 . . . . . . 7  |-  ( E. y  -.  A. x  x  =  y  ->  A. y  -.  A. x  x  =  y )
47 sp 1763 . . . . . . 7  |-  ( A. y  -.  A. x  x  =  y  ->  -.  A. x  x  =  y )
4846, 47syl 16 . . . . . 6  |-  ( E. y  -.  A. x  x  =  y  ->  -. 
A. x  x  =  y )
49 imim1 72 . . . . . 6  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y )  ->  (
( E. y  -. 
A. x  x  =  y  ->  -.  A. x  x  =  y )  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ) )
5041, 48, 49e10 28795 . . . . 5  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
51 orc 375 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  ( -.  A. x  x  =  y  \/  u  =  v ) )
5251imim2i 14 . . . . 5  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y )  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) )
5350, 52e1_ 28728 . . . 4  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) ).
5453in1 28662 . . 3  |-  ( u  =/=  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )
55 idn1 28665 . . . . . 6  |-  (. u  =  v  ->.  u  =  v ).
56 ax-1 5 . . . . . 6  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  u  =  v ) )
5755, 56e1_ 28728 . . . . 5  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  u  =  v ) ).
58 olc 374 . . . . . 6  |-  ( u  =  v  ->  ( -.  A. x  x  =  y  \/  u  =  v ) )
5958imim2i 14 . . . . 5  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  ->  u  =  v )  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )
6057, 59e1_ 28728 . . . 4  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) ).
6160in1 28662 . . 3  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )
62 exmidne 2607 . . 3  |-  ( u  =  v  \/  u  =/=  v )
63 jao 499 . . . 4  |-  ( ( u  =  v  -> 
( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) )  ->  ( ( u  =/=  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )  ->  (
( u  =  v  \/  u  =/=  v
)  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  -> 
( -.  A. x  x  =  y  \/  u  =  v )
) ) ) )
6463com12 29 . . 3  |-  ( ( u  =/=  v  -> 
( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) )  ->  ( ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )  ->  (
( u  =  v  \/  u  =/=  v
)  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  -> 
( -.  A. x  x  =  y  \/  u  =  v )
) ) ) )
6554, 61, 62, 64e000 28879 . 2  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
)
667, 65impbii 181 1  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  <->  E. x E. y ( x  =  u  /\  y  =  v ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359   A.wal 1549   E.wex 1550    = wceq 1652    =/= wne 2599
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-ne 2601  df-v 2958  df-vd1 28661  df-vd2 28670
  Copyright terms: Public domain W3C validator