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

Theorem findcard2 6751
Description: Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.)
Hypotheses
Ref Expression
findcard2.1  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
findcard2.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
findcard2.3  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
findcard2.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
findcard2.5  |-  ps
findcard2.6  |-  ( y  e.  Fin  ->  ( ch  ->  th ) )
Assertion
Ref Expression
findcard2  |-  ( A  e.  Fin  ->  ta )
Distinct variable groups:    x, y, z, A    ps, x    ch, x    th, x    ta, x    ph, y, z
Allowed substitution hints:    ph( x)    ps( y,
z)    ch( y, z)    th( y,
z)    ta( y, z)

Proof of Theorem findcard2
Dummy variables  w  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 findcard2.4 . 2  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2 isfi 6623 . . 3  |-  ( x  e.  Fin  <->  E. w  e.  om  x  ~~  w
)
3 breq2 3903 . . . . . . . 8  |-  ( w  =  (/)  ->  ( x 
~~  w  <->  x  ~~  (/) ) )
43imbi1d 230 . . . . . . 7  |-  ( w  =  (/)  ->  ( ( x  ~~  w  ->  ph )  <->  ( x  ~~  (/) 
->  ph ) ) )
54albidv 1780 . . . . . 6  |-  ( w  =  (/)  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  (/)  ->  ph )
) )
6 breq2 3903 . . . . . . . 8  |-  ( w  =  v  ->  (
x  ~~  w  <->  x  ~~  v ) )
76imbi1d 230 . . . . . . 7  |-  ( w  =  v  ->  (
( x  ~~  w  ->  ph )  <->  ( x  ~~  v  ->  ph )
) )
87albidv 1780 . . . . . 6  |-  ( w  =  v  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  v  ->  ph ) ) )
9 breq2 3903 . . . . . . . 8  |-  ( w  =  suc  v  -> 
( x  ~~  w  <->  x 
~~  suc  v )
)
109imbi1d 230 . . . . . . 7  |-  ( w  =  suc  v  -> 
( ( x  ~~  w  ->  ph )  <->  ( x  ~~  suc  v  ->  ph )
) )
1110albidv 1780 . . . . . 6  |-  ( w  =  suc  v  -> 
( A. x ( x  ~~  w  ->  ph )  <->  A. x ( x 
~~  suc  v  ->  ph ) ) )
12 en0 6657 . . . . . . . 8  |-  ( x 
~~  (/)  <->  x  =  (/) )
13 findcard2.5 . . . . . . . . 9  |-  ps
14 findcard2.1 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
1513, 14mpbiri 167 . . . . . . . 8  |-  ( x  =  (/)  ->  ph )
1612, 15sylbi 120 . . . . . . 7  |-  ( x 
~~  (/)  ->  ph )
1716ax-gen 1410 . . . . . 6  |-  A. x
( x  ~~  (/)  ->  ph )
18 peano3 4480 . . . . . . . . . . . . 13  |-  ( v  e.  om  ->  suc  v  =/=  (/) )
1918adantr 274 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =/=  (/) )
20 breq1 3902 . . . . . . . . . . . . . . . 16  |-  ( w  =  (/)  ->  ( w 
~~  suc  v  <->  (/)  ~~  suc  v ) )
2120anbi2d 459 . . . . . . . . . . . . . . 15  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  <-> 
( v  e.  om  /\  (/)  ~~  suc  v ) ) )
22 peano1 4478 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  om
23 peano2 4479 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  om  ->  suc  v  e.  om )
24 nneneq 6719 . . . . . . . . . . . . . . . . . 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 2123 . . . . . . . . . . . . . . 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 2329 . . . . . . . . . . . 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 6734 . . . . . . . . . . . . . . . 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 6735 . . . . . . . . . . . . . . 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 6747 . . . . . . . . . . . . 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 503 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  v  e.  om )
42 dif1en 6741 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  w  ~~  suc  v  /\  z  e.  w )  ->  ( w  \  {
z } )  ~~  v )
43423expa 1166 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
w  \  { z } )  ~~  v
)
44 fidifsnid 6733 . . . . . . . . . . . . . . . . 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 vex 2663 . . . . . . . . . . . . . . . . . . 19  |-  w  e. 
_V
47 difexg 4039 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  _V  ->  (
w  \  { z } )  e.  _V )
4846, 47ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( w 
\  { z } )  e.  _V
49 breq1 3902 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( w  \  { z } )  ->  ( y  ~~  v 
<->  ( w  \  {
z } )  ~~  v ) )
5049anbi2d 459 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( w  \  { z } )  ->  ( ( v  e.  om  /\  y  ~~  v )  <->  ( v  e.  om  /\  ( w 
\  { z } )  ~~  v ) ) )
51 uneq1 3193 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( y  u. 
{ z } )  =  ( ( w 
\  { z } )  u.  { z } ) )
5251sbceq1d 2887 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( w  \  { z } )  ->  ( [. (
y  u.  { z } )  /  x ]. ph  <->  [. ( ( w 
\  { z } )  u.  { z } )  /  x ]. ph ) )
5352imbi2d 229 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( w  \  { z } )  ->  ( ( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph )  <->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
) )
5450, 53imbi12d 233 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( w  \  { z } )  ->  ( ( ( v  e.  om  /\  y  ~~  v )  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph ) )  <->  ( (
v  e.  om  /\  ( w  \  { z } )  ~~  v
)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
) ) )
55 breq1 3902 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
x  ~~  v  <->  y  ~~  v ) )
56 findcard2.2 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
5755, 56imbi12d 233 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( x  ~~  v  ->  ph )  <->  ( y  ~~  v  ->  ch )
) )
5857spv 1816 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. x ( x  ~~  v  ->  ph )  ->  (
y  ~~  v  ->  ch ) )
59 rspe 2458 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( v  e.  om  /\  y  ~~  v )  ->  E. v  e.  om  y  ~~  v )
60 isfi 6623 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  Fin  <->  E. v  e.  om  y  ~~  v
)
6159, 60sylibr 133 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
y  e.  Fin )
62 pm2.27 40 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y 
~~  v  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
6362adantl 275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( ( y  ~~  v  ->  ch )  ->  ch ) )
64 findcard2.6 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  Fin  ->  ( ch  ->  th ) )
6561, 63, 64sylsyld 58 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( ( y  ~~  v  ->  ch )  ->  th ) )
6658, 65syl5 32 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( A. x ( x  ~~  v  ->  ph )  ->  th )
)
67 vex 2663 . . . . . . . . . . . . . . . . . . . . 21  |-  y  e. 
_V
68 vex 2663 . . . . . . . . . . . . . . . . . . . . . 22  |-  z  e. 
_V
6968snex 4079 . . . . . . . . . . . . . . . . . . . . 21  |-  { z }  e.  _V
7067, 69unex 4332 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  u.  { z } )  e.  _V
71 findcard2.3 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
7270, 71sbcie 2915 . . . . . . . . . . . . . . . . . . 19  |-  ( [. ( y  u.  {
z } )  /  x ]. ph  <->  th )
7366, 72syl6ibr 161 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph ) )
7448, 54, 73vtocl 2714 . . . . . . . . . . . . . . . . 17  |-  ( ( v  e.  om  /\  ( w  \  { z } )  ~~  v
)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
75 dfsbcq 2884 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  ( [. ( ( w  \  { z } )  u.  { z } )  /  x ]. ph  <->  [. w  /  x ]. ph ) )
7675imbi2d 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 ) ) )
7774, 76syl5ib 153 . . . . . . . . . . . . . . . 16  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  (
( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
7845, 77syl 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 )
) )
7941, 43, 78mp2and 429 . . . . . . . . . . . . . 14  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
)
8079ex 114 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( z  e.  w  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8180exlimdv 1775 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( E. z 
z  e.  w  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8240, 81sylbid 149 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =/=  (/)  ->  ( A. x
( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8382ex 114 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
w  ~~  suc  v  -> 
( w  =/=  (/)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) ) )
8432, 83mpdd 41 . . . . . . . . 9  |-  ( v  e.  om  ->  (
w  ~~  suc  v  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8584com23 78 . . . . . . . 8  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  (
w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
8685alrimdv 1832 . . . . . . 7  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. w
( w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
87 nfv 1493 . . . . . . . 8  |-  F/ w
( x  ~~  suc  v  ->  ph )
88 nfv 1493 . . . . . . . . 9  |-  F/ x  w  ~~  suc  v
89 nfsbc1v 2900 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
9088, 89nfim 1536 . . . . . . . 8  |-  F/ x
( w  ~~  suc  v  ->  [. w  /  x ]. ph )
91 breq1 3902 . . . . . . . . 9  |-  ( x  =  w  ->  (
x  ~~  suc  v  <->  w  ~~  suc  v ) )
92 sbceq1a 2891 . . . . . . . . 9  |-  ( x  =  w  ->  ( ph 
<-> 
[. w  /  x ]. ph ) )
9391, 92imbi12d 233 . . . . . . . 8  |-  ( x  =  w  ->  (
( x  ~~  suc  v  ->  ph )  <->  ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
) )
9487, 90, 93cbval 1712 . . . . . . 7  |-  ( A. x ( x  ~~  suc  v  ->  ph )  <->  A. w ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
)
9586, 94syl6ibr 161 . . . . . 6  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. x
( x  ~~  suc  v  ->  ph ) ) )
965, 8, 11, 17, 95finds1 4486 . . . . 5  |-  ( w  e.  om  ->  A. x
( x  ~~  w  ->  ph ) )
979619.21bi 1522 . . . 4  |-  ( w  e.  om  ->  (
x  ~~  w  ->  ph ) )
9897rexlimiv 2520 . . 3  |-  ( E. w  e.  om  x  ~~  w  ->  ph )
992, 98sylbi 120 . 2  |-  ( x  e.  Fin  ->  ph )
1001, 99vtoclga 2726 1  |-  ( A  e.  Fin  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104   A.wal 1314    = wceq 1316   E.wex 1453    e. wcel 1465    =/= wne 2285   E.wrex 2394   _Vcvv 2660   [.wsbc 2882    \ cdif 3038    u. cun 3039   (/)c0 3333   {csn 3497   class class class wbr 3899   suc csuc 4257   omcom 4474    ~~ cen 6600   Fincfn 6602
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 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-ral 2398  df-rex 2399  df-reu 2400  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-if 3445  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-iord 4258  df-on 4260  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-er 6397  df-en 6603  df-fin 6605
This theorem is referenced by:  finomni  6980  rexfiuz  10729  fimaxre2  10966
  Copyright terms: Public domain W3C validator