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) Avoid ax-pow . (Revised by BTernaryTau, 26-Aug-2024)

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 rexdif1en 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> E. z e. w ( w \ { z } ) ~~ v )
22 snssi 
 |-  ( z e. w -> { z } C_ w )
23 uncom 
 |-  ( ( w \ { z } ) u. { z } ) = ( { z } u. ( w \ { z } ) )
24 undif 
 |-  ( { z } C_ w <-> ( { z } u. ( w \ { z } ) ) = w )
25 24 biimpi 
 |-  ( { z } C_ w -> ( { z } u. ( w \ { z } ) ) = w )
26 23 25 syl5eq 
 |-  ( { z } C_ w -> ( ( w \ { z } ) u. { z } ) = w )
27 vex 
 |-  w e. _V
28 27 difexi 
 |-  ( w \ { z } ) e. _V
29 breq1 
 |-  ( y = ( w \ { z } ) -> ( y ~~ v <-> ( w \ { z } ) ~~ v ) )
30 29 anbi2d 
 |-  ( y = ( w \ { z } ) -> ( ( v e. _om /\ y ~~ v ) <-> ( v e. _om /\ ( w \ { z } ) ~~ v ) ) )
31 uneq1 
 |-  ( y = ( w \ { z } ) -> ( y u. { z } ) = ( ( w \ { z } ) u. { z } ) )
32 31 sbceq1d 
 |-  ( y = ( w \ { z } ) -> ( [. ( y u. { z } ) / x ]. ph <-> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) )
33 32 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 ) ) )
34 30 33 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 ) ) ) )
35 breq1 
 |-  ( x = y -> ( x ~~ v <-> y ~~ v ) )
36 35 2 imbi12d 
 |-  ( x = y -> ( ( x ~~ v -> ph ) <-> ( y ~~ v -> ch ) ) )
37 36 spvv 
 |-  ( A. x ( x ~~ v -> ph ) -> ( y ~~ v -> ch ) )
38 rspe 
 |-  ( ( v e. _om /\ y ~~ v ) -> E. v e. _om y ~~ v )
39 isfi 
 |-  ( y e. Fin <-> E. v e. _om y ~~ v )
40 38 39 sylibr 
 |-  ( ( v e. _om /\ y ~~ v ) -> y e. Fin )
41 pm2.27 
 |-  ( y ~~ v -> ( ( y ~~ v -> ch ) -> ch ) )
42 41 adantl 
 |-  ( ( v e. _om /\ y ~~ v ) -> ( ( y ~~ v -> ch ) -> ch ) )
43 40 42 6 sylsyld 
 |-  ( ( v e. _om /\ y ~~ v ) -> ( ( y ~~ v -> ch ) -> th ) )
44 37 43 syl5 
 |-  ( ( v e. _om /\ y ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> th ) )
45 vex 
 |-  y e. _V
46 snex 
 |-  { z } e. _V
47 45 46 unex 
 |-  ( y u. { z } ) e. _V
48 47 3 sbcie 
 |-  ( [. ( y u. { z } ) / x ]. ph <-> th )
49 44 48 syl6ibr 
 |-  ( ( v e. _om /\ y ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. ( y u. { z } ) / x ]. ph ) )
50 28 34 49 vtocl 
 |-  ( ( v e. _om /\ ( w \ { z } ) ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) )
51 dfsbcq 
 |-  ( ( ( w \ { z } ) u. { z } ) = w -> ( [. ( ( w \ { z } ) u. { z } ) / x ]. ph <-> [. w / x ]. ph ) )
52 51 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 ) ) )
53 50 52 syl5ib 
 |-  ( ( ( w \ { z } ) u. { z } ) = w -> ( ( v e. _om /\ ( w \ { z } ) ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
54 22 26 53 3syl 
 |-  ( z e. w -> ( ( v e. _om /\ ( w \ { z } ) ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
55 54 expd 
 |-  ( z e. w -> ( v e. _om -> ( ( w \ { z } ) ~~ v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) ) )
56 55 com12 
 |-  ( v e. _om -> ( z e. w -> ( ( w \ { z } ) ~~ v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) ) )
57 56 rexlimdv 
 |-  ( v e. _om -> ( E. z e. w ( w \ { z } ) ~~ v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
58 57 adantr 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> ( E. z e. w ( w \ { z } ) ~~ v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
59 21 58 mpd 
 |-  ( ( v e. _om /\ w ~~ suc v ) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) )
60 59 ex 
 |-  ( v e. _om -> ( w ~~ suc v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
61 60 com23 
 |-  ( v e. _om -> ( A. x ( x ~~ v -> ph ) -> ( w ~~ suc v -> [. w / x ]. ph ) ) )
62 61 alrimdv 
 |-  ( v e. _om -> ( A. x ( x ~~ v -> ph ) -> A. w ( w ~~ suc v -> [. w / x ]. ph ) ) )
63 nfv 
 |-  F/ w ( x ~~ suc v -> ph )
64 nfv 
 |-  F/ x w ~~ suc v
65 nfsbc1v 
 |-  F/ x [. w / x ]. ph
66 64 65 nfim 
 |-  F/ x ( w ~~ suc v -> [. w / x ]. ph )
67 breq1 
 |-  ( x = w -> ( x ~~ suc v <-> w ~~ suc v ) )
68 sbceq1a 
 |-  ( x = w -> ( ph <-> [. w / x ]. ph ) )
69 67 68 imbi12d 
 |-  ( x = w -> ( ( x ~~ suc v -> ph ) <-> ( w ~~ suc v -> [. w / x ]. ph ) ) )
70 63 66 69 cbvalv1 
 |-  ( A. x ( x ~~ suc v -> ph ) <-> A. w ( w ~~ suc v -> [. w / x ]. ph ) )
71 62 70 syl6ibr 
 |-  ( v e. _om -> ( A. x ( x ~~ v -> ph ) -> A. x ( x ~~ suc v -> ph ) ) )
72 10 13 16 20 71 finds1 
 |-  ( w e. _om -> A. x ( x ~~ w -> ph ) )
73 72 19.21bi 
 |-  ( w e. _om -> ( x ~~ w -> ph ) )
74 73 rexlimiv 
 |-  ( E. w e. _om x ~~ w -> ph )
75 7 74 sylbi 
 |-  ( x e. Fin -> ph )
76 4 75 vtoclga 
 |-  ( A e. Fin -> ta )