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

Theorem dfac5lem1 8495
Description: Lemma for dfac5 8500. (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 3673 . . . 4  |-  ( v  e.  ( ( { w }  X.  w
)  i^i  y )  <->  ( v  e.  ( { w }  X.  w
)  /\  v  e.  y ) )
2 elxp 5005 . . . . . 6  |-  ( v  e.  ( { w }  X.  w )  <->  E. t E. g ( v  = 
<. t ,  g >.  /\  ( t  e.  {
w }  /\  g  e.  w ) ) )
3 excom 1854 . . . . . 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 693 . . . 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 1777 . . . . 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 2526 . . . . . . . . . . 11  |-  ( v  =  <. t ,  g
>.  ->  ( v  e.  y  <->  <. t ,  g
>.  e.  y ) )
98pm5.32i 635 . . . . . . . . . 10  |-  ( ( v  =  <. t ,  g >.  /\  v  e.  y )  <->  ( v  =  <. t ,  g
>.  /\  <. t ,  g
>.  e.  y ) )
10 elsn 4030 . . . . . . . . . . 11  |-  ( t  e.  { w }  <->  t  =  w )
1110anbi1i 693 . . . . . . . . . 10  |-  ( ( t  e.  { w }  /\  g  e.  w
)  <->  ( t  =  w  /\  g  e.  w ) )
129, 11anbi12i 695 . . . . . . . . 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 822 . . . . . . . . . 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 448 . . . . . . . . . . 11  |-  ( ( v  =  <. t ,  g >.  /\  t  =  w )  <->  ( t  =  w  /\  v  =  <. t ,  g
>. ) )
15 ancom 448 . . . . . . . . . . 11  |-  ( (
<. t ,  g >.  e.  y  /\  g  e.  w )  <->  ( g  e.  w  /\  <. t ,  g >.  e.  y ) )
1614, 15anbi12i 695 . . . . . . . . . 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 647 . . . . . . . . . 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 1672 . . . . . . 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 3109 . . . . . . . 8  |-  w  e. 
_V
22 opeq1 4203 . . . . . . . . . 10  |-  ( t  =  w  ->  <. t ,  g >.  =  <. w ,  g >. )
2322eqeq2d 2468 . . . . . . . . 9  |-  ( t  =  w  ->  (
v  =  <. t ,  g >.  <->  v  =  <. w ,  g >.
) )
2422eleq1d 2523 . . . . . . . . . 10  |-  ( t  =  w  ->  ( <. t ,  g >.  e.  y  <->  <. w ,  g
>.  e.  y ) )
2524anbi2d 701 . . . . . . . . 9  |-  ( t  =  w  ->  (
( g  e.  w  /\  <. t ,  g
>.  e.  y )  <->  ( g  e.  w  /\  <. w ,  g >.  e.  y ) ) )
2623, 25anbi12d 708 . . . . . . . 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 3143 . . . . . . 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 1672 . . . . 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 2308 . 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 4736 . 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 367    = wceq 1398   E.wex 1617    e. wcel 1823   E!weu 2284    i^i cin 3460   {csn 4016   <.cop 4022    X. cxp 4986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-opab 4498  df-xp 4994
This theorem is referenced by:  dfac5lem5  8499
  Copyright terms: Public domain W3C validator