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

Theorem findcard2s 6446
Description: Variation of findcard2 6445 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 6329 . . 3  |-  ( x  e.  Fin  <->  E. w  e.  om  x  ~~  w
)
3 breq2 3809 . . . . . . . 8  |-  ( w  =  (/)  ->  ( x 
~~  w  <->  x  ~~  (/) ) )
43imbi1d 229 . . . . . . 7  |-  ( w  =  (/)  ->  ( ( x  ~~  w  ->  ph )  <->  ( x  ~~  (/) 
->  ph ) ) )
54albidv 1747 . . . . . 6  |-  ( w  =  (/)  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  (/)  ->  ph )
) )
6 breq2 3809 . . . . . . . 8  |-  ( w  =  v  ->  (
x  ~~  w  <->  x  ~~  v ) )
76imbi1d 229 . . . . . . 7  |-  ( w  =  v  ->  (
( x  ~~  w  ->  ph )  <->  ( x  ~~  v  ->  ph )
) )
87albidv 1747 . . . . . 6  |-  ( w  =  v  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  v  ->  ph ) ) )
9 breq2 3809 . . . . . . . 8  |-  ( w  =  suc  v  -> 
( x  ~~  w  <->  x 
~~  suc  v )
)
109imbi1d 229 . . . . . . 7  |-  ( w  =  suc  v  -> 
( ( x  ~~  w  ->  ph )  <->  ( x  ~~  suc  v  ->  ph )
) )
1110albidv 1747 . . . . . 6  |-  ( w  =  suc  v  -> 
( A. x ( x  ~~  w  ->  ph )  <->  A. x ( x 
~~  suc  v  ->  ph ) ) )
12 en0 6363 . . . . . . . 8  |-  ( x 
~~  (/)  <->  x  =  (/) )
13 findcard2s.5 . . . . . . . . 9  |-  ps
14 findcard2s.1 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
1513, 14mpbiri 166 . . . . . . . 8  |-  ( x  =  (/)  ->  ph )
1612, 15sylbi 119 . . . . . . 7  |-  ( x 
~~  (/)  ->  ph )
1716ax-gen 1379 . . . . . 6  |-  A. x
( x  ~~  (/)  ->  ph )
18 peano3 4365 . . . . . . . . . . . . 13  |-  ( v  e.  om  ->  suc  v  =/=  (/) )
1918adantr 270 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =/=  (/) )
20 breq1 3808 . . . . . . . . . . . . . . . 16  |-  ( w  =  (/)  ->  ( w 
~~  suc  v  <->  (/)  ~~  suc  v ) )
2120anbi2d 452 . . . . . . . . . . . . . . 15  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  <-> 
( v  e.  om  /\  (/)  ~~  suc  v ) ) )
22 peano1 4363 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  om
23 peano2 4364 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  om  ->  suc  v  e.  om )
24 nneneq 6413 . . . . . . . . . . . . . . . . . 18  |-  ( (
(/)  e.  om  /\  suc  v  e.  om )  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2522, 23, 24sylancr 405 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  om  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2625biimpa 290 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  (/)  =  suc  v )
2726eqcomd 2088 . . . . . . . . . . . . . . 15  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  suc  v  =  (/) )
2821, 27syl6bi 161 . . . . . . . . . . . . . 14  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =  (/) ) )
2928com12 30 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =  (/)  ->  suc  v  =  (/) ) )
3029necon3d 2293 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( suc  v  =/=  (/)  ->  w  =/=  (/) ) )
3119, 30mpd 13 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  w  =/=  (/) )
3231ex 113 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
w  ~~  suc  v  ->  w  =/=  (/) ) )
33 nnfi 6428 . . . . . . . . . . . . . . . 16  |-  ( suc  v  e.  om  ->  suc  v  e.  Fin )
3423, 33syl 14 . . . . . . . . . . . . . . 15  |-  ( v  e.  om  ->  suc  v  e.  Fin )
3534adantr 270 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  e.  Fin )
36 enfi 6429 . . . . . . . . . . . . . . 15  |-  ( w 
~~  suc  v  ->  ( w  e.  Fin  <->  suc  v  e. 
Fin ) )
3736adantl 271 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  e. 
Fin 
<->  suc  v  e.  Fin ) )
3835, 37mpbird 165 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  w  e.  Fin )
39 fin0 6441 . . . . . . . . . . . . 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 496 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  v  e.  om )
42 dif1en 6435 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  w  ~~  suc  v  /\  z  e.  w )  ->  ( w  \  {
z } )  ~~  v )
43423expa 1139 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
w  \  { z } )  ~~  v
)
44 fidifsnid 6427 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e.  Fin  /\  z  e.  w )  ->  ( ( w  \  { z } )  u.  { z } )  =  w )
4538, 44sylan 277 . . . . . . . . . . . . . . . 16  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
( w  \  {
z } )  u. 
{ z } )  =  w )
46 neldifsn 3538 . . . . . . . . . . . . . . . . . 18  |-  -.  z  e.  ( w  \  {
z } )
47 vex 2612 . . . . . . . . . . . . . . . . . . . 20  |-  w  e. 
_V
48 difexg 3939 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  _V  ->  (
w  \  { z } )  e.  _V )
4947, 48ax-mp 7 . . . . . . . . . . . . . . . . . . 19  |-  ( w 
\  { z } )  e.  _V
50 breq1 3808 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( y  ~~  v 
<->  ( w  \  {
z } )  ~~  v ) )
5150anbi2d 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( ( v  e.  om  /\  y  ~~  v )  <->  ( v  e.  om  /\  ( w 
\  { z } )  ~~  v ) ) )
52 eleq2 2146 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( z  e.  y  <->  z  e.  ( w  \  { z } ) ) )
5352notbid 625 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( -.  z  e.  y  <->  -.  z  e.  ( w  \  { z } ) ) )
5451, 53anbi12d 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( w  \  { z } )  ->  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y
)  <->  ( ( v  e.  om  /\  (
w  \  { z } )  ~~  v
)  /\  -.  z  e.  ( w  \  {
z } ) ) ) )
55 uneq1 3129 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( y  u. 
{ z } )  =  ( ( w 
\  { z } )  u.  { z } ) )
5655sbceq1d 2829 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( [. (
y  u.  { z } )  /  x ]. ph  <->  [. ( ( w 
\  { z } )  u.  { z } )  /  x ]. ph ) )
5756imbi2d 228 . . . . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . . . . 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 3808 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x  ~~  v  <->  y  ~~  v ) )
60 findcard2s.2 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
6159, 60imbi12d 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( x  ~~  v  ->  ph )  <->  ( y  ~~  v  ->  ch )
) )
6261spv 1783 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. x ( x  ~~  v  ->  ph )  ->  (
y  ~~  v  ->  ch ) )
63 pm2.27 39 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y 
~~  v  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
6463adantl 271 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( ( y  ~~  v  ->  ch )  ->  ch ) )
6564adantr 270 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
66 rspe 2417 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  om  /\  y  ~~  v )  ->  E. v  e.  om  y  ~~  v )
67 isfi 6329 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  Fin  <->  E. v  e.  om  y  ~~  v
)
6866, 67sylibr 132 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
y  e.  Fin )
69 findcard2s.6 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  Fin  /\  -.  z  e.  y
)  ->  ( ch  ->  th ) )
7068, 69sylan 277 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  ( ch  ->  th ) )
7165, 70syld 44 . . . . . . . . . . . . . . . . . . . . 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 2612 . . . . . . . . . . . . . . . . . . . . . 22  |-  y  e. 
_V
74 vex 2612 . . . . . . . . . . . . . . . . . . . . . . 23  |-  z  e. 
_V
7574snex 3977 . . . . . . . . . . . . . . . . . . . . . 22  |-  { z }  e.  _V
7673, 75unex 4222 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  u.  { z } )  e.  _V
77 findcard2s.3 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
7876, 77sbcie 2857 . . . . . . . . . . . . . . . . . . . 20  |-  ( [. ( y  u.  {
z } )  /  x ]. ph  <->  th )
7972, 78syl6ibr 160 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph ) )
8049, 58, 79vtocl 2661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  /\  -.  z  e.  ( w  \  { z } ) )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
8146, 80mpan2 416 . . . . . . . . . . . . . . . . 17  |-  ( ( v  e.  om  /\  ( w  \  { z } )  ~~  v
)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
82 dfsbcq 2826 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  ( [. ( ( w  \  { z } )  u.  { z } )  /  x ]. ph  <->  [. w  /  x ]. ph ) )
8382imbi2d 228 . . . . . . . . . . . . . . . . 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 152 . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . 14  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
)
8786ex 113 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( z  e.  w  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8887exlimdv 1742 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( E. z 
z  e.  w  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8940, 88sylbid 148 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =/=  (/)  ->  ( A. x
( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
9089ex 113 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
w  ~~  suc  v  -> 
( w  =/=  (/)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) ) )
9132, 90mpdd 40 . . . . . . . . 9  |-  ( v  e.  om  ->  (
w  ~~  suc  v  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
9291com23 77 . . . . . . . 8  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  (
w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
9392alrimdv 1799 . . . . . . 7  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. w
( w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
94 nfv 1462 . . . . . . . 8  |-  F/ w
( x  ~~  suc  v  ->  ph )
95 nfv 1462 . . . . . . . . 9  |-  F/ x  w  ~~  suc  v
96 nfsbc1v 2842 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
9795, 96nfim 1505 . . . . . . . 8  |-  F/ x
( w  ~~  suc  v  ->  [. w  /  x ]. ph )
98 breq1 3808 . . . . . . . . 9  |-  ( x  =  w  ->  (
x  ~~  suc  v  <->  w  ~~  suc  v ) )
99 sbceq1a 2833 . . . . . . . . 9  |-  ( x  =  w  ->  ( ph 
<-> 
[. w  /  x ]. ph ) )
10098, 99imbi12d 232 . . . . . . . 8  |-  ( x  =  w  ->  (
( x  ~~  suc  v  ->  ph )  <->  ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
) )
10194, 97, 100cbval 1679 . . . . . . 7  |-  ( A. x ( x  ~~  suc  v  ->  ph )  <->  A. w ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
)
10293, 101syl6ibr 160 . . . . . 6  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. x
( x  ~~  suc  v  ->  ph ) ) )
1035, 8, 11, 17, 102finds1 4371 . . . . 5  |-  ( w  e.  om  ->  A. x
( x  ~~  w  ->  ph ) )
10410319.21bi 1491 . . . 4  |-  ( w  e.  om  ->  (
x  ~~  w  ->  ph ) )
105104rexlimiv 2476 . . 3  |-  ( E. w  e.  om  x  ~~  w  ->  ph )
1062, 105sylbi 119 . 2  |-  ( x  e.  Fin  ->  ph )
1071, 106vtoclga 2672 1  |-  ( A  e.  Fin  ->  ta )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    <-> wb 103   A.wal 1283    = wceq 1285   E.wex 1422    e. wcel 1434    =/= wne 2249   E.wrex 2354   _Vcvv 2609   [.wsbc 2824    \ cdif 2979    u. cun 2980   (/)c0 3267   {csn 3416   class class class wbr 3805   suc csuc 4148   omcom 4359    ~~ cen 6306   Fincfn 6308
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3913  ax-sep 3916  ax-nul 3924  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308  ax-iinf 4357
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2611  df-sbc 2825  df-csb 2918  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-if 3369  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-int 3657  df-iun 3700  df-br 3806  df-opab 3860  df-mpt 3861  df-tr 3896  df-id 4076  df-iord 4149  df-on 4151  df-suc 4154  df-iom 4360  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-f1 4957  df-fo 4958  df-f1o 4959  df-fv 4960  df-er 6193  df-en 6309  df-fin 6311
This theorem is referenced by:  findcard2d  6447  findcard2sd  6448  diffifi  6450  ac6sfi  6454  fisseneq  6474
  Copyright terms: Public domain W3C validator