ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfplpq2 Unicode version

Theorem dfplpq2 7355
Description: Alternate definition of pre-addition on positive fractions. (Contributed by Jim Kingdon, 12-Sep-2019.)
Assertion
Ref Expression
dfplpq2  |-  +pQ  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
)  /\  E. w E. v E. u E. f ( ( x  =  <. w ,  v
>.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( v  .N  u ) ) ,  ( v  .N  f ) >. )
) }
Distinct variable group:    x, y, z, w, v, u, f

Proof of Theorem dfplpq2
StepHypRef Expression
1 df-mpo 5882 . 2  |-  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( ( 1st `  x )  .N  ( 2nd `  y
) )  +N  (
( 1st `  y
)  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
)  /\  z  =  <. ( ( ( 1st `  x )  .N  ( 2nd `  y ) )  +N  ( ( 1st `  y )  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y
) ) >. ) }
2 df-plpq 7345 . 2  |-  +pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N. 
X.  N. )  |->  <. (
( ( 1st `  x
)  .N  ( 2nd `  y ) )  +N  ( ( 1st `  y
)  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
3 1st2nd2 6178 . . . . . . . . . 10  |-  ( x  e.  ( N.  X.  N. )  ->  x  = 
<. ( 1st `  x
) ,  ( 2nd `  x ) >. )
43eqeq1d 2186 . . . . . . . . 9  |-  ( x  e.  ( N.  X.  N. )  ->  ( x  =  <. w ,  v
>. 
<-> 
<. ( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. w ,  v >. )
)
5 1st2nd2 6178 . . . . . . . . . 10  |-  ( y  e.  ( N.  X.  N. )  ->  y  = 
<. ( 1st `  y
) ,  ( 2nd `  y ) >. )
65eqeq1d 2186 . . . . . . . . 9  |-  ( y  e.  ( N.  X.  N. )  ->  ( y  =  <. u ,  f
>. 
<-> 
<. ( 1st `  y
) ,  ( 2nd `  y ) >.  =  <. u ,  f >. )
)
74, 6bi2anan9 606 . . . . . . . 8  |-  ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  ->  (
( x  =  <. w ,  v >.  /\  y  =  <. u ,  f
>. )  <->  ( <. ( 1st `  x ) ,  ( 2nd `  x
) >.  =  <. w ,  v >.  /\  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  =  <. u ,  f >. )
) )
87anbi1d 465 . . . . . . 7  |-  ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  ->  (
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( u  .N  v ) ) ,  ( v  .N  f ) >. )  <->  ( ( <. ( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. w ,  v >.  /\  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( u  .N  v ) ) ,  ( v  .N  f ) >. )
) )
9 xp1st 6168 . . . . . . . . . . . . . 14  |-  ( y  e.  ( N.  X.  N. )  ->  ( 1st `  y )  e.  N. )
109ad2antlr 489 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  ( 1st `  y )  e.  N. )
117biimpa 296 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  ( <. ( 1st `  x ) ,  ( 2nd `  x
) >.  =  <. w ,  v >.  /\  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  =  <. u ,  f >. )
)
1211simprd 114 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  <. ( 1st `  y ) ,  ( 2nd `  y )
>.  =  <. u ,  f >. )
13 vex 2742 . . . . . . . . . . . . . . . . 17  |-  u  e. 
_V
14 vex 2742 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
1513, 14opth2 4242 . . . . . . . . . . . . . . . 16  |-  ( <.
( 1st `  y
) ,  ( 2nd `  y ) >.  =  <. u ,  f >.  <->  ( ( 1st `  y )  =  u  /\  ( 2nd `  y )  =  f ) )
1615simplbi 274 . . . . . . . . . . . . . . 15  |-  ( <.
( 1st `  y
) ,  ( 2nd `  y ) >.  =  <. u ,  f >.  ->  ( 1st `  y )  =  u )
1716eleq1d 2246 . . . . . . . . . . . . . 14  |-  ( <.
( 1st `  y
) ,  ( 2nd `  y ) >.  =  <. u ,  f >.  ->  (
( 1st `  y
)  e.  N.  <->  u  e.  N. ) )
1812, 17syl 14 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  ( ( 1st `  y )  e. 
N. 
<->  u  e.  N. )
)
1910, 18mpbid 147 . . . . . . . . . . . 12  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  u  e.  N. )
20 xp2nd 6169 . . . . . . . . . . . . . 14  |-  ( x  e.  ( N.  X.  N. )  ->  ( 2nd `  x )  e.  N. )
2120ad2antrr 488 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  ( 2nd `  x )  e.  N. )
2211simpld 112 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  <. ( 1st `  x ) ,  ( 2nd `  x )
>.  =  <. w ,  v >. )
23 vex 2742 . . . . . . . . . . . . . . . . 17  |-  w  e. 
_V
24 vex 2742 . . . . . . . . . . . . . . . . 17  |-  v  e. 
_V
2523, 24opth2 4242 . . . . . . . . . . . . . . . 16  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. w ,  v >.  <->  ( ( 1st `  x )  =  w  /\  ( 2nd `  x )  =  v ) )
2625simprbi 275 . . . . . . . . . . . . . . 15  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. w ,  v >.  ->  ( 2nd `  x )  =  v )
2726eleq1d 2246 . . . . . . . . . . . . . 14  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. w ,  v >.  ->  (
( 2nd `  x
)  e.  N.  <->  v  e.  N. ) )
2822, 27syl 14 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  ( ( 2nd `  x )  e. 
N. 
<->  v  e.  N. )
)
2921, 28mpbid 147 . . . . . . . . . . . 12  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  v  e.  N. )
30 mulcompig 7332 . . . . . . . . . . . 12  |-  ( ( u  e.  N.  /\  v  e.  N. )  ->  ( u  .N  v
)  =  ( v  .N  u ) )
3119, 29, 30syl2anc 411 . . . . . . . . . . 11  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  ( u  .N  v )  =  ( v  .N  u ) )
3231oveq2d 5893 . . . . . . . . . 10  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  ( (
w  .N  f )  +N  ( u  .N  v ) )  =  ( ( w  .N  f )  +N  (
v  .N  u ) ) )
3332opeq1d 3786 . . . . . . . . 9  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  <. ( ( w  .N  f )  +N  ( u  .N  v ) ) ,  ( v  .N  f
) >.  =  <. (
( w  .N  f
)  +N  ( v  .N  u ) ) ,  ( v  .N  f ) >. )
3433eqeq2d 2189 . . . . . . . 8  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )
)  ->  ( z  =  <. ( ( w  .N  f )  +N  ( u  .N  v
) ) ,  ( v  .N  f )
>. 
<->  z  =  <. (
( w  .N  f
)  +N  ( v  .N  u ) ) ,  ( v  .N  f ) >. )
)
3534pm5.32da 452 . . . . . . 7  |-  ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  ->  (
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( u  .N  v ) ) ,  ( v  .N  f ) >. )  <->  ( ( x  =  <. w ,  v >.  /\  y  =  <. u ,  f
>. )  /\  z  =  <. ( ( w  .N  f )  +N  ( v  .N  u
) ) ,  ( v  .N  f )
>. ) ) )
368, 35bitr3d 190 . . . . . 6  |-  ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  ->  (
( ( <. ( 1st `  x ) ,  ( 2nd `  x
) >.  =  <. w ,  v >.  /\  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( u  .N  v ) ) ,  ( v  .N  f ) >. )  <->  ( ( x  =  <. w ,  v >.  /\  y  =  <. u ,  f
>. )  /\  z  =  <. ( ( w  .N  f )  +N  ( v  .N  u
) ) ,  ( v  .N  f )
>. ) ) )
37364exbidv 1870 . . . . 5  |-  ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  ->  ( E. w E. v E. u E. f ( ( <. ( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. w ,  v >.  /\  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( u  .N  v ) ) ,  ( v  .N  f ) >. )  <->  E. w E. v E. u E. f ( ( x  =  <. w ,  v >.  /\  y  =  <. u ,  f
>. )  /\  z  =  <. ( ( w  .N  f )  +N  ( v  .N  u
) ) ,  ( v  .N  f )
>. ) ) )
38 xp1st 6168 . . . . . . 7  |-  ( x  e.  ( N.  X.  N. )  ->  ( 1st `  x )  e.  N. )
3938, 20jca 306 . . . . . 6  |-  ( x  e.  ( N.  X.  N. )  ->  ( ( 1st `  x )  e.  N.  /\  ( 2nd `  x )  e. 
N. ) )
40 xp2nd 6169 . . . . . . 7  |-  ( y  e.  ( N.  X.  N. )  ->  ( 2nd `  y )  e.  N. )
419, 40jca 306 . . . . . 6  |-  ( y  e.  ( N.  X.  N. )  ->  ( ( 1st `  y )  e.  N.  /\  ( 2nd `  y )  e. 
N. ) )
42 simpll 527 . . . . . . . . . . 11  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  w  =  ( 1st `  x
) )
43 simprr 531 . . . . . . . . . . 11  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  f  =  ( 2nd `  y
) )
4442, 43oveq12d 5895 . . . . . . . . . 10  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  (
w  .N  f )  =  ( ( 1st `  x )  .N  ( 2nd `  y ) ) )
45 simprl 529 . . . . . . . . . . 11  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  u  =  ( 1st `  y
) )
46 simplr 528 . . . . . . . . . . 11  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  v  =  ( 2nd `  x
) )
4745, 46oveq12d 5895 . . . . . . . . . 10  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  (
u  .N  v )  =  ( ( 1st `  y )  .N  ( 2nd `  x ) ) )
4844, 47oveq12d 5895 . . . . . . . . 9  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  (
( w  .N  f
)  +N  ( u  .N  v ) )  =  ( ( ( 1st `  x )  .N  ( 2nd `  y
) )  +N  (
( 1st `  y
)  .N  ( 2nd `  x ) ) ) )
4946, 43oveq12d 5895 . . . . . . . . 9  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  (
v  .N  f )  =  ( ( 2nd `  x )  .N  ( 2nd `  y ) ) )
5048, 49opeq12d 3788 . . . . . . . 8  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  <. (
( w  .N  f
)  +N  ( u  .N  v ) ) ,  ( v  .N  f ) >.  =  <. ( ( ( 1st `  x
)  .N  ( 2nd `  y ) )  +N  ( ( 1st `  y
)  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
5150eqeq2d 2189 . . . . . . 7  |-  ( ( ( w  =  ( 1st `  x )  /\  v  =  ( 2nd `  x ) )  /\  ( u  =  ( 1st `  y
)  /\  f  =  ( 2nd `  y ) ) )  ->  (
z  =  <. (
( w  .N  f
)  +N  ( u  .N  v ) ) ,  ( v  .N  f ) >.  <->  z  =  <. ( ( ( 1st `  x )  .N  ( 2nd `  y ) )  +N  ( ( 1st `  y )  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y
) ) >. )
)
5251copsex4g 4249 . . . . . 6  |-  ( ( ( ( 1st `  x
)  e.  N.  /\  ( 2nd `  x )  e.  N. )  /\  ( ( 1st `  y
)  e.  N.  /\  ( 2nd `  y )  e.  N. ) )  ->  ( E. w E. v E. u E. f ( ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. w ,  v >.  /\  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( u  .N  v ) ) ,  ( v  .N  f ) >. )  <->  z  =  <. ( ( ( 1st `  x )  .N  ( 2nd `  y
) )  +N  (
( 1st `  y
)  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. ) )
5339, 41, 52syl2an 289 . . . . 5  |-  ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  ->  ( E. w E. v E. u E. f ( ( <. ( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. w ,  v >.  /\  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( u  .N  v ) ) ,  ( v  .N  f ) >. )  <->  z  =  <. ( ( ( 1st `  x )  .N  ( 2nd `  y
) )  +N  (
( 1st `  y
)  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. ) )
5437, 53bitr3d 190 . . . 4  |-  ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  ->  ( E. w E. v E. u E. f ( ( x  =  <. w ,  v >.  /\  y  =  <. u ,  f
>. )  /\  z  =  <. ( ( w  .N  f )  +N  ( v  .N  u
) ) ,  ( v  .N  f )
>. )  <->  z  =  <. ( ( ( 1st `  x
)  .N  ( 2nd `  y ) )  +N  ( ( 1st `  y
)  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. ) )
5554pm5.32i 454 . . 3  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. w E. v E. u E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( v  .N  u ) ) ,  ( v  .N  f ) >. )
)  <->  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  z  =  <. ( ( ( 1st `  x )  .N  ( 2nd `  y
) )  +N  (
( 1st `  y
)  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. ) )
5655oprabbii 5932 . 2  |-  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. w E. v E. u E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( v  .N  u ) ) ,  ( v  .N  f ) >. )
) }  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
)  /\  z  =  <. ( ( ( 1st `  x )  .N  ( 2nd `  y ) )  +N  ( ( 1st `  y )  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y
) ) >. ) }
571, 2, 563eqtr4i 2208 1  |-  +pQ  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
)  /\  E. w E. v E. u E. f ( ( x  =  <. w ,  v
>.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .N  f
)  +N  ( v  .N  u ) ) ,  ( v  .N  f ) >. )
) }
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105    = wceq 1353   E.wex 1492    e. wcel 2148   <.cop 3597    X. cxp 4626   ` cfv 5218  (class class class)co 5877   {coprab 5878    e. cmpo 5879   1stc1st 6141   2ndc2nd 6142   N.cnpi 7273    +N cpli 7274    .N cmi 7275    +pQ cplpq 7277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-recs 6308  df-irdg 6373  df-oadd 6423  df-omul 6424  df-ni 7305  df-mi 7307  df-plpq 7345
This theorem is referenced by:  addpipqqs  7371
  Copyright terms: Public domain W3C validator