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

Theorem a9e2ndeqVD 28685
Description: The following User's Proof is a Virtual Deduction proof (see: wvd1 28337) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. a9e2eq 28323 is a9e2ndeqVD 28685 without virtual deductions and was automatically derived from a9e2ndeqVD 28685. (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 28324 . . 3  |-  ( -. 
A. x  x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
2 a9e2eq 28323 . . . 4  |-  ( A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y
( x  =  u  /\  y  =  v ) ) )
31a1d 22 . . . 4  |-  ( -. 
A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) )
4 exmid 404 . . . 4  |-  ( A. x  x  =  y  \/  -.  A. x  x  =  y )
5 jao 498 . . . 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 28542 . . 3  |-  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
71, 6jaoi 368 . 2  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  ->  E. x E. y ( x  =  u  /\  y  =  v )
)
8 idn1 28342 . . . . . . . . . . . . . . . 16  |-  (. u  =/=  v  ->.  u  =/=  v ).
9 idn2 28385 . . . . . . . . . . . . . . . . 17  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  ( x  =  u  /\  y  =  v ) ).
10 simpl 443 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
119, 10e2 28403 . . . . . . . . . . . . . . . 16  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =  u ).
12 neeq1 2454 . . . . . . . . . . . . . . . . 17  |-  ( x  =  u  ->  (
x  =/=  v  <->  u  =/=  v ) )
1312biimprcd 216 . . . . . . . . . . . . . . . 16  |-  ( u  =/=  v  ->  (
x  =  u  ->  x  =/=  v ) )
148, 11, 13e12 28499 . . . . . . . . . . . . . . 15  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  v ).
15 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
169, 15e2 28403 . . . . . . . . . . . . . . 15  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  y  =  v ).
17 neeq2 2455 . . . . . . . . . . . . . . . 16  |-  ( y  =  v  ->  (
x  =/=  y  <->  x  =/=  v ) )
1817biimprcd 216 . . . . . . . . . . . . . . 15  |-  ( x  =/=  v  ->  (
y  =  v  ->  x  =/=  y ) )
1914, 16, 18e22 28443 . . . . . . . . . . . . . 14  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  y ).
20 df-ne 2448 . . . . . . . . . . . . . . . 16  |-  ( x  =/=  y  <->  -.  x  =  y )
2120bicomi 193 . . . . . . . . . . . . . . 15  |-  ( -.  x  =  y  <->  x  =/=  y )
22 sp 1716 . . . . . . . . . . . . . . . 16  |-  ( A. x  x  =  y  ->  x  =  y )
2322con3i 127 . . . . . . . . . . . . . . 15  |-  ( -.  x  =  y  ->  -.  A. x  x  =  y )
2421, 23sylbir 204 . . . . . . . . . . . . . 14  |-  ( x  =/=  y  ->  -.  A. x  x  =  y )
2519, 24e2 28403 . . . . . . . . . . . . 13  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  -.  A. x  x  =  y ).
2625in2 28377 . . . . . . . . . . . 12  |-  (. u  =/=  v  ->.  ( ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
2726gen11 28388 . . . . . . . . . . 11  |-  (. u  =/=  v  ->.  A. x ( ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
28 exim 1562 . . . . . . . . . . 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_ 28399 . . . . . . . . . 10  |-  (. u  =/=  v  ->.  ( E. x
( x  =  u  /\  y  =  v )  ->  E. x  -.  A. x  x  =  y ) ).
30 nfnae 1896 . . . . . . . . . . 11  |-  F/ x  -.  A. x  x  =  y
313019.9 1783 . . . . . . . . . 10  |-  ( E. x  -.  A. x  x  =  y  <->  -.  A. x  x  =  y )
32 imbi2 314 . . . . . . . . . . 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 215 . . . . . . . . . 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 28467 . . . . . . . . 9  |-  (. u  =/=  v  ->.  ( E. x
( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
3534gen11 28388 . . . . . . . 8  |-  (. u  =/=  v  ->.  A. y ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
36 exim 1562 . . . . . . . 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_ 28399 . . . . . . 7  |-  (. u  =/=  v  ->.  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) ).
38 excom 1786 . . . . . . 7  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  <->  E. y E. x ( x  =  u  /\  y  =  v )
)
39 imbi1 313 . . . . . . . 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 216 . . . . . . 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 28467 . . . . . 6  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) ).
42 hbnae 1895 . . . . . . . . 9  |-  ( -. 
A. x  x  =  y  ->  A. y  -.  A. x  x  =  y )
4342eximi 1563 . . . . . . . 8  |-  ( E. y  -.  A. x  x  =  y  ->  E. y A. y  -. 
A. x  x  =  y )
44 nfa1 1756 . . . . . . . . 9  |-  F/ y A. y  -.  A. x  x  =  y
454419.9 1783 . . . . . . . 8  |-  ( E. y A. y  -. 
A. x  x  =  y  <->  A. y  -.  A. x  x  =  y
)
4643, 45sylib 188 . . . . . . 7  |-  ( E. y  -.  A. x  x  =  y  ->  A. y  -.  A. x  x  =  y )
47 sp 1716 . . . . . . 7  |-  ( A. y  -.  A. x  x  =  y  ->  -.  A. x  x  =  y )
4846, 47syl 15 . . . . . 6  |-  ( E. y  -.  A. x  x  =  y  ->  -. 
A. x  x  =  y )
49 imim1 70 . . . . . 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 28467 . . . . 5  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
51 orc 374 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  ( -.  A. x  x  =  y  \/  u  =  v ) )
5251imim2i 13 . . . . 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_ 28399 . . . 4  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) ).
5453in1 28339 . . 3  |-  ( u  =/=  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )
55 idn1 28342 . . . . . 6  |-  (. u  =  v  ->.  u  =  v ).
56 ax-1 5 . . . . . 6  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  u  =  v ) )
5755, 56e1_ 28399 . . . . 5  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  u  =  v ) ).
58 olc 373 . . . . . 6  |-  ( u  =  v  ->  ( -.  A. x  x  =  y  \/  u  =  v ) )
5958imim2i 13 . . . . 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_ 28399 . . . 4  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) ).
6160in1 28339 . . 3  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )
62 exmidne 2452 . . 3  |-  ( u  =  v  \/  u  =/=  v )
63 jao 498 . . . 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 27 . . 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 28542 . 2  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
)
667, 65impbii 180 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 176    \/ wo 357    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    =/= wne 2446
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  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-fal 1311  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ne 2448  df-v 2790  df-vd1 28338  df-vd2 28347
  Copyright terms: Public domain W3C validator