Theorem ssfi 9226

Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5334, see ssfiALT 9227. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5334. (Revised by BTernaryTau, 12-Aug-2024.)

Assertion

Ref	Expression
ssfi	⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)

Proof of Theorem ssfi

Dummy variables 𝑏 𝑥 𝑦 𝑧 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssexg 5288	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ Fin) → 𝐵 ∈ V)
2	1	ancoms 464	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V)
3		sseq1 3938	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
4		eleq1 2852	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
5	3, 4	imbi12d 347	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin) ↔ (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
6	5	imbi2d 343	. . . 4 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))))
7		sseq2 3939	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ ∅))
8	7	imbi1d 344	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
9	8	albidv 1955	. . . . . 6 ⊢ (𝑥 = ∅ → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10		sseq2 3939	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝑦))
11	10	imbi1d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
12	11	albidv 1955	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
13		sseq2 3939	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
14	13	imbi1d 344	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
15	14	albidv 1955	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16		sseq2 3939	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝐴))
17	16	imbi1d 344	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
18	17	albidv 1955	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
19		ss0 4355	. . . . . . . 8 ⊢ (𝑏 ⊆ ∅ → 𝑏 = ∅)
20		0fi 9108	. . . . . . . 8 ⊢ ∅ ∈ Fin
21	19, 20	eqeltrdi 2872	. . . . . . 7 ⊢ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
22	21	ax-gen 1828	. . . . . 6 ⊢ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23		sseq1 3938	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑦 ↔ 𝑐 ⊆ 𝑦))
24		eleq1w 2847	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
25	23, 24	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ (𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin)))
26	25	cbvalvw 2071	. . . . . . . . 9 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
27		simp1 1154	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
28		snssi 4748	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑏 → {𝑧} ⊆ 𝑏)
29		undif 4441	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
30	28, 29	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31		uncom 4160	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
32	30, 31	eqtr3di 2813	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑏 → 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33		uncom 4160	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
34	33	sseq2i 3942	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35		ssundif 4446	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
36	34, 35	sylbb 222	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
37	32, 36	anim12ci 626	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38	37	3adant1 1148	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39		3anass 1111	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
40	27, 38, 39	sylanbrc 595	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41		vex 3458	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ∈ V
42	41	difexi 5299	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∖ {𝑧}) ∈ V
43		sseq1 3938	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ⊆ 𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44		eleq1 2852	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
45	43, 44	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
46	42, 45	spcv 3563	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
47	46	imp 412	. . . . . . . . . . . . . 14 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48		snfi 9109	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
49		unfi 9224	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
50	47, 48, 49	sylancl 598	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51		eleq1 2852	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
52	51	biimparc 485	. . . . . . . . . . . . 13 ⊢ ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
53	50, 52	stoic3 1809	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
54	40, 53	syl 18	. . . . . . . . . . 11 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55	54	3expib 1140	. . . . . . . . . 10 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
56	55	alrimiv 1962	. . . . . . . . 9 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
57	26, 56	sylbi 220	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58		disjsn 4673	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑏)
59		disjssun 4424	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦))
60	58, 59	sylbir 238	. . . . . . . . . . . 12 ⊢ (¬ 𝑧 ∈ 𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦))
61	60	biimpa 482	. . . . . . . . . . 11 ⊢ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏 ⊆ 𝑦)
62	34, 61	sylan2b 606	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ⊆ 𝑦)
63	62	imim1i 64	. . . . . . . . 9 ⊢ ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
64	63	alimi 1844	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65		exmid 908	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏)
66	65	jctl 533	. . . . . . . . . . 11 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67		andir 1026	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
68	66, 67	sylib 221	. . . . . . . . . 10 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69		pm3.44 974	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
70	68, 69	syl5 35	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
71	70	alanimi 1849	. . . . . . . 8 ⊢ ((∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
72	57, 64, 71	syl2anc 596	. . . . . . 7 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
73	72	a1i 11	. . . . . 6 ⊢ (𝑦 ∈ Fin → (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
74	9, 12, 15, 18, 22, 73	findcard2 9218	. . . . 5 ⊢ (𝐴 ∈ Fin → ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
75	74	19.21bi 2229	. . . 4 ⊢ (𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
76	6, 75	vtoclg 3521	. . 3 ⊢ (𝐵 ∈ V → (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
77	76	impd 416	. 2 ⊢ (𝐵 ∈ V → ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin))
78	2, 77	mpcom 39	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103  ∀wal 1568   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  {csn 4588  Fincfn 9011

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-om 7912  df-1o 8514  df-en 9012  df-fin 9015

This theorem is used by:  diffi  9228  pwssfi  9230  fnfi  9231  f1domfi  9234  domfi  9242  ssfid  9298  infi  9299  finresfin  9301  findcard3  9312  unfir  9338  f1fi  9344  imafi  9345  pwfilem  9347  xpfi  9349  fofinf1o  9359  cnvfiALT  9366  mapfi  9375  ixpfi2  9377  mptfi  9378  cnvimamptfin  9380  imafi2  9388  unifi3  9389  suppssfifsupp  9409  snopfsupp  9420  fsuppres  9422  sniffsupp  9429  elfiun  9459  oemapvali  9722  hffi  9946  hfsshf  9952  ackbij2lem1  10335  ackbij1lem11  10346  fin23lem26  10442  fin23lem23  10443  fin23lem21  10456  fin11a  10500  isfin1-3  10503  axcclem  10574  ssnn0fi  14168  hashun3  14569  hashss  14594  hashssdif  14598  hashsslei  14612  hashreshashfun  14625  hashbclem  14638  hashf1lem2  14642  seqcoll2  14651  pr2pwpr  14665  fsumless  16007  cvgcmpce  16029  qshash  16038  indsumhash  16040  incexclem  16049  incexc  16050  incexc2  16051  fprodmodd  16208  sumeven  16601  sumodd  16602  bitsfi  16651  bitsinv1  16656  bitsinvp1  16663  sadcaddlem  16671  sadadd2lem  16673  sadadd3  16675  sadaddlem  16680  sadasslem  16684  sadeq  16686  phicl2  16989  phibnd  16992  hashdvds  16996  phiprmpw  16997  phimullem  17000  eulerthlem2  17003  eulerth  17004  phisum  17012  sumhash  17118  prmreclem3  17140  prmreclem4  17141  prmreclem5  17142  1arith  17149  hashbccl  17225  prmgaplem3  17275  chnflenfi  18852  mndpsuppfi  19010  lagsubg  19460  symgfisg  19733  symggen2  19736  odcl2  19830  sylow1lem2  19864  sylow1lem3  19865  sylow1lem4  19866  sylow1lem5  19867  pgpssslw  19879  sylow2alem2  19883  sylow2a  19884  sylow2blem3  19887  sylow3lem3  19894  sylow3lem6  19897  gsumval3lem1  20170  gsumval3lem2  20171  gsumval3  20172  gsumpt  20227  ablfacrplem  20332  ablfacrp2  20334  ablfac1c  20338  ablfac1eulem  20339  ablfac1eu  20340  gsumle  20410  dsmmfi  22099  mplsubg  22364  mpllss  22365  psrbagsn  22427  psr1baslem  22558  submabas  22948  mdetdiaglem  22968  maducoeval2  23010  matunitlindflem1  23049  fctop  23377  restfpw  23552  fincmp  23766  cmpfi  23781  bwth  23783  finlocfin  23894  lfinpfin  23898  locfincmp  23900  1stckgenlem  23927  ptbasfi  23955  ptcnplem  23995  ptcmpfi  24187  cfinfil  24267  ufinffr  24303  fin1aufil  24306  tsmsres  24518  ovoliunlem1  25878  ovolicc2lem4  25896  ovolicc2lem5  25897  i1fima  26054  i1fd  26057  itg1cl  26061  itg1ge0  26062  i1f0  26063  i1f1  26066  i1fmul  26072  itg1addlem4  26075  itg1mulc  26080  itg10a  26086  itg1ge0a  26087  itg1climres  26090  rnplynfin  26685  plyexmo  26691  aannenlem2  26713  aalioulem2  26717  birthday  27339  wilthlem2  27453  ppifi  27490  prmdvdsfi  27491  ppiprm  27535  chtprm  27537  chtdif  27542  efchtdvds  27543  ppidif  27547  ppiltx  27561  mumul  27565  sqff1o  27566  musum  27575  ppiub  27588  vmasum  27600  logfac2  27601  dchrabs  27644  dchrptlem1  27648  dchrptlem2  27649  dchrpt  27651  lgsquadlem1  27764  lgsquadlem2  27765  lgsquadlem3  27766  chebbnd1lem1  27853  chtppilimlem1  27857  rpvmasum2  27896  dchrisum0re  27897  rplogsum  27911  dirith2  27912  oldfib  28820  bdayfinbndlem1  28910  cusgrfi  30096  hashwwlksnext  30560  relfi  33294  ffsrn  33416  xrge0tsmsd  33733  rmfsupp2  33897  hasheuni  34828  carsgclctunlem1  35060  sibfof  35083  sitgclg  35085  oddpwdc  35097  eulerpartlems  35103  eulerpartlemb  35111  eulerpartlemmf  35118  eulerpartlemgf  35122  eulerpartlemgs2  35123  coinfliplem  35222  coinflippv  35227  ballotlemfelz  35234  ballotlemfp1  35235  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemiex  35245  ballotlemsup  35248  ballotlemfg  35269  ballotlemfrc  35270  ballotlemfrceq  35272  ballotth  35281  breprexpnat  35374  hgt750lemb  35396  hgt750leme  35398  fineqvinfep  35934  fisshasheq  36101  deranglem  36139  subfacp1lem3  36155  subfacp1lem5  36157  subfacp1lem6  36158  erdszelem2  36165  erdszelem8  36171  erdsze2lem2  36177  snmlff  36302  mvrsfpw  36479  finminlem  37321  topdifinffinlem  38538  poimirlem9  38815  poimirlem26  38832  poimirlem27  38833  poimirlem28  38834  poimirlem30  38836  poimirlem32  38838  itg2addnclem2  38858  nnubfi  38950  nninfnub  38951  sstotbnd2  38974  cntotbnd  38996  sticksstones1  43462  frlmnzcoordinf  43920  rencldnfilem  44093  jm2.22  44268  jm2.23  44269  filnm  44358  dmstructfi  46189  disjinfi  46480  fsumiunss  46860  fprodexp  46879  fprodabs2  46880  mccllem  46882  sumnnodd  46915  fprodcncf  47183  dvnprodlem2  47230  fourierdlem25  47415  fourierdlem37  47427  fourierdlem51  47440  fourierdlem79  47468  fouriersw  47514  etransclem16  47533  etransclem24  47541  etransclem33  47550  etransclem44  47561  sge0resplit  47689  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  carageniuncllem2  47805  hsphoidmvle2  47868  hsphoidmvle  47869  hoidmvlelem4  47881  hoidmvlelem5  47882  sinnpoly  48214  fmtnoinf  48894  perfectALTVlem2  49093  rmsuppfi  49815  scmsuppfi  49817  suppmptcfin  49819