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

Theorem dfac5lem1 8291
Description: Lemma for dfac5 8296. (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 3537 . . . 4  |-  ( v  e.  ( ( { w }  X.  w
)  i^i  y )  <->  ( v  e.  ( { w }  X.  w
)  /\  v  e.  y ) )
2 elxp 4855 . . . . . 6  |-  ( v  e.  ( { w }  X.  w )  <->  E. t E. g ( v  = 
<. t ,  g >.  /\  ( t  e.  {
w }  /\  g  e.  w ) ) )
3 excom 1787 . . . . . 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 1921 . . . . 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 796 . . . . . . . . 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 2501 . . . . . . . . . . 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 3889 . . . . . . . . . . 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 820 . . . . . . . . . 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 1634 . . . . . . 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 2973 . . . . . . . 8  |-  w  e. 
_V
22 opeq1 4057 . . . . . . . . . 10  |-  ( t  =  w  ->  <. t ,  g >.  =  <. w ,  g >. )
2322eqeq2d 2452 . . . . . . . . 9  |-  ( t  =  w  ->  (
v  =  <. t ,  g >.  <->  v  =  <. w ,  g >.
) )
2422eleq1d 2507 . . . . . . . . . 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 3007 . . . . . . 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 1634 . . . . 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 2278 . 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 4589 . 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 1369   E.wex 1586    e. wcel 1756   E!weu 2253    i^i cin 3325   {csn 3875   <.cop 3881    X. cxp 4836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pr 4529
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-rab 2722  df-v 2972  df-sbc 3185  df-csb 3287  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-opab 4349  df-xp 4844
This theorem is referenced by:  dfac5lem5  8295
  Copyright terms: Public domain W3C validator