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)

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

Proof

Step	Hyp	Ref	Expression
1		findcard2.1	⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
2		findcard2.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		findcard2.3	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝜑 ↔ 𝜃 ) )
4		findcard2.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5		findcard2.5	⊢ 𝜓
6		findcard2.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		nsuceq0	⊢ suc 𝑣 ≠ ∅
22		breq1	⊢ ( 𝑤 = ∅ → ( 𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣 ) )
23	22	anbi2d	⊢ ( 𝑤 = ∅ → ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) ↔ ( 𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣 ) ) )
24		peano1	⊢ ∅ ∈ ω
25		peano2	⊢ ( 𝑣 ∈ ω → suc 𝑣 ∈ ω )
26		nneneq	⊢ ( ( ∅ ∈ ω ∧ suc 𝑣 ∈ ω ) → ( ∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣 ) )
27	24 25 26	sylancr	⊢ ( 𝑣 ∈ ω → ( ∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣 ) )
28	27	biimpa	⊢ ( ( 𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣 ) → ∅ = suc 𝑣 )
29	28	eqcomd	⊢ ( ( 𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣 ) → suc 𝑣 = ∅ )
30	23 29	syl6bi	⊢ ( 𝑤 = ∅ → ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → suc 𝑣 = ∅ ) )
31	30	com12	⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ( 𝑤 = ∅ → suc 𝑣 = ∅ ) )
32	31	necon3d	⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ( suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅ ) )
33	21 32	mpi	⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → 𝑤 ≠ ∅ )
34	33	ex	⊢ ( 𝑣 ∈ ω → ( 𝑤 ≈ suc 𝑣 → 𝑤 ≠ ∅ ) )
35		n0	⊢ ( 𝑤 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝑤 )
36		dif1en	⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ∧ 𝑧 ∈ 𝑤 ) → ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 )
37	36	3expia	⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ( 𝑧 ∈ 𝑤 → ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) )
38		snssi	⊢ ( 𝑧 ∈ 𝑤 → { 𝑧 } ⊆ 𝑤 )
39		uncom	⊢ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = ( { 𝑧 } ∪ ( 𝑤 ∖ { 𝑧 } ) )
40		undif	⊢ ( { 𝑧 } ⊆ 𝑤 ↔ ( { 𝑧 } ∪ ( 𝑤 ∖ { 𝑧 } ) ) = 𝑤 )
41	40	biimpi	⊢ ( { 𝑧 } ⊆ 𝑤 → ( { 𝑧 } ∪ ( 𝑤 ∖ { 𝑧 } ) ) = 𝑤 )
42	39 41	syl5eq	⊢ ( { 𝑧 } ⊆ 𝑤 → ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑤 )
43		vex	⊢ 𝑤 ∈ V
44	43	difexi	⊢ ( 𝑤 ∖ { 𝑧 } ) ∈ V
45		breq1	⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( 𝑦 ≈ 𝑣 ↔ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) )
46	45	anbi2d	⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) ↔ ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) ) )
47		uneq1	⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( 𝑦 ∪ { 𝑧 } ) = ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
48	47	sbceq1d	⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ↔ [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) )
49	48	imbi2d	⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ↔ ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ) )
50	46 49	imbi12d	⊢ ( 𝑦 = ( 𝑤 ∖ { 𝑧 } ) → ( ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ) ) )
51		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 𝑣 ↔ 𝑦 ≈ 𝑣 ) )
52	51 2	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≈ 𝑣 → 𝜑 ) ↔ ( 𝑦 ≈ 𝑣 → 𝜒 ) ) )
53	52	spvv	⊢ ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ( 𝑦 ≈ 𝑣 → 𝜒 ) )
54		rspe	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ∃ 𝑣 ∈ ω 𝑦 ≈ 𝑣 )
55		isfi	⊢ ( 𝑦 ∈ Fin ↔ ∃ 𝑣 ∈ ω 𝑦 ≈ 𝑣 )
56	54 55	sylibr	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → 𝑦 ∈ Fin )
57		pm2.27	⊢ ( 𝑦 ≈ 𝑣 → ( ( 𝑦 ≈ 𝑣 → 𝜒 ) → 𝜒 ) )
58	57	adantl	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ( 𝑦 ≈ 𝑣 → 𝜒 ) → 𝜒 ) )
59	56 58 6	sylsyld	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ( 𝑦 ≈ 𝑣 → 𝜒 ) → 𝜃 ) )
60	53 59	syl5	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → 𝜃 ) )
61		vex	⊢ 𝑦 ∈ V
62		snex	⊢ { 𝑧 } ∈ V
63	61 62	unex	⊢ ( 𝑦 ∪ { 𝑧 } ) ∈ V
64	63 3	sbcie	⊢ ( [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ↔ 𝜃 )
65	60 64	syl6ibr	⊢ ( ( 𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( 𝑦 ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) )
66	44 50 65	vtocl	⊢ ( ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) )
67		dfsbcq	⊢ ( ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑤 → ( [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) )
68	67	imbi2d	⊢ ( ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑤 → ( ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) / 𝑥 ] 𝜑 ) ↔ ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
69	66 68	syl5ib	⊢ ( ( ( 𝑤 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑤 → ( ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
70	38 42 69	3syl	⊢ ( 𝑧 ∈ 𝑤 → ( ( 𝑣 ∈ ω ∧ ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 ) → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
71	70	expd	⊢ ( 𝑧 ∈ 𝑤 → ( 𝑣 ∈ ω → ( ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) ) )
72	71	com12	⊢ ( 𝑣 ∈ ω → ( 𝑧 ∈ 𝑤 → ( ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) ) )
73	72	adantr	⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ( 𝑧 ∈ 𝑤 → ( ( 𝑤 ∖ { 𝑧 } ) ≈ 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) ) )
74	37 73	mpdd	⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ( 𝑧 ∈ 𝑤 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
75	74	exlimdv	⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ( ∃ 𝑧 𝑧 ∈ 𝑤 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
76	35 75	syl5bi	⊢ ( ( 𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ) → ( 𝑤 ≠ ∅ → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
77	76	ex	⊢ ( 𝑣 ∈ ω → ( 𝑤 ≈ suc 𝑣 → ( 𝑤 ≠ ∅ → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) ) )
78	34 77	mpdd	⊢ ( 𝑣 ∈ ω → ( 𝑤 ≈ suc 𝑣 → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
79	78	com23	⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
80	79	alrimdv	⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑤 ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
81		nfv	⊢ Ⅎ 𝑤 ( 𝑥 ≈ suc 𝑣 → 𝜑 )
82		nfv	⊢ Ⅎ 𝑥 𝑤 ≈ suc 𝑣
83		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑
84	82 83	nfim	⊢ Ⅎ 𝑥 ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 )
85		breq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 ≈ suc 𝑣 ↔ 𝑤 ≈ suc 𝑣 ) )
86		sbceq1a	⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) )
87	85 86	imbi12d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ↔ ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 ) ) )
88	81 84 87	cbvalv1	⊢ ( ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ↔ ∀ 𝑤 ( 𝑤 ≈ suc 𝑣 → [ 𝑤 / 𝑥 ] 𝜑 ) )
89	80 88	syl6ibr	⊢ ( 𝑣 ∈ ω → ( ∀ 𝑥 ( 𝑥 ≈ 𝑣 → 𝜑 ) → ∀ 𝑥 ( 𝑥 ≈ suc 𝑣 → 𝜑 ) ) )
90	10 13 16 20 89	finds1	⊢ ( 𝑤 ∈ ω → ∀ 𝑥 ( 𝑥 ≈ 𝑤 → 𝜑 ) )
91	90	19.21bi	⊢ ( 𝑤 ∈ ω → ( 𝑥 ≈ 𝑤 → 𝜑 ) )
92	91	rexlimiv	⊢ ( ∃ 𝑤 ∈ ω 𝑥 ≈ 𝑤 → 𝜑 )
93	7 92	sylbi	⊢ ( 𝑥 ∈ Fin → 𝜑 )
94	4 93	vtoclga	⊢ ( 𝐴 ∈ Fin → 𝜏 )