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

Theorem dfac5lem1 7750
Description: Lemma for dfac5 7755. (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 3358 . . . 4  |-  ( v  e.  ( ( { w }  X.  w
)  i^i  y )  <->  ( v  e.  ( { w }  X.  w
)  /\  v  e.  y ) )
2 elxp 4706 . . . . . 6  |-  ( v  e.  ( { w }  X.  w )  <->  E. t E. g ( v  = 
<. t ,  g >.  /\  ( t  e.  {
w }  /\  g  e.  w ) ) )
3 excom 1786 . . . . . 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 1843 . . . . 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 2343 . . . . . . . . . . 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 3655 . . . . . . . . . . 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 1569 . . . . . . 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 2791 . . . . . . . 8  |-  w  e. 
_V
22 opeq1 3796 . . . . . . . . . 10  |-  ( t  =  w  ->  <. t ,  g >.  =  <. w ,  g >. )
2322eqeq2d 2294 . . . . . . . . 9  |-  ( t  =  w  ->  (
v  =  <. t ,  g >.  <->  v  =  <. w ,  g >.
) )
2422eleq1d 2349 . . . . . . . . . 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 2823 . . . . . . 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 1569 . . . . 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 2152 . 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 4266 . 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 1528    = wceq 1623    e. wcel 1684   E!weu 2143    i^i cin 3151   {csn 3640   <.cop 3643    X. cxp 4687
This theorem is referenced by:  dfac5lem5  7754
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-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695
  Copyright terms: Public domain W3C validator