Theorem findcard

Description: Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step	Hyp	Ref	Expression
1		findcard.1	⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
2		findcard.2	⊢ ( 𝑥 = ( 𝑦 ∖ { 𝑧 } ) → ( 𝜑 ↔ 𝜒 ) )
3		findcard.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜃 ) )
4		findcard.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5		findcard.5	⊢ 𝜓
6		findcard.6	⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑧 ∈ 𝑦 𝜒 → 𝜃 ) )
7		isfi	⊢ ( 𝑥 ∈ Fin ↔ ∃ 𝑤 ∈ ω 𝑥 ≈ 𝑤 )
8		breq2	⊢ ( 𝑤 = ∅ → ( 𝑥 ≈ 𝑤 ↔ 𝑥 ≈ ∅ ) )
9	8	imbi1d	⊢ ( 𝑤 = ∅ → ( ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ( 𝑥 ≈ ∅ → 𝜑 ) ) )
10	9	albidv	⊢ ( 𝑤 = ∅ → ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ≈ ∅ → 𝜑 ) ) )
11		breq2	⊢ ( 𝑤 = 𝑣 → ( 𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑣 ) )
12	11	imbi1d	⊢ ( 𝑤 = 𝑣 → ( ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ( 𝑥 ≈ 𝑣 → 𝜑 ) ) )
13	12	albidv	⊢ ( 𝑤 = 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ) )
14		breq2	⊢ ( 𝑤 = suc 𝑣 → ( 𝑥 ≈ 𝑤 ↔ 𝑥 ≈ suc 𝑣 ) )
15	14	imbi1d	⊢ ( 𝑤 = suc 𝑣 → ( ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ) )
16	15	albidv	⊢ ( 𝑤 = suc 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ) )
17		en0	⊢ ( 𝑥 ≈ ∅ ↔ 𝑥 = ∅ )
18	5 1	mpbiri	⊢ ( 𝑥 = ∅ → 𝜑 )
19	17 18	sylbi	⊢ ( 𝑥 ≈ ∅ → 𝜑 )
20	19	ax-gen	⊢ ∀ 𝑥 ( 𝑥 ≈ ∅ → 𝜑 )
21		peano2	⊢ ( 𝑣 ∈ ω → suc 𝑣 ∈ ω )
22		breq2	⊢ ( 𝑤 = suc 𝑣 → ( 𝑦 ≈ 𝑤 ↔ 𝑦 ≈ suc 𝑣 ) )
23	22	rspcev	⊢ ( ( suc 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) → ∃ 𝑤 ∈ ω 𝑦 ≈ 𝑤 )
24	21 23	sylan	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) → ∃ 𝑤 ∈ ω 𝑦 ≈ 𝑤 )
25		isfi	⊢ ( 𝑦 ∈ Fin ↔ ∃ 𝑤 ∈ ω 𝑦 ≈ 𝑤 )
26	24 25	sylibr	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) → 𝑦 ∈ Fin )
27	26	3adant2	⊢ ( ( 𝑣 ∈ ω ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ∧ 𝑦 ≈ suc 𝑣 ) → 𝑦 ∈ Fin )
28		dif1en	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ∧ 𝑧 ∈ 𝑦 ) → ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 )
29	28	3expa	⊢ ( ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) ∧ 𝑧 ∈ 𝑦 ) → ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 )
30		vex	⊢ 𝑦 ∈ V
31	30	difexi	⊢ ( 𝑦 ∖ { 𝑧 } ) ∈ V
32		breq1	⊢ ( 𝑥 = ( 𝑦 ∖ { 𝑧 } ) → ( 𝑥 ≈ 𝑣 ↔ ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 ) )
33	32 2	imbi12d	⊢ ( 𝑥 = ( 𝑦 ∖ { 𝑧 } ) → ( ( 𝑥 ≈ 𝑣 → 𝜑 ) ↔ ( ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 → 𝜒 ) ) )
34	31 33	spcv	⊢ ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ( ( 𝑦 ∖ { 𝑧 } ) ≈ 𝑣 → 𝜒 ) )
35	29 34	syl5com	⊢ ( ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) ∧ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → 𝜒 ) )
36	35	ralrimdva	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑧 ∈ 𝑦 𝜒 ) )
37	36	imp	⊢ ( ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣 ) ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ) → ∀ 𝑧 ∈ 𝑦 𝜒 )
38	37	an32s	⊢ ( ( ( 𝑣 ∈ ω ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ) ∧ 𝑦 ≈ suc 𝑣 ) → ∀ 𝑧 ∈ 𝑦 𝜒 )
39	38	3impa	⊢ ( ( 𝑣 ∈ ω ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ∧ 𝑦 ≈ suc 𝑣 ) → ∀ 𝑧 ∈ 𝑦 𝜒 )
40	27 39 6	sylc	⊢ ( ( 𝑣 ∈ ω ∧ ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) ∧ 𝑦 ≈ suc 𝑣 ) → 𝜃 )
41	40	3exp	⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ( 𝑦 ≈ suc 𝑣 → 𝜃 ) ) )
42	41	alrimdv	⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑦 ( 𝑦 ≈ suc 𝑣 → 𝜃 ) ) )
43		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ suc 𝑣 ↔ 𝑦 ≈ suc 𝑣 ) )
44	43 3	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ↔ ( 𝑦 ≈ suc 𝑣 → 𝜃 ) ) )
45	44	cbvalvw	⊢ ( ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ≈ suc 𝑣 → 𝜃 ) )
46	42 45	syl6ibr	⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ) )
47	10 13 16 20 46	finds1	⊢ ( 𝑤 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) )
48	47	19.21bi	⊢ ( 𝑤 ∈ ω → ( 𝑥 ≈ 𝑤 → 𝜑 ) )
49	48	rexlimiv	⊢ ( ∃ 𝑤 ∈ ω 𝑥 ≈ 𝑤 → 𝜑 )
50	7 49	sylbi	⊢ ( 𝑥 ∈ Fin → 𝜑 )
51	4 50	vtoclga	⊢ ( 𝐴 ∈ Fin → 𝜏 )