Metamath Proof Explorer

Theorem findcard

Description: Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses findcard.1 
|- ( x = (/) -> ( ph <-> ps ) )
findcard.2 
|- ( x = ( y \ { z } ) -> ( ph <-> ch ) )
findcard.3 
|- ( x = y -> ( ph <-> th ) )
findcard.4 
|- ( x = A -> ( ph <-> ta ) )
findcard.5 
|- ps
findcard.6 
|- ( y e. Fin -> ( A. z e. y ch -> th ) )
Assertion findcard 
|- ( A e. Fin -> ta )

Proof

Step Hyp Ref Expression
1 findcard.1 
 |-  ( x = (/) -> ( ph <-> ps ) )
2 findcard.2 
 |-  ( x = ( y \ { z } ) -> ( ph <-> ch ) )
3 findcard.3 
 |-  ( x = y -> ( ph <-> th ) )
4 findcard.4 
 |-  ( x = A -> ( ph <-> ta ) )
5 findcard.5 
 |-  ps
6 findcard.6 
 |-  ( y e. Fin -> ( A. z e. y ch -> th ) )
7 isfi 
 |-  ( x e. Fin <-> E. w e. _om x ~~ w )
8 breq2 
 |-  ( w = (/) -> ( x ~~ w <-> x ~~ (/) ) )
9 8 imbi1d 
 |-  ( w = (/) -> ( ( x ~~ w -> ph ) <-> ( x ~~ (/) -> ph ) ) )
10 9 albidv 
 |-  ( w = (/) -> ( A. x ( x ~~ w -> ph ) <-> A. x ( x ~~ (/) -> ph ) ) )
11 breq2 
 |-  ( w = v -> ( x ~~ w <-> x ~~ v ) )
12 11 imbi1d 
 |-  ( w = v -> ( ( x ~~ w -> ph ) <-> ( x ~~ v -> ph ) ) )
13 12 albidv 
 |-  ( w = v -> ( A. x ( x ~~ w -> ph ) <-> A. x ( x ~~ v -> ph ) ) )
14 breq2 
 |-  ( w = suc v -> ( x ~~ w <-> x ~~ suc v ) )
15 14 imbi1d 
 |-  ( w = suc v -> ( ( x ~~ w -> ph ) <-> ( x ~~ suc v -> ph ) ) )
16 15 albidv 
 |-  ( w = suc v -> ( A. x ( x ~~ w -> ph ) <-> A. x ( x ~~ suc v -> ph ) ) )
17 en0 
 |-  ( x ~~ (/) <-> x = (/) )
18 5 1 mpbiri 
 |-  ( x = (/) -> ph )
19 17 18 sylbi 
 |-  ( x ~~ (/) -> ph )
20 19 ax-gen 
 |-  A. x ( x ~~ (/) -> ph )
21 peano2 
 |-  ( v e. _om -> suc v e. _om )
22 breq2 
 |-  ( w = suc v -> ( y ~~ w <-> y ~~ suc v ) )
23 22 rspcev 
 |-  ( ( suc v e. _om /\ y ~~ suc v ) -> E. w e. _om y ~~ w )
24 21 23 sylan 
 |-  ( ( v e. _om /\ y ~~ suc v ) -> E. w e. _om y ~~ w )
25 isfi 
 |-  ( y e. Fin <-> E. w e. _om y ~~ w )
26 24 25 sylibr 
 |-  ( ( v e. _om /\ y ~~ suc v ) -> y e. Fin )
27 26 3adant2 
 |-  ( ( v e. _om /\ A. x ( x ~~ v -> ph ) /\ y ~~ suc v ) -> y e. Fin )
28 dif1en 
 |-  ( ( v e. _om /\ y ~~ suc v /\ z e. y ) -> ( y \ { z } ) ~~ v )
29 28 3expa 
 |-  ( ( ( v e. _om /\ y ~~ suc v ) /\ z e. y ) -> ( y \ { z } ) ~~ v )
30 vex 
 |-  y e. _V
31 30 difexi 
 |-  ( y \ { z } ) e. _V
32 breq1 
 |-  ( x = ( y \ { z } ) -> ( x ~~ v <-> ( y \ { z } ) ~~ v ) )
33 32 2 imbi12d 
 |-  ( x = ( y \ { z } ) -> ( ( x ~~ v -> ph ) <-> ( ( y \ { z } ) ~~ v -> ch ) ) )
34 31 33 spcv 
 |-  ( A. x ( x ~~ v -> ph ) -> ( ( y \ { z } ) ~~ v -> ch ) )
35 29 34 syl5com 
 |-  ( ( ( v e. _om /\ y ~~ suc v ) /\ z e. y ) -> ( A. x ( x ~~ v -> ph ) -> ch ) )
36 35 ralrimdva 
 |-  ( ( v e. _om /\ y ~~ suc v ) -> ( A. x ( x ~~ v -> ph ) -> A. z e. y ch ) )
37 36 imp 
 |-  ( ( ( v e. _om /\ y ~~ suc v ) /\ A. x ( x ~~ v -> ph ) ) -> A. z e. y ch )
38 37 an32s 
 |-  ( ( ( v e. _om /\ A. x ( x ~~ v -> ph ) ) /\ y ~~ suc v ) -> A. z e. y ch )
39 38 3impa 
 |-  ( ( v e. _om /\ A. x ( x ~~ v -> ph ) /\ y ~~ suc v ) -> A. z e. y ch )
40 27 39 6 sylc 
 |-  ( ( v e. _om /\ A. x ( x ~~ v -> ph ) /\ y ~~ suc v ) -> th )
41 40 3exp 
 |-  ( v e. _om -> ( A. x ( x ~~ v -> ph ) -> ( y ~~ suc v -> th ) ) )
42 41 alrimdv 
 |-  ( v e. _om -> ( A. x ( x ~~ v -> ph ) -> A. y ( y ~~ suc v -> th ) ) )
43 breq1 
 |-  ( x = y -> ( x ~~ suc v <-> y ~~ suc v ) )
44 43 3 imbi12d 
 |-  ( x = y -> ( ( x ~~ suc v -> ph ) <-> ( y ~~ suc v -> th ) ) )
45 44 cbvalvw 
 |-  ( A. x ( x ~~ suc v -> ph ) <-> A. y ( y ~~ suc v -> th ) )
46 42 45 syl6ibr 
 |-  ( v e. _om -> ( A. x ( x ~~ v -> ph ) -> A. x ( x ~~ suc v -> ph ) ) )
47 10 13 16 20 46 finds1 
 |-  ( w e. _om -> A. x ( x ~~ w -> ph ) )
48 47 19.21bi 
 |-  ( w e. _om -> ( x ~~ w -> ph ) )
49 48 rexlimiv 
 |-  ( E. w e. _om x ~~ w -> ph )
50 7 49 sylbi 
 |-  ( x e. Fin -> ph )
51 4 50 vtoclga 
 |-  ( A e. Fin -> ta )