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 )