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=\varnothing \to \left(\phi \leftrightarrow \psi \right)$$
	findcard2.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
	findcard2.3	$$⊢x=y\cup \left\{z\right\}\to \left(\phi \leftrightarrow \theta \right)$$
	findcard2.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
	findcard2.5	$$⊢\psi$$
	findcard2.6	$$⊢y\in \mathrm{Fin}\to \left(\chi \to \theta \right)$$
Assertion	findcard2	$$⊢A\in \mathrm{Fin}\to \tau$$

Proof

Step	Hyp	Ref	Expression
1		findcard2.1	$$⊢x=\varnothing \to \left(\phi \leftrightarrow \psi \right)$$
2		findcard2.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
3		findcard2.3	$$⊢x=y\cup \left\{z\right\}\to \left(\phi \leftrightarrow \theta \right)$$
4		findcard2.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
5		findcard2.5	$$⊢\psi$$
6		findcard2.6	$$⊢y\in \mathrm{Fin}\to \left(\chi \to \theta \right)$$
7		isfi	$$⊢x\in \mathrm{Fin}\leftrightarrow \exists w\in \mathrm{\omega }x\approx w$$
8		breq2	$$⊢w=\varnothing \to \left(x\approx w\leftrightarrow x\approx \varnothing \right)$$
9	8	imbi1d	$$⊢w=\varnothing \to \left(\left(x\approx w\to \phi \right)\leftrightarrow \left(x\approx \varnothing \to \phi \right)\right)$$
10	9	albidv	$$⊢w=\varnothing \to \left(\forall x\left(x\approx w\to \phi \right)\leftrightarrow \forall x\left(x\approx \varnothing \to \phi \right)\right)$$
11		breq2	$$⊢w=v\to \left(x\approx w\leftrightarrow x\approx v\right)$$
12	11	imbi1d	$$⊢w=v\to \left(\left(x\approx w\to \phi \right)\leftrightarrow \left(x\approx v\to \phi \right)\right)$$
13	12	albidv	$$⊢w=v\to \left(\forall x\left(x\approx w\to \phi \right)\leftrightarrow \forall x\left(x\approx v\to \phi \right)\right)$$
14		breq2	$$⊢w=\mathrm{suc}v\to \left(x\approx w\leftrightarrow x\approx \mathrm{suc}v\right)$$
15	14	imbi1d	$$⊢w=\mathrm{suc}v\to \left(\left(x\approx w\to \phi \right)\leftrightarrow \left(x\approx \mathrm{suc}v\to \phi \right)\right)$$
16	15	albidv	$$⊢w=\mathrm{suc}v\to \left(\forall x\left(x\approx w\to \phi \right)\leftrightarrow \forall x\left(x\approx \mathrm{suc}v\to \phi \right)\right)$$
17		en0	$$⊢x\approx \varnothing \leftrightarrow x=\varnothing$$
18	5 1	mpbiri	$$⊢x=\varnothing \to \phi$$
19	17 18	sylbi	$$⊢x\approx \varnothing \to \phi$$
20	19	ax-gen	$$⊢\forall x\left(x\approx \varnothing \to \phi \right)$$
21		rexdif1en	$$⊢\left(v\in \mathrm{\omega }\wedge w\approx \mathrm{suc}v\right)\to \exists z\in w\left(w\setminus \left\{z\right\}\right)\approx v$$
22		snssi	$$⊢z\in w\to \left\{z\right\}\subseteq w$$
23		uncom	$$⊢\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}=\left\{z\right\}\cup \left(w\setminus \left\{z\right\}\right)$$
24		undif	$$⊢\left\{z\right\}\subseteq w\leftrightarrow \left\{z\right\}\cup \left(w\setminus \left\{z\right\}\right)=w$$
25	24	biimpi	$$⊢\left\{z\right\}\subseteq w\to \left\{z\right\}\cup \left(w\setminus \left\{z\right\}\right)=w$$
26	23 25	eqtrid	$$⊢\left\{z\right\}\subseteq w\to \left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}=w$$
27		vex	$$⊢w\in \mathrm{V}$$
28	27	difexi	$$⊢w\setminus \left\{z\right\}\in \mathrm{V}$$
29		breq1	$$⊢y=w\setminus \left\{z\right\}\to \left(y\approx v\leftrightarrow \left(w\setminus \left\{z\right\}\right)\approx v\right)$$
30	29	anbi2d	$$⊢y=w\setminus \left\{z\right\}\to \left(\left(v\in \mathrm{\omega }\wedge y\approx v\right)\leftrightarrow \left(v\in \mathrm{\omega }\wedge \left(w\setminus \left\{z\right\}\right)\approx v\right)\right)$$
31		uneq1	$$⊢y=w\setminus \left\{z\right\}\to y\cup \left\{z\right\}=\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}$$
32	31	sbceq1d	$$⊢y=w\setminus \left\{z\right\}\to \left(\underset{\dot{}}{[}\left(y\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \right)$$
33	32	imbi2d	$$⊢y=w\setminus \left\{z\right\}\to \left(\left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}\left(y\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}\left(\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \right)\right)$$
34	30 33	imbi12d	$$⊢y=w\setminus \left\{z\right\}\to \left(\left(\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}\left(y\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(\left(v\in \mathrm{\omega }\wedge \left(w\setminus \left\{z\right\}\right)\approx v\right)\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}\left(\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
35		breq1	$$⊢x=y\to \left(x\approx v\leftrightarrow y\approx v\right)$$
36	35 2	imbi12d	$$⊢x=y\to \left(\left(x\approx v\to \phi \right)\leftrightarrow \left(y\approx v\to \chi \right)\right)$$
37	36	spvv	$$⊢\forall x\left(x\approx v\to \phi \right)\to \left(y\approx v\to \chi \right)$$
38		rspe	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to \exists v\in \mathrm{\omega }y\approx v$$
39		isfi	$$⊢y\in \mathrm{Fin}\leftrightarrow \exists v\in \mathrm{\omega }y\approx v$$
40	38 39	sylibr	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to y\in \mathrm{Fin}$$
41		pm2.27	$$⊢y\approx v\to \left(\left(y\approx v\to \chi \right)\to \chi \right)$$
42	41	adantl	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to \left(\left(y\approx v\to \chi \right)\to \chi \right)$$
43	40 42 6	sylsyld	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to \left(\left(y\approx v\to \chi \right)\to \theta \right)$$
44	37 43	syl5	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to \left(\forall x\left(x\approx v\to \phi \right)\to \theta \right)$$
45		vex	$$⊢y\in \mathrm{V}$$
46		snex	$$⊢\left\{z\right\}\in \mathrm{V}$$
47	45 46	unex	$$⊢y\cup \left\{z\right\}\in \mathrm{V}$$
48	47 3	sbcie	$$⊢\underset{\dot{}}{[}\left(y\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \theta$$
49	44 48	syl6ibr	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}\left(y\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \right)$$
50	28 34 49	vtocl	$$⊢\left(v\in \mathrm{\omega }\wedge \left(w\setminus \left\{z\right\}\right)\approx v\right)\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}\left(\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \right)$$
51		dfsbcq	$$⊢\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}=w\to \left(\underset{\dot{}}{[}\left(\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
52	51	imbi2d	$$⊢\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}=w\to \left(\left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}\left(\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)$$
53	50 52	syl5ib	$$⊢\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}=w\to \left(\left(v\in \mathrm{\omega }\wedge \left(w\setminus \left\{z\right\}\right)\approx v\right)\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)$$
54	22 26 53	3syl	$$⊢z\in w\to \left(\left(v\in \mathrm{\omega }\wedge \left(w\setminus \left\{z\right\}\right)\approx v\right)\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)$$
55	54	expd	$$⊢z\in w\to \left(v\in \mathrm{\omega }\to \left(\left(w\setminus \left\{z\right\}\right)\approx v\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
56	55	com12	$$⊢v\in \mathrm{\omega }\to \left(z\in w\to \left(\left(w\setminus \left\{z\right\}\right)\approx v\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
57	56	rexlimdv	$$⊢v\in \mathrm{\omega }\to \left(\exists z\in w\left(w\setminus \left\{z\right\}\right)\approx v\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)$$
58	57	adantr	$$⊢\left(v\in \mathrm{\omega }\wedge w\approx \mathrm{suc}v\right)\to \left(\exists z\in w\left(w\setminus \left\{z\right\}\right)\approx v\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)$$
59	21 58	mpd	$$⊢\left(v\in \mathrm{\omega }\wedge w\approx \mathrm{suc}v\right)\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
60	59	ex	$$⊢v\in \mathrm{\omega }\to \left(w\approx \mathrm{suc}v\to \left(\forall x\left(x\approx v\to \phi \right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)$$
61	60	com23	$$⊢v\in \mathrm{\omega }\to \left(\forall x\left(x\approx v\to \phi \right)\to \left(w\approx \mathrm{suc}v\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)$$
62	61	alrimdv	$$⊢v\in \mathrm{\omega }\to \left(\forall x\left(x\approx v\to \phi \right)\to \forall w\left(w\approx \mathrm{suc}v\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)$$
63		nfv	$$⊢Ⅎw\left(x\approx \mathrm{suc}v\to \phi \right)$$
64		nfv	$$⊢Ⅎxw\approx \mathrm{suc}v$$
65		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi$$
66	64 65	nfim	$$⊢Ⅎx\left(w\approx \mathrm{suc}v\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
67		breq1	$$⊢x=w\to \left(x\approx \mathrm{suc}v\leftrightarrow w\approx \mathrm{suc}v\right)$$
68		sbceq1a	$$⊢x=w\to \left(\phi \leftrightarrow \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
69	67 68	imbi12d	$$⊢x=w\to \left(\left(x\approx \mathrm{suc}v\to \phi \right)\leftrightarrow \left(w\approx \mathrm{suc}v\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)\right)$$
70	63 66 69	cbvalv1	$$⊢\forall x\left(x\approx \mathrm{suc}v\to \phi \right)\leftrightarrow \forall w\left(w\approx \mathrm{suc}v\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
71	62 70	syl6ibr	$$⊢v\in \mathrm{\omega }\to \left(\forall x\left(x\approx v\to \phi \right)\to \forall x\left(x\approx \mathrm{suc}v\to \phi \right)\right)$$
72	10 13 16 20 71	finds1	$$⊢w\in \mathrm{\omega }\to \forall x\left(x\approx w\to \phi \right)$$
73	72	19.21bi	$$⊢w\in \mathrm{\omega }\to \left(x\approx w\to \phi \right)$$
74	73	rexlimiv	$$⊢\exists w\in \mathrm{\omega }x\approx w\to \phi$$
75	7 74	sylbi	$$⊢x\in \mathrm{Fin}\to \phi$$
76	4 75	vtoclga	$$⊢A\in \mathrm{Fin}\to \tau$$