Metamath Proof Explorer

Theorem findcard2

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)

Ref Expression
Hypotheses 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 findcard2 
|- ( A e. Fin -> ta )

Proof

Step Hyp Ref Expression
1 findcard2.1 
 |-  ( x = (/) -> ( ph <-> ps ) )
2 findcard2.2 
 |-  ( x = y -> ( ph <-> ch ) )
3 findcard2.3 
 |-  ( x = ( y u. { z } ) -> ( ph <-> th ) )
4 findcard2.4 
 |-  ( x = A -> ( ph <-> ta ) )
5 findcard2.5 
 |-  ps
6 findcard2.6 
 |-  ( y e. Fin -> ( 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 nsuceq0 
 |-  suc v =/= (/)
22 breq1 
 |-  ( w = (/) -> ( w ~~ suc v <-> (/) ~~ suc v ) )
23 22 anbi2d 
 |-  ( w = (/) -> ( ( v e. _om /\ w ~~ suc v ) <-> ( v e. _om /\ (/) ~~ suc v ) ) )
24 peano1 
 |-  (/) e. _om
25 peano2 
 |-  ( v e. _om -> suc v e. _om )
26 nneneq 
 |-  ( ( (/) e. _om /\ suc v e. _om ) -> ( (/) ~~ suc v <-> (/) = suc v ) )
27 24 25 26 sylancr 
 |-  ( v e. _om -> ( (/) ~~ suc v <-> (/) = suc v ) )
28 27 biimpa 
 |-  ( ( v e. _om /\ (/) ~~ suc v ) -> (/) = suc v )
29 28 eqcomd 
 |-  ( ( v e. _om /\ (/) ~~ suc v ) -> suc v = (/) )
30 23 29 syl6bi 
 |-  ( w = (/) -> ( ( v e. _om /\ w ~~ suc v ) -> suc v = (/) ) )
31 30 com12 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> ( w = (/) -> suc v = (/) ) )
32 31 necon3d 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> ( suc v =/= (/) -> w =/= (/) ) )
33 21 32 mpi 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> w =/= (/) )
34 33 ex 
 |-  ( v e. _om -> ( w ~~ suc v -> w =/= (/) ) )
35 n0 
 |-  ( w =/= (/) <-> E. z z e. w )
36 dif1en 
 |-  ( ( v e. _om /\ w ~~ suc v /\ z e. w ) -> ( w \ { z } ) ~~ v )
37 36 3expia 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> ( z e. w -> ( w \ { z } ) ~~ v ) )
38 snssi 
 |-  ( z e. w -> { z } C_ w )
39 uncom 
 |-  ( ( w \ { z } ) u. { z } ) = ( { z } u. ( w \ { z } ) )
40 undif 
 |-  ( { z } C_ w <-> ( { z } u. ( w \ { z } ) ) = w )
41 40 biimpi 
 |-  ( { z } C_ w -> ( { z } u. ( w \ { z } ) ) = w )
42 39 41 syl5eq 
 |-  ( { z } C_ w -> ( ( w \ { z } ) u. { z } ) = w )
43 vex 
 |-  w e. _V
44 43 difexi 
 |-  ( w \ { z } ) e. _V
45 breq1 
 |-  ( y = ( w \ { z } ) -> ( y ~~ v <-> ( w \ { z } ) ~~ v ) )
46 45 anbi2d 
 |-  ( y = ( w \ { z } ) -> ( ( v e. _om /\ y ~~ v ) <-> ( v e. _om /\ ( w \ { z } ) ~~ v ) ) )
47 uneq1 
 |-  ( y = ( w \ { z } ) -> ( y u. { z } ) = ( ( w \ { z } ) u. { z } ) )
48 47 sbceq1d 
 |-  ( y = ( w \ { z } ) -> ( [. ( y u. { z } ) / x ]. ph <-> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) )
49 48 imbi2d 
 |-  ( y = ( w \ { z } ) -> ( ( A. x ( x ~~ v -> ph ) -> [. ( y u. { z } ) / x ]. ph ) <-> ( A. x ( x ~~ v -> ph ) -> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) ) )
50 46 49 imbi12d 
 |-  ( 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 ) ) ) )
51 breq1 
 |-  ( x = y -> ( x ~~ v <-> y ~~ v ) )
52 51 2 imbi12d 
 |-  ( x = y -> ( ( x ~~ v -> ph ) <-> ( y ~~ v -> ch ) ) )
53 52 spvv 
 |-  ( A. x ( x ~~ v -> ph ) -> ( y ~~ v -> ch ) )
54 rspe 
 |-  ( ( v e. _om /\ y ~~ v ) -> E. v e. _om y ~~ v )
