MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac5lem1 Structured version   Unicode version

Theorem dfac5lem1 8507
Description: Lemma for dfac5 8512. (Contributed by NM, 12-Apr-2004.)
Assertion
Ref Expression
dfac5lem1  |-  ( E! v  v  e.  ( ( { w }  X.  w )  i^i  y
)  <->  E! g ( g  e.  w  /\  <. w ,  g >.  e.  y ) )
Distinct variable group:    w, v, y, g

Proof of Theorem dfac5lem1
Dummy variable  t is distinct from all other variables.
StepHypRef Expression
1 elin 3672 . . . 4  |-  ( v  e.  ( ( { w }  X.  w
)  i^i  y )  <->  ( v  e.  ( { w }  X.  w
)  /\  v  e.  y ) )
2 elxp 5006 . . . . . 6  |-  ( v  e.  ( { w }  X.  w )  <->  E. t E. g ( v  = 
<. t ,  g >.  /\  ( t  e.  {
w }  /\  g  e.  w ) ) )
3 excom 1835 . . . . . 6  |-  ( E. t E. g ( v  =  <. t ,  g >.  /\  (
t  e.  { w }  /\  g  e.  w
) )  <->  E. g E. t ( v  = 
<. t ,  g >.  /\  ( t  e.  {
w }  /\  g  e.  w ) ) )
42, 3bitri 249 . . . . 5  |-  ( v  e.  ( { w }  X.  w )  <->  E. g E. t ( v  = 
<. t ,  g >.  /\  ( t  e.  {
w }  /\  g  e.  w ) ) )
54anbi1i 695 . . . 4  |-  ( ( v  e.  ( { w }  X.  w
)  /\  v  e.  y )  <->  ( E. g E. t ( v  =  <. t ,  g
>.  /\  ( t  e. 
{ w }  /\  g  e.  w )
)  /\  v  e.  y ) )
6 19.41vv 1758 . . . . 5  |-  ( E. g E. t ( ( v  =  <. t ,  g >.  /\  (
t  e.  { w }  /\  g  e.  w
) )  /\  v  e.  y )  <->  ( E. g E. t ( v  =  <. t ,  g
>.  /\  ( t  e. 
{ w }  /\  g  e.  w )
)  /\  v  e.  y ) )
7 an32 798 . . . . . . . . 9  |-  ( ( ( v  =  <. t ,  g >.  /\  (
t  e.  { w }  /\  g  e.  w
) )  /\  v  e.  y )  <->  ( (
v  =  <. t ,  g >.  /\  v  e.  y )  /\  (
t  e.  { w }  /\  g  e.  w
) ) )
8 eleq1 2515 . . . . . . . . . . 11  |-  ( v  =  <. t ,  g
>.  ->  ( v  e.  y  <->  <. t ,  g
>.  e.  y ) )
98pm5.32i 637 . . . . . . . . . 10  |-  ( ( v  =  <. t ,  g >.  /\  v  e.  y )  <->  ( v  =  <. t ,  g
>.  /\  <. t ,  g
>.  e.  y ) )
10 elsn 4028 . . . . . . . . . . 11  |-  ( t  e.  { w }  <->  t  =  w )
1110anbi1i 695 . . . . . . . . . 10  |-  ( ( t  e.  { w }  /\  g  e.  w
)  <->  ( t  =  w  /\  g  e.  w ) )
129, 11anbi12i 697 . . . . . . . . 9  |-  ( ( ( v  =  <. t ,  g >.  /\  v  e.  y )  /\  (
t  e.  { w }  /\  g  e.  w
) )  <->  ( (
v  =  <. t ,  g >.  /\  <. t ,  g >.  e.  y )  /\  ( t  =  w  /\  g  e.  w ) ) )
13 an4 824 . . . . . . . . . 10  |-  ( ( ( v  =  <. t ,  g >.  /\  <. t ,  g >.  e.  y )  /\  ( t  =  w  /\  g  e.  w ) )  <->  ( (
v  =  <. t ,  g >.  /\  t  =  w )  /\  ( <. t ,  g >.  e.  y  /\  g  e.  w ) ) )
14 ancom 450 . . . . . . . . . . 11  |-  ( ( v  =  <. t ,  g >.  /\  t  =  w )  <->  ( t  =  w  /\  v  =  <. t ,  g
>. ) )
15 ancom 450 . . . . . . . . . . 11  |-  ( (
<. t ,  g >.  e.  y  /\  g  e.  w )  <->  ( g  e.  w  /\  <. t ,  g >.  e.  y ) )
1614, 15anbi12i 697 . . . . . . . . . 10  |-  ( ( ( v  =  <. t ,  g >.  /\  t  =  w )  /\  ( <. t ,  g >.  e.  y  /\  g  e.  w ) )  <->  ( (
t  =  w  /\  v  =  <. t ,  g >. )  /\  (
g  e.  w  /\  <.
t ,  g >.  e.  y ) ) )
17 anass 649 . . . . . . . . . 10  |-  ( ( ( t  =  w  /\  v  =  <. t ,  g >. )  /\  ( g  e.  w  /\  <. t ,  g
>.  e.  y ) )  <-> 
( t  =  w  /\  ( v  = 
<. t ,  g >.  /\  ( g  e.  w  /\  <. t ,  g
>.  e.  y ) ) ) )
1813, 16, 173bitri 271 . . . . . . . . 9  |-  ( ( ( v  =  <. t ,  g >.  /\  <. t ,  g >.  e.  y )  /\  ( t  =  w  /\  g  e.  w ) )  <->  ( t  =  w  /\  (
v  =  <. t ,  g >.  /\  (
g  e.  w  /\  <.
t ,  g >.  e.  y ) ) ) )
197, 12, 183bitri 271 . . . . . . . 8  |-  ( ( ( v  =  <. t ,  g >.  /\  (
t  e.  { w }  /\  g  e.  w
) )  /\  v  e.  y )  <->  ( t  =  w  /\  (
v  =  <. t ,  g >.  /\  (
g  e.  w  /\  <.
t ,  g >.  e.  y ) ) ) )
2019exbii 1654 . . . . . . 7  |-  ( E. t ( ( v  =  <. t ,  g
>.  /\  ( t  e. 
{ w }  /\  g  e.  w )
)  /\  v  e.  y )  <->  E. t
( t  =  w  /\  ( v  = 
<. t ,  g >.  /\  ( g  e.  w  /\  <. t ,  g
>.  e.  y ) ) ) )
21 vex 3098 . . . . . . . 8  |-  w  e. 
_V
22 opeq1 4202 . . . . . . . . . 10  |-  ( t  =  w  ->  <. t ,  g >.  =  <. w ,  g >. )
2322eqeq2d 2457 . . . . . . . . 9  |-  ( t  =  w  ->  (
v  =  <. t ,  g >.  <->  v  =  <. w ,  g >.
) )
2422eleq1d 2512 . . . . . . . . . 10  |-  ( t  =  w  ->  ( <. t ,  g >.  e.  y  <->  <. w ,  g
>.  e.  y ) )
2524anbi2d 703 . . . . . . . . 9  |-  ( t  =  w  ->  (
( g  e.  w  /\  <. t ,  g
>.  e.  y )  <->  ( g  e.  w  /\  <. w ,  g >.  e.  y ) ) )
2623, 25anbi12d 710 . . . . . . . 8  |-  ( t  =  w  ->  (
( v  =  <. t ,  g >.  /\  (
g  e.  w  /\  <.
t ,  g >.  e.  y ) )  <->  ( v  =  <. w ,  g
>.  /\  ( g  e.  w  /\  <. w ,  g >.  e.  y ) ) ) )
2721, 26ceqsexv 3132 . . . . . . 7  |-  ( E. t ( t  =  w  /\  ( v  =  <. t ,  g
>.  /\  ( g  e.  w  /\  <. t ,  g >.  e.  y ) ) )  <->  ( v  =  <. w ,  g
>.  /\  ( g  e.  w  /\  <. w ,  g >.  e.  y ) ) )
2820, 27bitri 249 . . . . . 6  |-  ( E. t ( ( v  =  <. t ,  g
>.  /\  ( t  e. 
{ w }  /\  g  e.  w )
)  /\  v  e.  y )  <->  ( v  =  <. w ,  g
>.  /\  ( g  e.  w  /\  <. w ,  g >.  e.  y ) ) )
2928exbii 1654 . . . . 5  |-  ( E. g E. t ( ( v  =  <. t ,  g >.  /\  (
t  e.  { w }  /\  g  e.  w
) )  /\  v  e.  y )  <->  E. g
( v  =  <. w ,  g >.  /\  (
g  e.  w  /\  <.
w ,  g >.  e.  y ) ) )
306, 29bitr3i 251 . . . 4  |-  ( ( E. g E. t
( v  =  <. t ,  g >.  /\  (
t  e.  { w }  /\  g  e.  w
) )  /\  v  e.  y )  <->  E. g
( v  =  <. w ,  g >.  /\  (
g  e.  w  /\  <.
w ,  g >.  e.  y ) ) )
311, 5, 303bitri 271 . . 3  |-  ( v  e.  ( ( { w }  X.  w
)  i^i  y )  <->  E. g ( v  = 
<. w ,  g >.  /\  ( g  e.  w  /\  <. w ,  g
>.  e.  y ) ) )
3231eubii 2292 . 2  |-  ( E! v  v  e.  ( ( { w }  X.  w )  i^i  y
)  <->  E! v E. g
( v  =  <. w ,  g >.  /\  (
g  e.  w  /\  <.
w ,  g >.  e.  y ) ) )
3321euop2 4737 . 2  |-  ( E! v E. g ( v  =  <. w ,  g >.  /\  (
g  e.  w  /\  <.
w ,  g >.  e.  y ) )  <->  E! g
( g  e.  w  /\  <. w ,  g
>.  e.  y ) )
3432, 33bitri 249 1  |-  ( E! v  v  e.  ( ( { w }  X.  w )  i^i  y
)  <->  E! g ( g  e.  w  /\  <. w ,  g >.  e.  y ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1383   E.wex 1599    e. wcel 1804   E!weu 2268    i^i cin 3460   {csn 4014   <.cop 4020    X. cxp 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-opab 4496  df-xp 4995
This theorem is referenced by:  dfac5lem5  8511
  Copyright terms: Public domain W3C validator