Theorem findcard2 7186

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
findcard2	|- ( A e. Fin -> ta )

Distinct variable groups:   x, y, z, A   ps, x   ch, x   th, x   ta, x   ph, y, z

Allowed substitution hints:   ph( x)   ps( y, z)   ch( y, z)   th( y, z)   ta( y, z)

Proof of Theorem findcard2

Dummy variables w v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		findcard2.4	. 2 |- ( x = A -> ( ph <-> ta ) )
2		isfi 7040	. . 3 |- ( x e. Fin <-> E. w e. om x ~~ w )
3		breq2 4132	. . . . . . . 8 |- ( w = (/) -> ( x ~~ w <-> x ~~ (/) ) )
4	3	imbi1d 231	. . . . . . 7 |- ( w = (/) -> ( ( x ~~ w -> ph ) <-> ( x ~~ (/) -> ph ) ) )
5	4	albidv 1877	. . . . . 6 |- ( w = (/) -> ( A. x ( x ~~ w -> ph ) <-> A. x ( x ~~ (/) -> ph ) ) )
6		breq2 4132	. . . . . . . 8 |- ( w = v -> ( x ~~ w <-> x ~~ v ) )
7	6	imbi1d 231	. . . . . . 7 |- ( w = v -> ( ( x ~~ w -> ph ) <-> ( x ~~ v -> ph ) ) )
8	7	albidv 1877	. . . . . 6 |- ( w = v -> ( A. x ( x ~~ w -> ph ) <-> A. x ( x ~~ v -> ph ) ) )
9		breq2 4132	. . . . . . . 8 |- ( w = suc v -> ( x ~~ w <-> x ~~ suc v ) )
10	9	imbi1d 231	. . . . . . 7 |- ( w = suc v -> ( ( x ~~ w -> ph ) <-> ( x ~~ suc v -> ph ) ) )
11	10	albidv 1877	. . . . . 6 |- ( w = suc v -> ( A. x ( x ~~ w -> ph ) <-> A. x ( x ~~ suc v -> ph ) ) )
12		en0 7075	. . . . . . . 8 |- ( x ~~ (/) <-> x = (/) )
13		findcard2.5	. . . . . . . . 9 |- ps
14		findcard2.1	. . . . . . . . 9 |- ( x = (/) -> ( ph <-> ps ) )
15	13, 14	mpbiri 168	. . . . . . . 8 |- ( x = (/) -> ph )
16	12, 15	sylbi 121	. . . . . . 7 |- ( x ~~ (/) -> ph )
17	16	ax-gen 1502	. . . . . 6 |- A. x ( x ~~ (/) -> ph )
18		peano3 4741	. . . . . . . . . . . . 13 |- ( v e. om -> suc v =/= (/) )
19	18	adantr 276	. . . . . . . . . . . 12 |- ( ( v e. om /\ w ~~ suc v ) -> suc v =/= (/) )
20		breq1 4131	. . . . . . . . . . . . . . . 16 |- ( w = (/) -> ( w ~~ suc v <-> (/) ~~ suc v ) )
21	20	anbi2d 468	. . . . . . . . . . . . . . 15 |- ( w = (/) -> ( ( v e. om /\ w ~~ suc v ) <-> ( v e. om /\ (/) ~~ suc v ) ) )
22		peano1 4739	. . . . . . . . . . . . . . . . . 18 |- (/) e. om
23		peano2 4740	. . . . . . . . . . . . . . . . . 18 |- ( v e. om -> suc v e. om )
24		nneneq 7151	. . . . . . . . . . . . . . . . . 18 |- ( ( (/) e. om /\ suc v e. om ) -> ( (/) ~~ suc v <-> (/) = suc v ) )
25	22, 23, 24	sylancr 418	. . . . . . . . . . . . . . . . 17 |- ( v e. om -> ( (/) ~~ suc v <-> (/) = suc v ) )
26	25	biimpa 296	. . . . . . . . . . . . . . . 16 |- ( ( v e. om /\ (/) ~~ suc v ) -> (/) = suc v )
27	26	eqcomd 2244	. . . . . . . . . . . . . . 15 |- ( ( v e. om /\ (/) ~~ suc v ) -> suc v = (/) )
28	21, 27	biimtrdi 163	. . . . . . . . . . . . . 14 |- ( w = (/) -> ( ( v e. om /\ w ~~ suc v ) -> suc v = (/) ) )
29	28	com12 30	. . . . . . . . . . . . 13 |- ( ( v e. om /\ w ~~ suc v ) -> ( w = (/) -> suc v = (/) ) )
30	29	necon3d 2464	. . . . . . . . . . . 12 |- ( ( v e. om /\ w ~~ suc v ) -> ( suc v =/= (/) -> w =/= (/) ) )
31	19, 30	mpd 13	. . . . . . . . . . 11 |- ( ( v e. om /\ w ~~ suc v ) -> w =/= (/) )
32	31	ex 115	. . . . . . . . . 10 |- ( v e. om -> ( w ~~ suc v -> w =/= (/) ) )
33		nnfi 7167	. . . . . . . . . . . . . . . 16 |- ( suc v e. om -> suc v e. Fin )
34	23, 33	syl 14	. . . . . . . . . . . . . . 15 |- ( v e. om -> suc v e. Fin )
35	34	adantr 276	. . . . . . . . . . . . . 14 |- ( ( v e. om /\ w ~~ suc v ) -> suc v e. Fin )
36		enfi 7168	. . . . . . . . . . . . . . 15 |- ( w ~~ suc v -> ( w e. Fin <-> suc v e. Fin ) )
37	36	adantl 277	. . . . . . . . . . . . . 14 |- ( ( v e. om /\ w ~~ suc v ) -> ( w e. Fin <-> suc v e. Fin ) )
38	35, 37	mpbird 167	. . . . . . . . . . . . 13 |- ( ( v e. om /\ w ~~ suc v ) -> w e. Fin )
39		fin0 7182	. . . . . . . . . . . . 13 |- ( w e. Fin -> ( w =/= (/) <-> E. z z e. w ) )
40	38, 39	syl 14	. . . . . . . . . . . 12 |- ( ( v e. om /\ w ~~ suc v ) -> ( w =/= (/) <-> E. z z e. w ) )
41		simpll 531	. . . . . . . . . . . . . . 15 |- ( ( ( v e. om /\ w ~~ suc v ) /\ z e. w ) -> v e. om )
42		dif1en 7176	. . . . . . . . . . . . . . . 16 |- ( ( v e. om /\ w ~~ suc v /\ z e. w ) -> ( w \ { z } ) ~~ v )
43	42	3expa 1234	. . . . . . . . . . . . . . 15 |- ( ( ( v e. om /\ w ~~ suc v ) /\ z e. w ) -> ( w \ { z } ) ~~ v )
44		fidifsnid 7166	. . . . . . . . . . . . . . . . 17 |- ( ( w e. Fin /\ z e. w ) -> ( ( w \ { z } ) u. { z } ) = w )
45	38, 44	sylan 283	. . . . . . . . . . . . . . . 16 |- ( ( ( v e. om /\ w ~~ suc v ) /\ z e. w ) -> ( ( w \ { z } ) u. { z } ) = w )
46		vex 2824	. . . . . . . . . . . . . . . . . . 19 |- w e. _V
47		difexg 4273	. . . . . . . . . . . . . . . . . . 19 |- ( w e. _V -> ( w \ { z } ) e. _V )
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( w \ { z } ) e. _V
49		breq1 4131	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( w \ { z } ) -> ( y ~~ v <-> ( w \ { z } ) ~~ v ) )
50	49	anbi2d 468	. . . . . . . . . . . . . . . . . . 19 |- ( y = ( w \ { z } ) -> ( ( v e. om /\ y ~~ v ) <-> ( v e. om /\ ( w \ { z } ) ~~ v ) ) )
51		uneq1 3376	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( w \ { z } ) -> ( y u. { z } ) = ( ( w \ { z } ) u. { z } ) )
52	51	sbceq1d 3056	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( w \ { z } ) -> ( [. ( y u. { z } ) / x ]. ph <-> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) )
53	52	imbi2d 230	. . . . . . . . . . . . . . . . . . 19 |- ( y = ( w \ { z } ) -> ( ( A. x ( x ~~ v -> ph ) -> [. ( y u. { z } ) / x ]. ph ) <-> ( A. x ( x ~~ v -> ph ) -> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) ) )
54	50, 53	imbi12d 234	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) )
55		breq1 4131	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( x ~~ v <-> y ~~ v ) )
56		findcard2.2	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( ph <-> ch ) )
57	55, 56	imbi12d 234	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( ( x ~~ v -> ph ) <-> ( y ~~ v -> ch ) ) )
58	57	spv 1913	. . . . . . . . . . . . . . . . . . . 20 |- ( A. x ( x ~~ v -> ph ) -> ( y ~~ v -> ch ) )
59		rspe 2599	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( v e. om /\ y ~~ v ) -> E. v e. om y ~~ v )
60		isfi 7040	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. Fin <-> E. v e. om y ~~ v )
61	59, 60	sylibr 134	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( v e. om /\ y ~~ v ) -> y e. Fin )
62		pm2.27 40	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y ~~ v -> ( ( y ~~ v -> ch ) -> ch ) )
63	62	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( v e. om /\ y ~~ v ) -> ( ( y ~~ v -> ch ) -> ch ) )
64		findcard2.6	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. Fin -> ( ch -> th ) )
65	61, 63, 64	sylsyld 58	. . . . . . . . . . . . . . . . . . . 20 |- ( ( v e. om /\ y ~~ v ) -> ( ( y ~~ v -> ch ) -> th ) )
66	58, 65	syl5 32	. . . . . . . . . . . . . . . . . . 19 |- ( ( v e. om /\ y ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> th ) )
67		vex 2824	. . . . . . . . . . . . . . . . . . . . 21 |- y e. _V
68		vex 2824	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. _V
69	68	snex 4320	. . . . . . . . . . . . . . . . . . . . 21 |- { z } e. _V
70	67, 69	unex 4585	. . . . . . . . . . . . . . . . . . . 20 |- ( y u. { z } ) e. _V
71		findcard2.3	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( y u. { z } ) -> ( ph <-> th ) )
72	70, 71	sbcie 3086	. . . . . . . . . . . . . . . . . . 19 |- ( [. ( y u. { z } ) / x ]. ph <-> th )
73	66, 72	imbitrrdi 162	. . . . . . . . . . . . . . . . . 18 |- ( ( v e. om /\ y ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. ( y u. { z } ) / x ]. ph ) )
74	48, 54, 73	vtocl 2877	. . . . . . . . . . . . . . . . 17 |- ( ( v e. om /\ ( w \ { z } ) ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) )
75		dfsbcq 3053	. . . . . . . . . . . . . . . . . 18 |- ( ( ( w \ { z } ) u. { z } ) = w -> ( [. ( ( w \ { z } ) u. { z } ) / x ]. ph <-> [. w / x ]. ph ) )
76	75	imbi2d 230	. . . . . . . . . . . . . . . . 17 |- ( ( ( w \ { z } ) u. { z } ) = w -> ( ( A. x ( x ~~ v -> ph ) -> [. ( ( w \ { z } ) u. { z } ) / x ]. ph ) <-> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
77	74, 76	imbitrid 154	. . . . . . . . . . . . . . . 16 |- ( ( ( w \ { z } ) u. { z } ) = w -> ( ( v e. om /\ ( w \ { z } ) ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
78	45, 77	syl 14	. . . . . . . . . . . . . . 15 |- ( ( ( v e. om /\ w ~~ suc v ) /\ z e. w ) -> ( ( v e. om /\ ( w \ { z } ) ~~ v ) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
79	41, 43, 78	mp2and 437	. . . . . . . . . . . . . 14 |- ( ( ( v e. om /\ w ~~ suc v ) /\ z e. w ) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) )
80	79	ex 115	. . . . . . . . . . . . 13 |- ( ( v e. om /\ w ~~ suc v ) -> ( z e. w -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
81	80	exlimdv 1872	. . . . . . . . . . . 12 |- ( ( v e. om /\ w ~~ suc v ) -> ( E. z z e. w -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
82	40, 81	sylbid 150	. . . . . . . . . . 11 |- ( ( v e. om /\ w ~~ suc v ) -> ( w =/= (/) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
83	82	ex 115	. . . . . . . . . 10 |- ( v e. om -> ( w ~~ suc v -> ( w =/= (/) -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) ) )
84	32, 83	mpdd 41	. . . . . . . . 9 |- ( v e. om -> ( w ~~ suc v -> ( A. x ( x ~~ v -> ph ) -> [. w / x ]. ph ) ) )
85	84	com23 78	. . . . . . . 8 |- ( v e. om -> ( A. x ( x ~~ v -> ph ) -> ( w ~~ suc v -> [. w / x ]. ph ) ) )
86	85	alrimdv 1929	. . . . . . 7 |- ( v e. om -> ( A. x ( x ~~ v -> ph ) -> A. w ( w ~~ suc v -> [. w / x ]. ph ) ) )
87		nfv 1581	. . . . . . . 8 |- F/ w ( x ~~ suc v -> ph )
88		nfv 1581	. . . . . . . . 9 |- F/ x w ~~ suc v
89		nfsbc1v 3070	. . . . . . . . 9 |- F/ x [. w / x ]. ph
90	88, 89	nfim 1625	. . . . . . . 8 |- F/ x ( w ~~ suc v -> [. w / x ]. ph )
91		breq1 4131	. . . . . . . . 9 |- ( x = w -> ( x ~~ suc v <-> w ~~ suc v ) )
92		sbceq1a 3061	. . . . . . . . 9 |- ( x = w -> ( ph <-> [. w / x ]. ph ) )
93	91, 92	imbi12d 234	. . . . . . . 8 |- ( x = w -> ( ( x ~~ suc v -> ph ) <-> ( w ~~ suc v -> [. w / x ]. ph ) ) )
94	87, 90, 93	cbval 1807	. . . . . . 7 |- ( A. x ( x ~~ suc v -> ph ) <-> A. w ( w ~~ suc v -> [. w / x ]. ph ) )
95	86, 94	imbitrrdi 162	. . . . . 6 |- ( v e. om -> ( A. x ( x ~~ v -> ph ) -> A. x ( x ~~ suc v -> ph ) ) )
96	5, 8, 11, 17, 95	finds1 4747	. . . . 5 |- ( w e. om -> A. x ( x ~~ w -> ph ) )
97	96	19.21bi 1611	. . . 4 |- ( w e. om -> ( x ~~ w -> ph ) )
98	97	rexlimiv 2662	. . 3 |- ( E. w e. om x ~~ w -> ph )
99	2, 98	sylbi 121	. 2 |- ( x e. Fin -> ph )
100	1, 99	vtoclga 2889	1 |- ( A e. Fin -> ta )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1400   = wceq 1402   E.wex 1545   e. wcel 2209   =/= wne 2420   E.wrex 2529   _Vcvv 2821   [.wsbc 3051   \ cdif 3217   u. cun 3218   (/)c0 3520   {csn 3708   class class class wbr 4128   suc csuc 4508   omcom 4735   ~~ cen 7013   Fincfn 7015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4244  ax-sep 4247  ax-nul 4257  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682  ax-iinf 4733

This theorem depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-int 3969  df-iun 4012  df-br 4129  df-opab 4191  df-mpt 4192  df-tr 4228  df-id 4436  df-iord 4509  df-on 4511  df-suc 4514  df-iom 4736  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382  df-fv 5383  df-er 6800  df-en 7016  df-fin 7018

This theorem is referenced by:  finomni  7473  rexfiuz  11736  fimaxre2  11974