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

Theorem findcard2 6837
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 6709 . . 3  |-  ( x  e.  Fin  <->  E. w  e.  om  x  ~~  w
)
3 breq2 3971 . . . . . . . 8  |-  ( w  =  (/)  ->  ( x 
~~  w  <->  x  ~~  (/) ) )
43imbi1d 230 . . . . . . 7  |-  ( w  =  (/)  ->  ( ( x  ~~  w  ->  ph )  <->  ( x  ~~  (/) 
->  ph ) ) )
54albidv 1804 . . . . . 6  |-  ( w  =  (/)  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  (/)  ->  ph )
) )
6 breq2 3971 . . . . . . . 8  |-  ( w  =  v  ->  (
x  ~~  w  <->  x  ~~  v ) )
76imbi1d 230 . . . . . . 7  |-  ( w  =  v  ->  (
( x  ~~  w  ->  ph )  <->  ( x  ~~  v  ->  ph )
) )
87albidv 1804 . . . . . 6  |-  ( w  =  v  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  v  ->  ph ) ) )
9 breq2 3971 . . . . . . . 8  |-  ( w  =  suc  v  -> 
( x  ~~  w  <->  x 
~~  suc  v )
)
109imbi1d 230 . . . . . . 7  |-  ( w  =  suc  v  -> 
( ( x  ~~  w  ->  ph )  <->  ( x  ~~  suc  v  ->  ph )
) )
1110albidv 1804 . . . . . 6  |-  ( w  =  suc  v  -> 
( A. x ( x  ~~  w  ->  ph )  <->  A. x ( x 
~~  suc  v  ->  ph ) ) )
12 en0 6743 . . . . . . . 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 1429 . . . . . 6  |-  A. x
( x  ~~  (/)  ->  ph )
18 peano3 4558 . . . . . . . . . . . . 13  |-  ( v  e.  om  ->  suc  v  =/=  (/) )
1918adantr 274 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =/=  (/) )
20 breq1 3970 . . . . . . . . . . . . . . . 16  |-  ( w  =  (/)  ->  ( w 
~~  suc  v  <->  (/)  ~~  suc  v ) )
2120anbi2d 460 . . . . . . . . . . . . . . 15  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  <-> 
( v  e.  om  /\  (/)  ~~  suc  v ) ) )
22 peano1 4556 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  om
23 peano2 4557 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  om  ->  suc  v  e.  om )
24 nneneq 6805 . . . . . . . . . . . . . . . . . 18  |-  ( (
(/)  e.  om  /\  suc  v  e.  om )  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2522, 23, 24sylancr 411 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  om  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2625biimpa 294 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  (/)  =  suc  v )
2726eqcomd 2163 . . . . . . . . . . . . . . 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 2371 . . . . . . . . . . . 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 6820 . . . . . . . . . . . . . . . 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 6821 . . . . . . . . . . . . . . 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 6833 . . . . . . . . . . . . 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 519 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  v  e.  om )
42 dif1en 6827 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  w  ~~  suc  v  /\  z  e.  w )  ->  ( w  \  {
z } )  ~~  v )
43423expa 1185 . . . . . . . . . . . . . . 15  |-  ( ( ( v  e.  om  /\  w  ~~  suc  v
)  /\  z  e.  w )  ->  (
w  \  { z } )  ~~  v
)
44 fidifsnid 6819 . . . . . . . . . . . . . . . . 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 2715 . . . . . . . . . . . . . . . . . . 19  |-  w  e. 
_V
47 difexg 4108 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  _V  ->  (
w  \  { z } )  e.  _V )
4846, 47ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( w 
\  { z } )  e.  _V
49 breq1 3970 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( w  \  { z } )  ->  ( y  ~~  v 
<->  ( w  \  {
z } )  ~~  v ) )
5049anbi2d 460 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( w  \  { z } )  ->  ( ( v  e.  om  /\  y  ~~  v )  <->  ( v  e.  om  /\  ( w 
\  { z } )  ~~  v ) ) )
51 uneq1 3255 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( y  u. 
{ z } )  =  ( ( w 
\  { z } )  u.  { z } ) )
5251sbceq1d 2942 . . . . . . . . . . . . . . . . . . . 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 3970 . . . . . . . . . . . . . . . . . . . . . 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 1840 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. x ( x  ~~  v  ->  ph )  ->  (
y  ~~  v  ->  ch ) )
59 rspe 2506 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( v  e.  om  /\  y  ~~  v )  ->  E. v  e.  om  y  ~~  v )
60 isfi 6709 . . . . . . . . . . . . . . . . . . . . . 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 2715 . . . . . . . . . . . . . . . . . . . . 21  |-  y  e. 
_V
68 vex 2715 . . . . . . . . . . . . . . . . . . . . . 22  |-  z  e. 
_V
6968snex 4149 . . . . . . . . . . . . . . . . . . . . 21  |-  { z }  e.  _V
7067, 69unex 4404 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  u.  { z } )  e.  _V
71 findcard2.3 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
7270, 71sbcie 2971 . . . . . . . . . . . . . . . . . . 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 2766 . . . . . . . . . . . . . . . . 17  |-  ( ( v  e.  om  /\  ( w  \  { z } )  ~~  v
)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
75 dfsbcq 2939 . . . . . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . . 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 1799 . . . . . . . . . . . 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 1856 . . . . . . 7  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. w
( w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
87 nfv 1508 . . . . . . . 8  |-  F/ w
( x  ~~  suc  v  ->  ph )
88 nfv 1508 . . . . . . . . 9  |-  F/ x  w  ~~  suc  v
89 nfsbc1v 2955 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
9088, 89nfim 1552 . . . . . . . 8  |-  F/ x
( w  ~~  suc  v  ->  [. w  /  x ]. ph )
91 breq1 3970 . . . . . . . . 9  |-  ( x  =  w  ->  (
x  ~~  suc  v  <->  w  ~~  suc  v ) )
92 sbceq1a 2946 . . . . . . . . 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 1734 . . . . . . 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 4564 . . . . 5  |-  ( w  e.  om  ->  A. x
( x  ~~  w  ->  ph ) )
979619.21bi 1538 . . . 4  |-  ( w  e.  om  ->  (
x  ~~  w  ->  ph ) )
9897rexlimiv 2568 . . 3  |-  ( E. w  e.  om  x  ~~  w  ->  ph )
992, 98sylbi 120 . 2  |-  ( x  e.  Fin  ->  ph )
1001, 99vtoclga 2778 1  |-  ( A  e.  Fin  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104   A.wal 1333    = wceq 1335   E.wex 1472    e. wcel 2128    =/= wne 2327   E.wrex 2436   _Vcvv 2712   [.wsbc 2937    \ cdif 3099    u. cun 3100   (/)c0 3395   {csn 3561   class class class wbr 3967   suc csuc 4328   omcom 4552    ~~ cen 6686   Fincfn 6688
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 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4082  ax-sep 4085  ax-nul 4093  ax-pow 4138  ax-pr 4172  ax-un 4396  ax-setind 4499  ax-iinf 4550
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3396  df-if 3507  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-int 3810  df-iun 3853  df-br 3968  df-opab 4029  df-mpt 4030  df-tr 4066  df-id 4256  df-iord 4329  df-on 4331  df-suc 4334  df-iom 4553  df-xp 4595  df-rel 4596  df-cnv 4597  df-co 4598  df-dm 4599  df-rn 4600  df-res 4601  df-ima 4602  df-iota 5138  df-fun 5175  df-fn 5176  df-f 5177  df-f1 5178  df-fo 5179  df-f1o 5180  df-fv 5181  df-er 6483  df-en 6689  df-fin 6691
This theorem is referenced by:  finomni  7086  rexfiuz  10901  fimaxre2  11138
  Copyright terms: Public domain W3C validator