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		nnon	$$⊢v\in \mathrm{\omega }\to v\in \mathrm{On}$$
22		rexdif1en	$$⊢\left(v\in \mathrm{On}\wedge w\approx \mathrm{suc}v\right)\to \exists z\in w\left(w\setminus \left\{z\right\}\right)\approx v$$
23	21 22	sylan	$$⊢\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$$
24		snssi	$$⊢z\in w\to \left\{z\right\}\subseteq w$$
25		uncom	$$⊢\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}=\left\{z\right\}\cup \left(w\setminus \left\{z\right\}\right)$$
26		undif	$$⊢\left\{z\right\}\subseteq w\leftrightarrow \left\{z\right\}\cup \left(w\setminus \left\{z\right\}\right)=w$$
27	26	biimpi	$$⊢\left\{z\right\}\subseteq w\to \left\{z\right\}\cup \left(w\setminus \left\{z\right\}\right)=w$$
28	25 27	eqtrid	$$⊢\left\{z\right\}\subseteq w\to \left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}=w$$
29		vex	$$⊢w\in \mathrm{V}$$
30	29	difexi	$$⊢w\setminus \left\{z\right\}\in \mathrm{V}$$
31		breq1	$$⊢y=w\setminus \left\{z\right\}\to \left(y\approx v\leftrightarrow \left(w\setminus \left\{z\right\}\right)\approx v\right)$$
32	31	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)$$
33		uneq1	$$⊢y=w\setminus \left\{z\right\}\to y\cup \left\{z\right\}=\left(w\setminus \left\{z\right\}\right)\cup \left\{z\right\}$$
34	33	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)$$
35	34	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)$$
36	32 35	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)$$
37		breq1	$$⊢x=y\to \left(x\approx v\leftrightarrow y\approx v\right)$$
38	37 2	imbi12d	$$⊢x=y\to \left(\left(x\approx v\to \phi \right)\leftrightarrow \left(y\approx v\to \chi \right)\right)$$
39	38	spvv	$$⊢\forall x\left(x\approx v\to \phi \right)\to \left(y\approx v\to \chi \right)$$
40		rspe	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to \exists v\in \mathrm{\omega }y\approx v$$
41		isfi	$$⊢y\in \mathrm{Fin}\leftrightarrow \exists v\in \mathrm{\omega }y\approx v$$
42	40 41	sylibr	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to y\in \mathrm{Fin}$$
43		pm2.27	$$⊢y\approx v\to \left(\left(y\approx v\to \chi \right)\to \chi \right)$$
44	43	adantl	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to \left(\left(y\approx v\to \chi \right)\to \chi \right)$$
45	42 44 6	sylsyld	$$⊢\left(v\in \mathrm{\omega }\wedge y\approx v\right)\to \left(\left(y\approx v\to \chi \right)\to \theta \right)$$
46	39 45	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)$$
47		vex	$$⊢y\in \mathrm{V}$$
48		vsnex	$$⊢\left\{z\right\}\in \mathrm{V}$$
49	47 48	unex	$$⊢y\cup \left\{z\right\}\in \mathrm{V}$$
50	49 3	sbcie	$$⊢\underset{\dot{}}{[}\left(y\cup \left\{z\right\}\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \theta$$
51	46 50	imbitrrdi	$$⊢\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)$$
52	30 36 51	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)$$
53		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)$$
54	53	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)$$
55	52 54	imbitrid	$$⊢\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)$$
56	24 28 55	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)$$
57	56	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)$$
58	57	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)$$
59	58	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)$$
60	59	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)$$
61	23 60	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)$$
62	61	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)$$
63	62	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)$$
64	63	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)$$
65		nfv	$$⊢Ⅎw\left(x\approx \mathrm{suc}v\to \phi \right)$$
66		nfv	$$⊢Ⅎxw\approx \mathrm{suc}v$$
67		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi$$
68	66 67	nfim	$$⊢Ⅎx\left(w\approx \mathrm{suc}v\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
69		breq1	$$⊢x=w\to \left(x\approx \mathrm{suc}v\leftrightarrow w\approx \mathrm{suc}v\right)$$
70		sbceq1a	$$⊢x=w\to \left(\phi \leftrightarrow \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
71	69 70	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)$$
72	65 68 71	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)$$
73	64 72	imbitrrdi	$$⊢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)$$
74	10 13 16 20 73	finds1	$$⊢w\in \mathrm{\omega }\to \forall x\left(x\approx w\to \phi \right)$$
75	74	19.21bi	$$⊢w\in \mathrm{\omega }\to \left(x\approx w\to \phi \right)$$
76	75	rexlimiv	$$⊢\exists w\in \mathrm{\omega }x\approx w\to \phi$$
77	7 76	sylbi	$$⊢x\in \mathrm{Fin}\to \phi$$
78	4 77	vtoclga	$$⊢A\in \mathrm{Fin}\to \tau$$