This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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