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

Theorem dfac5lem1 7766
Description: Lemma for dfac5 7771. (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 3371 . . . 4  |-  ( v  e.  ( ( { w }  X.  w
)  i^i  y )  <->  ( v  e.  ( { w }  X.  w
)  /\  v  e.  y ) )
2 elxp 4722 . . . . . 6  |-  ( v  e.  ( { w }  X.  w )  <->  E. t E. g ( v  = 
<. t ,  g >.  /\  ( t  e.  {
w }  /\  g  e.  w ) ) )
3 excom 1798 . . . . . 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 240 . . . . 5  |-  ( v  e.  ( { w }  X.  w )  <->  E. g E. t ( v  = 
<. t ,  g >.  /\  ( t  e.  {
w }  /\  g  e.  w ) ) )
54anbi1i 676 . . . 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 1855 . . . . 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 773 . . . . . . . . 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 2356 . . . . . . . . . . 11  |-  ( v  =  <. t ,  g
>.  ->  ( v  e.  y  <->  <. t ,  g
>.  e.  y ) )
98pm5.32i 618 . . . . . . . . . 10  |-  ( ( v  =  <. t ,  g >.  /\  v  e.  y )  <->  ( v  =  <. t ,  g
>.  /\  <. t ,  g
>.  e.  y ) )
10 elsn 3668 . . . . . . . . . . 11  |-  ( t  e.  { w }  <->  t  =  w )
1110anbi1i 676 . . . . . . . . . 10  |-  ( ( t  e.  { w }  /\  g  e.  w
)  <->  ( t  =  w  /\  g  e.  w ) )
129, 11anbi12i 678 . . . . . . . . 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 797 . . . . . . . . . 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 437 . . . . . . . . . . 11  |-  ( ( v  =  <. t ,  g >.  /\  t  =  w )  <->  ( t  =  w  /\  v  =  <. t ,  g
>. ) )
15 ancom 437 . . . . . . . . . . 11  |-  ( (
<. t ,  g >.  e.  y  /\  g  e.  w )  <->  ( g  e.  w  /\  <. t ,  g >.  e.  y ) )
1614, 15anbi12i 678 . . . . . . . . . 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 630 . . . . . . . . . 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 262 . . . . . . . . 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 262 . . . . . . . 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 1572 . . . . . . 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 2804 . . . . . . . 8  |-  w  e. 
_V
22 opeq1 3812 . . . . . . . . . 10  |-  ( t  =  w  ->  <. t ,  g >.  =  <. w ,  g >. )
2322eqeq2d 2307 . . . . . . . . 9  |-  ( t  =  w  ->  (
v  =  <. t ,  g >.  <->  v  =  <. w ,  g >.
) )
2422eleq1d 2362 . . . . . . . . . 10  |-  ( t  =  w  ->  ( <. t ,  g >.  e.  y  <->  <. w ,  g
>.  e.  y ) )
2524anbi2d 684 . . . . . . . . 9  |-  ( t  =  w  ->  (
( g  e.  w  /\  <. t ,  g
>.  e.  y )  <->  ( g  e.  w  /\  <. w ,  g >.  e.  y ) ) )
2623, 25anbi12d 691 . . . . . . . 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 2836 . . . . . . 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 240 . . . . . 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 1572 . . . . 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 242 . . . 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 262 . . 3  |-  ( v  e.  ( ( { w }  X.  w
)  i^i  y )  <->  E. g ( v  = 
<. w ,  g >.  /\  ( g  e.  w  /\  <. w ,  g
>.  e.  y ) ) )
3231eubii 2165 . 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 4282 . 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 240 1  |-  ( E! v  v  e.  ( ( { w }  X.  w )  i^i  y
)  <->  E! g ( g  e.  w  /\  <. w ,  g >.  e.  y ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1531    = wceq 1632    e. wcel 1696   E!weu 2156    i^i cin 3164   {csn 3653   <.cop 3656    X. cxp 4703
This theorem is referenced by:  dfac5lem5  7770
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-opab 4094  df-xp 4711
  Copyright terms: Public domain W3C validator