55 isfi 
 |-  ( y e. Fin <-> E. v e. _om y ~~ v )
56 54 55 sylibr 
 |-  ( ( v e. _om /\ y ~~ v ) -> y e. Fin )
57 pm2.27 
 |-  ( y ~~ v -> ( ( y ~~ v -> ch ) -> ch ) )
58 57 adantl 
 |-  ( ( v e. _om /\ y ~~ v ) -> ( ( y ~~ v -> ch ) -> ch ) )
59 56 58 6 sylsyld 
 |-  ( ( v e. _om /\ y ~~ v ) -> ( ( y ~~ v -> ch ) -> th ) )
60 53 59 syl5 
 |-  ( ( v e. _om /\ y ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> th ) )
61 vex 
 |-  y e. _V
62 snex 
 |-  { z } e. _V
63 61 62 unex 
 |-  ( y u. { z } ) e. _V
64 63 3 sbcie 
 |-  ( [. ( y u. { z } ) / x ]. ph <-> th )
65 60 64 syl6ibr 
 |-  ( ( v e. _om /\ y ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. ( y u. { z } ) / x ]. ph ) )
66 44 50 65 vtocl 
 |-  ( ( v e. _om /\ ( w \ { z } ) ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) )
67 dfsbcq 
 |-  ( ( ( w \ { z } ) u. { z } ) = w -> ( [. ( ( w \ { z } ) u. { z } ) / x ]. ph <-> [. w / x ]. ph ) )
68 67 imbi2d 
 |-  ( ( ( w \ { z } ) u. { z } ) = w -> ( ( A. x ( x ~~ v -> ph ) -> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) <-> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
69 66 68 syl5ib 
 |-  ( ( ( w \ { z } ) u. { z } ) = w -> ( ( v e. _om /\ ( w \ { z } ) ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
70 38 42 69 3syl 
 |-  ( z e. w -> ( ( v e. _om /\ ( w \ { z } ) ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
71 70 expd 
 |-  ( z e. w -> ( v e. _om -> ( ( w \ { z } ) ~~ v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) ) )
72 71 com12 
 |-  ( v e. _om -> ( z e. w -> ( ( w \ { z } ) ~~ v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) ) )
73 72 adantr 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> ( z e. w -> ( ( w \ { z } ) ~~ v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) ) )
74 37 73 mpdd 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> ( z e. w -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
75 74 exlimdv 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> ( E. z z e. w -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
76 35 75 syl5bi 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> ( w =/= (/) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
77 76 ex 
 |-  ( v e. _om -> ( w ~~ suc v -> ( w =/= (/) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) ) )
78 34 77 mpdd 
 |-  ( v e. _om -> ( w ~~ suc v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
79 78 com23 
 |-  ( v e. _om -> ( A. x ( x ~~ v -> ph ) -> ( w ~~ suc v -> [. w / x ]. ph ) ) )
80 79 alrimdv 
 |-  ( v e. _om -> ( A. x ( x ~~ v -> ph ) -> A. w ( w ~~ suc v -> [. w / x ]. ph ) ) )
81 nfv 
 |-  F/ w ( x ~~ suc v -> ph )
82 nfv 
 |-  F/ x w ~~ suc v
83 nfsbc1v 
 |-  F/ x [. w / x ]. ph
84 82 83 nfim 
 |-  F/ x ( w ~~ suc v -> [. w / x ]. ph )
85 breq1 
 |-  ( x = w -> ( x ~~ suc v <-> w ~~ suc v ) )
86 sbceq1a 
 |-  ( x = w -> ( ph <-> [. w / x ]. ph ) )
87 85 86 imbi12d 
 |-  ( x = w -> ( ( x ~~ suc v -> ph ) <-> ( w ~~ suc v -> [. w / x ]. ph ) ) )
88 81 84 87 cbvalv1 
 |-  ( A. x ( x ~~ suc v -> ph ) <-> A. w ( w ~~ suc v -> [. w / x ]. ph ) )
89 80 88 syl6ibr 
 |-  ( v e. _om -> ( A. x ( x ~~ v -> ph ) -> A. x ( x ~~ suc v -> ph ) ) )
90 10 13 16 20 89 finds1 
 |-  ( w e. _om -> A. x ( x ~~ w -> ph ) )
91 90 19.21bi 
 |-  ( w e. _om -> ( x ~~ w -> ph ) )
92 91 rexlimiv 
 |-  ( E. w e. _om x ~~ w -> ph )
93 7 92 sylbi 
 |-  ( x e. Fin -> ph )
94 4 93 vtoclga 
 |-  ( A e. Fin -> ta )