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

Theorem findcard2s 6884
Description: Variation of findcard2 6883 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.)
Hypotheses
Ref Expression
findcard2s.1  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
findcard2s.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
findcard2s.3  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
findcard2s.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
findcard2s.5  |-  ps
findcard2s.6  |-  ( ( y  e.  Fin  /\  -.  z  e.  y
)  ->  ( ch  ->  th ) )
Assertion
Ref Expression
findcard2s  |-  ( A  e.  Fin  ->  ta )
Distinct variable groups:    x, A, y, z    ch, x    ph, y, z    ps, x    ta, x    th, x
Allowed substitution hints:    ph( x)    ps( y,
z)    ch( y, z)    th( y,
z)    ta( y, z)

Proof of Theorem findcard2s
Dummy variables  v  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 findcard2s.4 . 2  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2 isfi 6755 . . 3  |-  ( x  e.  Fin  <->  E. w  e.  om  x  ~~  w
)
3 breq2 4004 . . . . . . . 8  |-  ( w  =  (/)  ->  ( x 
~~  w  <->  x  ~~  (/) ) )
43imbi1d 231 . . . . . . 7  |-  ( w  =  (/)  ->  ( ( x  ~~  w  ->  ph )  <->  ( x  ~~  (/) 
->  ph ) ) )
54albidv 1824 . . . . . 6  |-  ( w  =  (/)  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  (/)  ->  ph )
) )
6 breq2 4004 . . . . . . . 8  |-  ( w  =  v  ->  (
x  ~~  w  <->  x  ~~  v ) )
76imbi1d 231 . . . . . . 7  |-  ( w  =  v  ->  (
( x  ~~  w  ->  ph )  <->  ( x  ~~  v  ->  ph )
) )
87albidv 1824 . . . . . 6  |-  ( w  =  v  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  v  ->  ph ) ) )
9 breq2 4004 . . . . . . . 8  |-  ( w  =  suc  v  -> 
( x  ~~  w  <->  x 
~~  suc  v )
)
109imbi1d 231 . . . . . . 7  |-  ( w  =  suc  v  -> 
( ( x  ~~  w  ->  ph )  <->  ( x  ~~  suc  v  ->  ph )
) )
1110albidv 1824 . . . . . 6  |-  ( w  =  suc  v  -> 
( A. x ( x  ~~  w  ->  ph )  <->  A. x ( x 
~~  suc  v  ->  ph ) ) )
12 en0 6789 . . . . . . . 8  |-  ( x 
~~  (/)  <->  x  =  (/) )
13 findcard2s.5 . . . . . . . . 9  |-  ps
14 findcard2s.1 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
1513, 14mpbiri 168 . . . . . . . 8  |-  ( x  =  (/)  ->  ph )
1612, 15sylbi 121 . . . . . . 7  |-  ( x 
~~  (/)  ->  ph )
1716ax-gen 1449 . . . . . 6  |-  A. x
( x  ~~  (/)  ->  ph )
18 peano3 4592 . . . . . . . . . . . . 13  |-  ( v  e.  om  ->  suc  v  =/=  (/) )
1918adantr 276 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =/=  (/) )
20 breq1 4003 . . . . . . . . . . . . . . . 16  |-  ( w  =  (/)  ->  ( w 
~~  suc  v  <->  (/)  ~~  suc  v ) )
2120anbi2d 464 . . . . . . . . . . . . . . 15  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  <-> 
( v  e.  om  /\  (/)  ~~  suc  v ) ) )
22 peano1 4590 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  om
23 peano2 4591 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  om  ->  suc  v  e.  om )
24 nneneq 6851 . . . . . . . . . . . . . . . . . 18  |-  ( (
(/)  e.  om  /\  suc  v  e.  om )  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2522, 23, 24sylancr 414 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  om  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2625biimpa 296 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  (/)  =  suc  v )
2726eqcomd 2183 . . . . . . . . . . . . . . 15  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  suc  v  =  (/) )
2821, 27syl6bi 163 . . . . . . . . . . . . . 14  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =  (/) ) )
2928com12 30 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =  (/)  ->  suc  v  =  (/) ) )
3029necon3d 2391 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( suc  v  =/=  (/)  ->  w  =/=  (/) ) )
3119, 30mpd 13 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  w  =/=  (/) )
3231ex 115 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
w  ~~  suc  v  ->  w  =/=  (/) ) )
33 nnfi 6866 . . . . . . . . . . . . . . . 16  |-  ( suc  v  e.  om  ->  suc  v  e.  Fin )
3423, 33syl 14 . . . . . . . . . . . . . . 15  |-  ( v  e.  om  ->  suc  v  e.  Fin )
3534adantr 276 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  e.  Fin )
36 enfi 6867 . . . . . . . . . . . . . . 15  |-  ( w 
~~  suc  v  ->  ( w  e.  Fin  <->  suc  v  e. 
Fin ) )
3736adantl 277 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  e. 
Fin 
<->  suc  v  e.  Fin ) )
3835, 37mpbird 167 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  w  e.  Fin )
39 fin0 6879 . . . . . . . . . . . . 13  |-  ( w  e.  Fin  ->  (
w  =/=  (/)  <->  E. z 
z  e.  w ) )
4038, 39syl 14 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =/=  (/) 
<->  E. z  z  e.  w ) )
41 simpll 527 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  v  e.  om )
42 dif1en 6873 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  w  ~~  suc  v  /\  z  e.  w )  ->  ( w  \  {
z } )  ~~  v )
43423expa 1203 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
w  \  { z } )  ~~  v
)
44 fidifsnid 6865 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e.  Fin  /\  z  e.  w )  ->  ( ( w  \  { z } )  u.  { z } )  =  w )
4538, 44sylan 283 . . . . . . . . . . . . . . . 16  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
( w  \  {
z } )  u. 
{ z } )  =  w )
46 neldifsn 3721 . . . . . . . . . . . . . . . . . 18  |-  -.  z  e.  ( w  \  {
z } )
47 vex 2740 . . . . . . . . . . . . . . . . . . . 20  |-  w  e. 
_V
48 difexg 4141 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  _V  ->  (
w  \  { z } )  e.  _V )
4947, 48ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( w 
\  { z } )  e.  _V
50 breq1 4003 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( y  ~~  v 
<->  ( w  \  {
z } )  ~~  v ) )
5150anbi2d 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( ( v  e.  om  /\  y  ~~  v )  <->  ( v  e.  om  /\  ( w 
\  { z } )  ~~  v ) ) )
52 eleq2 2241 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( z  e.  y  <->  z  e.  ( w  \  { z } ) ) )
5352notbid 667 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( -.  z  e.  y  <->  -.  z  e.  ( w  \  { z } ) ) )
5451, 53anbi12d 473 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( w  \  { z } )  ->  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y
)  <->  ( ( v  e.  om  /\  (
w  \  { z } )  ~~  v
)  /\  -.  z  e.  ( w  \  {
z } ) ) ) )
55 uneq1 3282 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( y  u. 
{ z } )  =  ( ( w 
\  { z } )  u.  { z } ) )
5655sbceq1d 2967 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( [. (
y  u.  { z } )  /  x ]. ph  <->  [. ( ( w 
\  { z } )  u.  { z } )  /  x ]. ph ) )
5756imbi2d 230 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( w  \  { z } )  ->  ( ( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph )  <->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
) )
5854, 57imbi12d 234 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( w  \  { z } )  ->  ( ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph ) )  <->  ( (
( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  /\  -.  z  e.  ( w  \  { z } ) )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
) ) )
59 breq1 4003 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x  ~~  v  <->  y  ~~  v ) )
60 findcard2s.2 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
6159, 60imbi12d 234 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( x  ~~  v  ->  ph )  <->  ( y  ~~  v  ->  ch )
) )
6261spv 1860 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. x ( x  ~~  v  ->  ph )  ->  (
y  ~~  v  ->  ch ) )
63 pm2.27 40 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y 
~~  v  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
6463adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( ( y  ~~  v  ->  ch )  ->  ch ) )
6564adantr 276 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
66 rspe 2526 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  om  /\  y  ~~  v )  ->  E. v  e.  om  y  ~~  v )
67 isfi 6755 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  Fin  <->  E. v  e.  om  y  ~~  v
)
6866, 67sylibr 134 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
y  e.  Fin )
69 findcard2s.6 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  Fin  /\  -.  z  e.  y
)  ->  ( ch  ->  th ) )
7068, 69sylan 283 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  ( ch  ->  th ) )
7165, 70syld 45 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  (
( y  ~~  v  ->  ch )  ->  th )
)
7262, 71syl5 32 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  th )
)
73 vex 2740 . . . . . . . . . . . . . . . . . . . . . 22  |-  y  e. 
_V
74 vex 2740 . . . . . . . . . . . . . . . . . . . . . . 23  |-  z  e. 
_V
7574snex 4182 . . . . . . . . . . . . . . . . . . . . . 22  |-  { z }  e.  _V
7673, 75unex 4438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  u.  { z } )  e.  _V
77 findcard2s.3 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
7876, 77sbcie 2997 . . . . . . . . . . . . . . . . . . . 20  |-  ( [. ( y  u.  {
z } )  /  x ]. ph  <->  th )
7972, 78syl6ibr 162 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph ) )
8049, 58, 79vtocl 2791 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  /\  -.  z  e.  ( w  \  { z } ) )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
8146, 80mpan2 425 . . . . . . . . . . . . . . . . 17  |-  ( ( v  e.  om  /\  ( w  \  { z } )  ~~  v
)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
82 dfsbcq 2964 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  ( [. ( ( w  \  { z } )  u.  { z } )  /  x ]. ph  <->  [. w  /  x ]. ph ) )
8382imbi2d 230 . . . . . . . . . . . . . . . . 17  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  (
( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )  <->  ( A. x ( x 
~~  v  ->  ph )  ->  [. w  /  x ]. ph ) ) )
8481, 83imbitrid 154 . . . . . . . . . . . . . . . 16  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  (
( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8545, 84syl 14 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8641, 43, 85mp2and 433 . . . . . . . . . . . . . 14  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
)
8786ex 115 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( z  e.  w  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8887exlimdv 1819 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( E. z 
z  e.  w  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8940, 88sylbid 150 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =/=  (/)  ->  ( A. x
( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
9089ex 115 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
w  ~~  suc  v  -> 
( w  =/=  (/)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) ) )
9132, 90mpdd 41 . . . . . . . . 9  |-  ( v  e.  om  ->  (
w  ~~  suc  v  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
9291com23 78 . . . . . . . 8  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  (
w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
9392alrimdv 1876 . . . . . . 7  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. w
( w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
94 nfv 1528 . . . . . . . 8  |-  F/ w
( x  ~~  suc  v  ->  ph )
95 nfv 1528 . . . . . . . . 9  |-  F/ x  w  ~~  suc  v
96 nfsbc1v 2981 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
9795, 96nfim 1572 . . . . . . . 8  |-  F/ x
( w  ~~  suc  v  ->  [. w  /  x ]. ph )
98 breq1 4003 . . . . . . . . 9  |-  ( x  =  w  ->  (
x  ~~  suc  v  <->  w  ~~  suc  v ) )
99 sbceq1a 2972 . . . . . . . . 9  |-  ( x  =  w  ->  ( ph 
<-> 
[. w  /  x ]. ph ) )
10098, 99imbi12d 234 . . . . . . . 8  |-  ( x  =  w  ->  (
( x  ~~  suc  v  ->  ph )  <->  ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
) )
10194, 97, 100cbval 1754 . . . . . . 7  |-  ( A. x ( x  ~~  suc  v  ->  ph )  <->  A. w ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
)
10293, 101syl6ibr 162 . . . . . 6  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. x
( x  ~~  suc  v  ->  ph ) ) )
1035, 8, 11, 17, 102finds1 4598 . . . . 5  |-  ( w  e.  om  ->  A. x
( x  ~~  w  ->  ph ) )
10410319.21bi 1558 . . . 4  |-  ( w  e.  om  ->  (
x  ~~  w  ->  ph ) )
105104rexlimiv 2588 . . 3  |-  ( E. w  e.  om  x  ~~  w  ->  ph )
1062, 105sylbi 121 . 2  |-  ( x  e.  Fin  ->  ph )
1071, 106vtoclga 2803 1  |-  ( A  e.  Fin  ->  ta )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105   A.wal 1351    = wceq 1353   E.wex 1492    e. wcel 2148    =/= wne 2347   E.wrex 2456   _Vcvv 2737   [.wsbc 2962    \ cdif 3126    u. cun 3127   (/)c0 3422   {csn 3591   class class class wbr 4000   suc csuc 4362   omcom 4586    ~~ cen 6732   Fincfn 6734
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 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  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 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-er 6529  df-en 6735  df-fin 6737
This theorem is referenced by:  findcard2d  6885  findcard2sd  6886  diffifi  6888  ac6sfi  6892  fisseneq  6925  fsum2d  11427  modfsummod  11450  fsumabs  11457  fsumiun  11469  fprod2d  11615
  Copyright terms: Public domain W3C validator