Theorem findcard2 8842

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 5258. (Revised by BTernaryTau, 26-Aug-2024.)

Hypotheses

Ref	Expression
findcard2.1	⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
findcard2.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
findcard2.3	⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))
findcard2.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
findcard2.5	⊢ 𝜓
findcard2.6	⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))

Assertion

Ref	Expression
findcard2	⊢ (𝐴 ∈ Fin → 𝜏)

Distinct variable groups:   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝑥,𝐴   𝜑,𝑦,𝑧   𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦,𝑧)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)   𝐴(𝑦,𝑧)

Proof of Theorem findcard2

Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		findcard2.4	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
2		isfi 8652	. . 3 ⊢ (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥 ≈ 𝑤)
3		breq2 5057	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ ∅))
4	3	imbi1d 345	. . . . . . 7 ⊢ (𝑤 = ∅ → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
5	4	albidv 1928	. . . . . 6 ⊢ (𝑤 = ∅ → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6		breq2 5057	. . . . . . . 8 ⊢ (𝑤 = 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑣))
7	6	imbi1d 345	. . . . . . 7 ⊢ (𝑤 = 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑣 → 𝜑)))
8	7	albidv 1928	. . . . . 6 ⊢ (𝑤 = 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑣 → 𝜑)))
9		breq2 5057	. . . . . . . 8 ⊢ (𝑤 = suc 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ suc 𝑣))
10	9	imbi1d 345	. . . . . . 7 ⊢ (𝑤 = suc 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ suc 𝑣 → 𝜑)))
11	10	albidv 1928	. . . . . 6 ⊢ (𝑤 = suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
12		en0 8691	. . . . . . . 8 ⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13		findcard2.5	. . . . . . . . 9 ⊢ 𝜓
14		findcard2.1	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
15	13, 14	mpbiri 261	. . . . . . . 8 ⊢ (𝑥 = ∅ → 𝜑)
16	12, 15	sylbi 220	. . . . . . 7 ⊢ (𝑥 ≈ ∅ → 𝜑)
17	16	ax-gen 1803	. . . . . 6 ⊢ ∀𝑥(𝑥 ≈ ∅ → 𝜑)
18		rexdif1en 8839	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → ∃𝑧 ∈ 𝑤 (𝑤 ∖ {𝑧}) ≈ 𝑣)
19		snssi 4721	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑤 → {𝑧} ⊆ 𝑤)
20		uncom 4067	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = ({𝑧} ∪ (𝑤 ∖ {𝑧}))
21		undif 4396	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑧} ⊆ 𝑤 ↔ ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
22	21	biimpi 219	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑤 → ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
23	20, 22	eqtrid 2789	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ⊆ 𝑤 → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
24		vex 3412	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑤 ∈ V
25	24	difexi 5221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∖ {𝑧}) ∈ V
26		breq1 5056	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ≈ 𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
27	26	anbi2d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
28		uneq1 4070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
29	28	sbceq1d 3699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
30	29	imbi2d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
31	27, 30	imbi12d 348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
32		breq1 5056	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑣 ↔ 𝑦 ≈ 𝑣))
33		findcard2.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
34	32, 33	imbi12d 348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑣 → 𝜑) ↔ (𝑦 ≈ 𝑣 → 𝜒)))
35	34	spvv 2005	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑦 ≈ 𝑣 → 𝜒))
36		rspe 3223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
37		isfi 8652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
38	36, 37	sylibr 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → 𝑦 ∈ Fin)
39		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ≈ 𝑣 → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
40	39	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
41		findcard2.6	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))
42	38, 40, 41	sylsyld 61	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜃))
43	35, 42	syl5 34	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → 𝜃))
44		vex 3412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
45		snex 5324	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑧} ∈ V
46	44, 45	unex 7531	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∪ {𝑧}) ∈ V
47		findcard2.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))
48	46, 47	sbcie 3737	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ 𝜃)
49	43, 48	syl6ibr 255	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
50	25, 31, 49	vtocl 3474	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
51		dfsbcq 3696	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑))
52	51	imbi2d 344	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
53	50, 52	syl5ib 247	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
54	19, 23, 53	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
55	54	expd 419	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝑤 → (𝑣 ∈ ω → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
56	55	com12 32	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ω → (𝑧 ∈ 𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
57	56	rexlimdv 3202	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ω → (∃𝑧 ∈ 𝑤 (𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
58	57	adantr 484	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 ∈ 𝑤 (𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
59	18, 58	mpd 15	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))
60	59	ex 416	. . . . . . . . 9 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
61	60	com23 86	. . . . . . . 8 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
62	61	alrimdv 1937	. . . . . . 7 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
63		nfv 1922	. . . . . . . 8 ⊢ Ⅎ𝑤(𝑥 ≈ suc 𝑣 → 𝜑)
64		nfv 1922	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑤 ≈ suc 𝑣
65		nfsbc1v 3714	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
66	64, 65	nfim 1904	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)
67		breq1 5056	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣 ↔ 𝑤 ≈ suc 𝑣))
68		sbceq1a 3705	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑))
69	67, 68	imbi12d 348	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣 → 𝜑) ↔ (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
70	63, 66, 69	cbvalv1 2341	. . . . . . 7 ⊢ (∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑))
71	62, 70	syl6ibr 255	. . . . . 6 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
72	5, 8, 11, 17, 71	finds1 7679	. . . . 5 ⊢ (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))
73	72	19.21bi 2186	. . . 4 ⊢ (𝑤 ∈ ω → (𝑥 ≈ 𝑤 → 𝜑))
74	73	rexlimiv 3199	. . 3 ⊢ (∃𝑤 ∈ ω 𝑥 ≈ 𝑤 → 𝜑)
75	2, 74	sylbi 220	. 2 ⊢ (𝑥 ∈ Fin → 𝜑)
76	1, 75	vtoclga 3489	1 ⊢ (𝐴 ∈ Fin → 𝜏)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541   = wceq 1543   ∈ wcel 2110  ∃wrex 3062  [wsbc 3694   ∖ cdif 3863   ∪ cun 3864   ⊆ wss 3866  ∅c0 4237  {csn 4541   class class class wbr 5053  suc csuc 6215  ωcom 7644   ≈ cen 8623  Fincfn 8626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-om 7645  df-en 8627  df-fin 8630

This theorem is referenced by:  findcard2s  8843  ssfi  8851  imafi  8853  pwfi  8856  cnvfi  8857  fnfi  8858  frfi  8916  iunfi  8964  finsschain  8983  infdiffi  9273  fin1a2lem10  10023  wunfi  10335  rexfiuz  14911  modfsummod  15358  lcmfunsnlem  16198  lcmfun  16202  drsdirfi  17812  fiuncmp  22301  finiunmbl  24441  fineqvac  32779  mbfresfi  35560  heibor1lem  35704  pclfinclN  37701