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

Theorem findcard2s 6784
Description: Variation of findcard2 6783 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 6655 . . 3  |-  ( x  e.  Fin  <->  E. w  e.  om  x  ~~  w
)
3 breq2 3933 . . . . . . . 8  |-  ( w  =  (/)  ->  ( x 
~~  w  <->  x  ~~  (/) ) )
43imbi1d 230 . . . . . . 7  |-  ( w  =  (/)  ->  ( ( x  ~~  w  ->  ph )  <->  ( x  ~~  (/) 
->  ph ) ) )
54albidv 1796 . . . . . 6  |-  ( w  =  (/)  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  (/)  ->  ph )
) )
6 breq2 3933 . . . . . . . 8  |-  ( w  =  v  ->  (
x  ~~  w  <->  x  ~~  v ) )
76imbi1d 230 . . . . . . 7  |-  ( w  =  v  ->  (
( x  ~~  w  ->  ph )  <->  ( x  ~~  v  ->  ph )
) )
87albidv 1796 . . . . . 6  |-  ( w  =  v  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  v  ->  ph ) ) )
9 breq2 3933 . . . . . . . 8  |-  ( w  =  suc  v  -> 
( x  ~~  w  <->  x 
~~  suc  v )
)
109imbi1d 230 . . . . . . 7  |-  ( w  =  suc  v  -> 
( ( x  ~~  w  ->  ph )  <->  ( x  ~~  suc  v  ->  ph )
) )
1110albidv 1796 . . . . . 6  |-  ( w  =  suc  v  -> 
( A. x ( x  ~~  w  ->  ph )  <->  A. x ( x 
~~  suc  v  ->  ph ) ) )
12 en0 6689 . . . . . . . 8  |-  ( x 
~~  (/)  <->  x  =  (/) )
13 findcard2s.5 . . . . . . . . 9  |-  ps
14 findcard2s.1 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
1513, 14mpbiri 167 . . . . . . . 8  |-  ( x  =  (/)  ->  ph )
1612, 15sylbi 120 . . . . . . 7  |-  ( x 
~~  (/)  ->  ph )
1716ax-gen 1425 . . . . . 6  |-  A. x
( x  ~~  (/)  ->  ph )
18 peano3 4510 . . . . . . . . . . . . 13  |-  ( v  e.  om  ->  suc  v  =/=  (/) )
1918adantr 274 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =/=  (/) )
20 breq1 3932 . . . . . . . . . . . . . . . 16  |-  ( w  =  (/)  ->  ( w 
~~  suc  v  <->  (/)  ~~  suc  v ) )
2120anbi2d 459 . . . . . . . . . . . . . . 15  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  <-> 
( v  e.  om  /\  (/)  ~~  suc  v ) ) )
22 peano1 4508 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  om
23 peano2 4509 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  om  ->  suc  v  e.  om )
24 nneneq 6751 . . . . . . . . . . . . . . . . . 18  |-  ( (
(/)  e.  om  /\  suc  v  e.  om )  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2522, 23, 24sylancr 410 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  om  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2625biimpa 294 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  (/)  =  suc  v )
2726eqcomd 2145 . . . . . . . . . . . . . . 15  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  suc  v  =  (/) )
2821, 27syl6bi 162 . . . . . . . . . . . . . 14  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =  (/) ) )
2928com12 30 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =  (/)  ->  suc  v  =  (/) ) )
3029necon3d 2352 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( suc  v  =/=  (/)  ->  w  =/=  (/) ) )
3119, 30mpd 13 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  w  =/=  (/) )
3231ex 114 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
w  ~~  suc  v  ->  w  =/=  (/) ) )
33 nnfi 6766 . . . . . . . . . . . . . . . 16  |-  ( suc  v  e.  om  ->  suc  v  e.  Fin )
3423, 33syl 14 . . . . . . . . . . . . . . 15  |-  ( v  e.  om  ->  suc  v  e.  Fin )
3534adantr 274 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  e.  Fin )
36 enfi 6767 . . . . . . . . . . . . . . 15  |-  ( w 
~~  suc  v  ->  ( w  e.  Fin  <->  suc  v  e. 
Fin ) )
3736adantl 275 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  e. 
Fin 
<->  suc  v  e.  Fin ) )
3835, 37mpbird 166 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  w  e.  Fin )
39 fin0 6779 . . . . . . . . . . . . 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 518 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  v  e.  om )
42 dif1en 6773 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  w  ~~  suc  v  /\  z  e.  w )  ->  ( w  \  {
z } )  ~~  v )
43423expa 1181 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
w  \  { z } )  ~~  v
)
44 fidifsnid 6765 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e.  Fin  /\  z  e.  w )  ->  ( ( w  \  { z } )  u.  { z } )  =  w )
4538, 44sylan 281 . . . . . . . . . . . . . . . 16  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
( w  \  {
z } )  u. 
{ z } )  =  w )
46 neldifsn 3653 . . . . . . . . . . . . . . . . . 18  |-  -.  z  e.  ( w  \  {
z } )
47 vex 2689 . . . . . . . . . . . . . . . . . . . 20  |-  w  e. 
_V
48 difexg 4069 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  _V  ->  (
w  \  { z } )  e.  _V )
4947, 48ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( w 
\  { z } )  e.  _V
50 breq1 3932 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( y  ~~  v 
<->  ( w  \  {
z } )  ~~  v ) )
5150anbi2d 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( ( v  e.  om  /\  y  ~~  v )  <->  ( v  e.  om  /\  ( w 
\  { z } )  ~~  v ) ) )
52 eleq2 2203 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( z  e.  y  <->  z  e.  ( w  \  { z } ) ) )
5352notbid 656 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( -.  z  e.  y  <->  -.  z  e.  ( w  \  { z } ) ) )
5451, 53anbi12d 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( w  \  { z } )  ->  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y
)  <->  ( ( v  e.  om  /\  (
w  \  { z } )  ~~  v
)  /\  -.  z  e.  ( w  \  {
z } ) ) ) )
55 uneq1 3223 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( y  u. 
{ z } )  =  ( ( w 
\  { z } )  u.  { z } ) )
5655sbceq1d 2914 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( [. (
y  u.  { z } )  /  x ]. ph  <->  [. ( ( w 
\  { z } )  u.  { z } )  /  x ]. ph ) )
5756imbi2d 229 . . . . . . . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . . . . . . . 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 3932 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x  ~~  v  <->  y  ~~  v ) )
60 findcard2s.2 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
6159, 60imbi12d 233 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( x  ~~  v  ->  ph )  <->  ( y  ~~  v  ->  ch )
) )
6261spv 1832 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. x ( x  ~~  v  ->  ph )  ->  (
y  ~~  v  ->  ch ) )
63 pm2.27 40 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y 
~~  v  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
6463adantl 275 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( ( y  ~~  v  ->  ch )  ->  ch ) )
6564adantr 274 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
66 rspe 2481 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  om  /\  y  ~~  v )  ->  E. v  e.  om  y  ~~  v )
67 isfi 6655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  Fin  <->  E. v  e.  om  y  ~~  v
)
6866, 67sylibr 133 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
y  e.  Fin )
69 findcard2s.6 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  Fin  /\  -.  z  e.  y
)  ->  ( ch  ->  th ) )
7068, 69sylan 281 . . . . . . . . . . . . . . . . . . . . . 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 2689 . . . . . . . . . . . . . . . . . . . . . 22  |-  y  e. 
_V
74 vex 2689 . . . . . . . . . . . . . . . . . . . . . . 23  |-  z  e. 
_V
7574snex 4109 . . . . . . . . . . . . . . . . . . . . . 22  |-  { z }  e.  _V
7673, 75unex 4362 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  u.  { z } )  e.  _V
77 findcard2s.3 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
7876, 77sbcie 2943 . . . . . . . . . . . . . . . . . . . 20  |-  ( [. ( y  u.  {
z } )  /  x ]. ph  <->  th )
7972, 78syl6ibr 161 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph ) )
8049, 58, 79vtocl 2740 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  /\  -.  z  e.  ( w  \  { z } ) )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
8146, 80mpan2 421 . . . . . . . . . . . . . . . . 17  |-  ( ( v  e.  om  /\  ( w  \  { z } )  ~~  v
)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
82 dfsbcq 2911 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  ( [. ( ( w  \  { z } )  u.  { z } )  /  x ]. ph  <->  [. w  /  x ]. ph ) )
8382imbi2d 229 . . . . . . . . . . . . . . . . 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, 83syl5ib 153 . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . 14  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
)
8786ex 114 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( z  e.  w  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8887exlimdv 1791 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( E. z 
z  e.  w  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8940, 88sylbid 149 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =/=  (/)  ->  ( A. x
( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
9089ex 114 . . . . . . . . . 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 1848 . . . . . . 7  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. w
( w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
94 nfv 1508 . . . . . . . 8  |-  F/ w
( x  ~~  suc  v  ->  ph )
95 nfv 1508 . . . . . . . . 9  |-  F/ x  w  ~~  suc  v
96 nfsbc1v 2927 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
9795, 96nfim 1551 . . . . . . . 8  |-  F/ x
( w  ~~  suc  v  ->  [. w  /  x ]. ph )
98 breq1 3932 . . . . . . . . 9  |-  ( x  =  w  ->  (
x  ~~  suc  v  <->  w  ~~  suc  v ) )
99 sbceq1a 2918 . . . . . . . . 9  |-  ( x  =  w  ->  ( ph 
<-> 
[. w  /  x ]. ph ) )
10098, 99imbi12d 233 . . . . . . . 8  |-  ( x  =  w  ->  (
( x  ~~  suc  v  ->  ph )  <->  ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
) )
10194, 97, 100cbval 1727 . . . . . . 7  |-  ( A. x ( x  ~~  suc  v  ->  ph )  <->  A. w ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
)
10293, 101syl6ibr 161 . . . . . 6  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. x
( x  ~~  suc  v  ->  ph ) ) )
1035, 8, 11, 17, 102finds1 4516 . . . . 5  |-  ( w  e.  om  ->  A. x
( x  ~~  w  ->  ph ) )
10410319.21bi 1537 . . . 4  |-  ( w  e.  om  ->  (
x  ~~  w  ->  ph ) )
105104rexlimiv 2543 . . 3  |-  ( E. w  e.  om  x  ~~  w  ->  ph )
1062, 105sylbi 120 . 2  |-  ( x  e.  Fin  ->  ph )
1071, 106vtoclga 2752 1  |-  ( A  e.  Fin  ->  ta )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104   A.wal 1329    = wceq 1331   E.wex 1468    e. wcel 1480    =/= wne 2308   E.wrex 2417   _Vcvv 2686   [.wsbc 2909    \ cdif 3068    u. cun 3069   (/)c0 3363   {csn 3527   class class class wbr 3929   suc csuc 4287   omcom 4504    ~~ cen 6632   Fincfn 6634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-er 6429  df-en 6635  df-fin 6637
This theorem is referenced by:  findcard2d  6785  findcard2sd  6786  diffifi  6788  ac6sfi  6792  fisseneq  6820  fsum2d  11216  modfsummod  11239  fsumabs  11246  fsumiun  11258
  Copyright terms: Public domain W3C validator