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

Theorem findcard2s 6375
Description: Variation of findcard2 6374 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 6269 . . 3  |-  ( x  e.  Fin  <->  E. w  e.  om  x  ~~  w
)
3 breq2 3793 . . . . . . . 8  |-  ( w  =  (/)  ->  ( x 
~~  w  <->  x  ~~  (/) ) )
43imbi1d 224 . . . . . . 7  |-  ( w  =  (/)  ->  ( ( x  ~~  w  ->  ph )  <->  ( x  ~~  (/) 
->  ph ) ) )
54albidv 1719 . . . . . 6  |-  ( w  =  (/)  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  (/)  ->  ph )
) )
6 breq2 3793 . . . . . . . 8  |-  ( w  =  v  ->  (
x  ~~  w  <->  x  ~~  v ) )
76imbi1d 224 . . . . . . 7  |-  ( w  =  v  ->  (
( x  ~~  w  ->  ph )  <->  ( x  ~~  v  ->  ph )
) )
87albidv 1719 . . . . . 6  |-  ( w  =  v  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  v  ->  ph ) ) )
9 breq2 3793 . . . . . . . 8  |-  ( w  =  suc  v  -> 
( x  ~~  w  <->  x 
~~  suc  v )
)
109imbi1d 224 . . . . . . 7  |-  ( w  =  suc  v  -> 
( ( x  ~~  w  ->  ph )  <->  ( x  ~~  suc  v  ->  ph )
) )
1110albidv 1719 . . . . . 6  |-  ( w  =  suc  v  -> 
( A. x ( x  ~~  w  ->  ph )  <->  A. x ( x 
~~  suc  v  ->  ph ) ) )
12 en0 6303 . . . . . . . 8  |-  ( x 
~~  (/)  <->  x  =  (/) )
13 findcard2s.5 . . . . . . . . 9  |-  ps
14 findcard2s.1 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
1513, 14mpbiri 161 . . . . . . . 8  |-  ( x  =  (/)  ->  ph )
1612, 15sylbi 118 . . . . . . 7  |-  ( x 
~~  (/)  ->  ph )
1716ax-gen 1352 . . . . . 6  |-  A. x
( x  ~~  (/)  ->  ph )
18 peano3 4344 . . . . . . . . . . . . 13  |-  ( v  e.  om  ->  suc  v  =/=  (/) )
1918adantr 265 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =/=  (/) )
20 breq1 3792 . . . . . . . . . . . . . . . 16  |-  ( w  =  (/)  ->  ( w 
~~  suc  v  <->  (/)  ~~  suc  v ) )
2120anbi2d 445 . . . . . . . . . . . . . . 15  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  <-> 
( v  e.  om  /\  (/)  ~~  suc  v ) ) )
22 peano1 4342 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  om
23 peano2 4343 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  om  ->  suc  v  e.  om )
24 nneneq 6348 . . . . . . . . . . . . . . . . . 18  |-  ( (
(/)  e.  om  /\  suc  v  e.  om )  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2522, 23, 24sylancr 399 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  om  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2625biimpa 284 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  (/)  =  suc  v )
2726eqcomd 2059 . . . . . . . . . . . . . . 15  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  suc  v  =  (/) )
2821, 27syl6bi 156 . . . . . . . . . . . . . 14  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =  (/) ) )
2928com12 30 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =  (/)  ->  suc  v  =  (/) ) )
3029necon3d 2262 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( suc  v  =/=  (/)  ->  w  =/=  (/) ) )
3119, 30mpd 13 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  w  =/=  (/) )
3231ex 112 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
w  ~~  suc  v  ->  w  =/=  (/) ) )
33 nnfi 6361 . . . . . . . . . . . . . . . 16  |-  ( suc  v  e.  om  ->  suc  v  e.  Fin )
3423, 33syl 14 . . . . . . . . . . . . . . 15  |-  ( v  e.  om  ->  suc  v  e.  Fin )
3534adantr 265 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  e.  Fin )
36 enfi 6362 . . . . . . . . . . . . . . 15  |-  ( w 
~~  suc  v  ->  ( w  e.  Fin  <->  suc  v  e. 
Fin ) )
3736adantl 266 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  e. 
Fin 
<->  suc  v  e.  Fin ) )
3835, 37mpbird 160 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  w  e.  Fin )
39 fin0 6370 . . . . . . . . . . . . 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 489 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  v  e.  om )
42 dif1en 6365 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  w  ~~  suc  v  /\  z  e.  w )  ->  ( w  \  {
z } )  ~~  v )
43423expa 1113 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
w  \  { z } )  ~~  v
)
44 fidifsnid 6360 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e.  Fin  /\  z  e.  w )  ->  ( ( w  \  { z } )  u.  { z } )  =  w )
4538, 44sylan 271 . . . . . . . . . . . . . . . 16  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
( w  \  {
z } )  u. 
{ z } )  =  w )
46 neldifsn 3522 . . . . . . . . . . . . . . . . . 18  |-  -.  z  e.  ( w  \  {
z } )
47 vex 2575 . . . . . . . . . . . . . . . . . . . 20  |-  w  e. 
_V
48 difexg 3923 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  _V  ->  (
w  \  { z } )  e.  _V )
4947, 48ax-mp 7 . . . . . . . . . . . . . . . . . . 19  |-  ( w 
\  { z } )  e.  _V
50 breq1 3792 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( y  ~~  v 
<->  ( w  \  {
z } )  ~~  v ) )
5150anbi2d 445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( ( v  e.  om  /\  y  ~~  v )  <->  ( v  e.  om  /\  ( w 
\  { z } )  ~~  v ) ) )
52 eleq2 2115 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( z  e.  y  <->  z  e.  ( w  \  { z } ) ) )
5352notbid 600 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( -.  z  e.  y  <->  -.  z  e.  ( w  \  { z } ) ) )
5451, 53anbi12d 450 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( w  \  { z } )  ->  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y
)  <->  ( ( v  e.  om  /\  (
w  \  { z } )  ~~  v
)  /\  -.  z  e.  ( w  \  {
z } ) ) ) )
55 uneq1 3115 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( y  u. 
{ z } )  =  ( ( w 
\  { z } )  u.  { z } ) )
5655sbceq1d 2789 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( [. (
y  u.  { z } )  /  x ]. ph  <->  [. ( ( w 
\  { z } )  u.  { z } )  /  x ]. ph ) )
5756imbi2d 223 . . . . . . . . . . . . . . . . . . . 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 227 . . . . . . . . . . . . . . . . . . 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 3792 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x  ~~  v  <->  y  ~~  v ) )
60 findcard2s.2 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
6159, 60imbi12d 227 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( x  ~~  v  ->  ph )  <->  ( y  ~~  v  ->  ch )
) )
6261spv 1754 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. x ( x  ~~  v  ->  ph )  ->  (
y  ~~  v  ->  ch ) )
63 pm2.27 39 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y 
~~  v  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
6463adantl 266 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( ( y  ~~  v  ->  ch )  ->  ch ) )
6564adantr 265 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
66 rspe 2385 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  om  /\  y  ~~  v )  ->  E. v  e.  om  y  ~~  v )
67 isfi 6269 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  Fin  <->  E. v  e.  om  y  ~~  v
)
6866, 67sylibr 141 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
y  e.  Fin )
69 findcard2s.6 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  Fin  /\  -.  z  e.  y
)  ->  ( ch  ->  th ) )
7068, 69sylan 271 . . . . . . . . . . . . . . . . . . . . . 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 2575 . . . . . . . . . . . . . . . . . . . . . 22  |-  y  e. 
_V
74 vex 2575 . . . . . . . . . . . . . . . . . . . . . . 23  |-  z  e. 
_V
7574snex 3962 . . . . . . . . . . . . . . . . . . . . . 22  |-  { z }  e.  _V
7673, 75unex 4201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  u.  { z } )  e.  _V
77 findcard2s.3 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
7876, 77sbcie 2817 . . . . . . . . . . . . . . . . . . . 20  |-  ( [. ( y  u.  {
z } )  /  x ]. ph  <->  th )
7972, 78syl6ibr 155 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( v  e.  om  /\  y  ~~  v )  /\  -.  z  e.  y )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph ) )
8049, 58, 79vtocl 2623 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  /\  -.  z  e.  ( w  \  { z } ) )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
8146, 80mpan2 409 . . . . . . . . . . . . . . . . 17  |-  ( ( v  e.  om  /\  ( w  \  { z } )  ~~  v
)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
82 dfsbcq 2786 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  ( [. ( ( w  \  { z } )  u.  { z } )  /  x ]. ph  <->  [. w  /  x ]. ph ) )
8382imbi2d 223 . . . . . . . . . . . . . . . . 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 147 . . . . . . . . . . . . . . . 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 417 . . . . . . . . . . . . . 14  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
)
8786ex 112 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( z  e.  w  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8887exlimdv 1714 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( E. z 
z  e.  w  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8940, 88sylbid 143 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =/=  (/)  ->  ( A. x
( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
9089ex 112 . . . . . . . . . 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 76 . . . . . . . 8  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  (
w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
9392alrimdv 1770 . . . . . . 7  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. w
( w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
94 nfv 1435 . . . . . . . 8  |-  F/ w
( x  ~~  suc  v  ->  ph )
95 nfv 1435 . . . . . . . . 9  |-  F/ x  w  ~~  suc  v
96 nfsbc1v 2802 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
9795, 96nfim 1478 . . . . . . . 8  |-  F/ x
( w  ~~  suc  v  ->  [. w  /  x ]. ph )
98 breq1 3792 . . . . . . . . 9  |-  ( x  =  w  ->  (
x  ~~  suc  v  <->  w  ~~  suc  v ) )
99 sbceq1a 2793 . . . . . . . . 9  |-  ( x  =  w  ->  ( ph 
<-> 
[. w  /  x ]. ph ) )
10098, 99imbi12d 227 . . . . . . . 8  |-  ( x  =  w  ->  (
( x  ~~  suc  v  ->  ph )  <->  ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
) )
10194, 97, 100cbval 1651 . . . . . . 7  |-  ( A. x ( x  ~~  suc  v  ->  ph )  <->  A. w ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
)
10293, 101syl6ibr 155 . . . . . 6  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. x
( x  ~~  suc  v  ->  ph ) ) )
1035, 8, 11, 17, 102finds1 4350 . . . . 5  |-  ( w  e.  om  ->  A. x
( x  ~~  w  ->  ph ) )
10410319.21bi 1464 . . . 4  |-  ( w  e.  om  ->  (
x  ~~  w  ->  ph ) )
105104rexlimiv 2442 . . 3  |-  ( E. w  e.  om  x  ~~  w  ->  ph )
1062, 105sylbi 118 . 2  |-  ( x  e.  Fin  ->  ph )
1071, 106vtoclga 2634 1  |-  ( A  e.  Fin  ->  ta )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 101    <-> wb 102   A.wal 1255    = wceq 1257   E.wex 1395    e. wcel 1407    =/= wne 2218   E.wrex 2322   _Vcvv 2572   [.wsbc 2784    \ cdif 2939    u. cun 2940   (/)c0 3249   {csn 3400   class class class wbr 3789   suc csuc 4127   omcom 4338    ~~ cen 6247   Fincfn 6249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-13 1418  ax-14 1419  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-coll 3897  ax-sep 3900  ax-nul 3908  ax-pow 3952  ax-pr 3969  ax-un 4195  ax-setind 4287  ax-iinf 4336
This theorem depends on definitions:  df-bi 114  df-dc 752  df-3or 895  df-3an 896  df-tru 1260  df-fal 1263  df-nf 1364  df-sb 1660  df-eu 1917  df-mo 1918  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ne 2219  df-ral 2326  df-rex 2327  df-reu 2328  df-rab 2330  df-v 2574  df-sbc 2785  df-csb 2878  df-dif 2945  df-un 2947  df-in 2949  df-ss 2956  df-nul 3250  df-if 3357  df-pw 3386  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3606  df-int 3641  df-iun 3684  df-br 3790  df-opab 3844  df-mpt 3845  df-tr 3880  df-id 4055  df-iord 4128  df-on 4130  df-suc 4133  df-iom 4339  df-xp 4376  df-rel 4377  df-cnv 4378  df-co 4379  df-dm 4380  df-rn 4381  df-res 4382  df-ima 4383  df-iota 4892  df-fun 4929  df-fn 4930  df-f 4931  df-f1 4932  df-fo 4933  df-f1o 4934  df-fv 4935  df-er 6134  df-en 6250  df-fin 6252
This theorem is referenced by:  findcard2d  6376  findcard2sd  6377  diffifi  6379  ac6sfi  6380
  Copyright terms: Public domain W3C validator