Theorem ssfi 9213

Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5365, see ssfiALT 9214. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5365. (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 5323	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ Fin) → 𝐵 ∈ V)
2	1	ancoms 458	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V)
3		sseq1 4009	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
4		eleq1 2829	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin) ↔ (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
6	5	imbi2d 340	. . . 4 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))))
7		sseq2 4010	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ ∅))
8	7	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
9	8	albidv 1920	. . . . . 6 ⊢ (𝑥 = ∅ → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10		sseq2 4010	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝑦))
11	10	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
12	11	albidv 1920	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
13		sseq2 4010	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
14	13	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
15	14	albidv 1920	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16		sseq2 4010	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝐴))
17	16	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
18	17	albidv 1920	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
19		ss0 4402	. . . . . . . 8 ⊢ (𝑏 ⊆ ∅ → 𝑏 = ∅)
20		0fi 9082	. . . . . . . 8 ⊢ ∅ ∈ Fin
21	19, 20	eqeltrdi 2849	. . . . . . 7 ⊢ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
22	21	ax-gen 1795	. . . . . 6 ⊢ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23		sseq1 4009	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑦 ↔ 𝑐 ⊆ 𝑦))
24		eleq1w 2824	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
25	23, 24	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ (𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin)))
26	25	cbvalvw 2035	. . . . . . . . 9 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
27		simp1 1137	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
28		snssi 4808	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑏 → {𝑧} ⊆ 𝑏)
29		undif 4482	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
30	28, 29	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31		uncom 4158	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
32	30, 31	eqtr3di 2792	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑏 → 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33		uncom 4158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
34	33	sseq2i 4013	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35		ssundif 4488	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
36	34, 35	sylbb 219	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
37	32, 36	anim12ci 614	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38	37	3adant1 1131	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39		3anass 1095	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
40	27, 38, 39	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41		vex 3484	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ∈ V
42	41	difexi 5330	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∖ {𝑧}) ∈ V
43		sseq1 4009	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ⊆ 𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44		eleq1 2829	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
45	43, 44	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
46	42, 45	spcv 3605	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
47	46	imp 406	. . . . . . . . . . . . . 14 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48		snfi 9083	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
49		unfi 9211	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
50	47, 48, 49	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51		eleq1 2829	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
52	51	biimparc 479	. . . . . . . . . . . . 13 ⊢ ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
53	50, 52	stoic3 1776	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
54	40, 53	syl 17	. . . . . . . . . . 11 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55	54	3expib 1123	. . . . . . . . . 10 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
56	55	alrimiv 1927	. . . . . . . . 9 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
57	26, 56	sylbi 217	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58		disjsn 4711	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑏)
59		disjssun 4468	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦))
60	58, 59	sylbir 235	. . . . . . . . . . . 12 ⊢ (¬ 𝑧 ∈ 𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦))
61	60	biimpa 476	. . . . . . . . . . 11 ⊢ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏 ⊆ 𝑦)
62	34, 61	sylan2b 594	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ⊆ 𝑦)
63	62	imim1i 63	. . . . . . . . 9 ⊢ ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
64	63	alimi 1811	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65		exmid 895	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏)
66	65	jctl 523	. . . . . . . . . . 11 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67		andir 1011	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
68	66, 67	sylib 218	. . . . . . . . . 10 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69		pm3.44 962	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
70	68, 69	syl5 34	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
71	70	alanimi 1816	. . . . . . . 8 ⊢ ((∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
72	57, 64, 71	syl2anc 584	. . . . . . 7 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
73	72	a1i 11	. . . . . 6 ⊢ (𝑦 ∈ Fin → (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
74	9, 12, 15, 18, 22, 73	findcard2 9204	. . . . 5 ⊢ (𝐴 ∈ Fin → ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
75	74	19.21bi 2189	. . . 4 ⊢ (𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
76	6, 75	vtoclg 3554	. . 3 ⊢ (𝐵 ∈ V → (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
77	76	impd 410	. 2 ⊢ (𝐵 ∈ V → ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin))
78	2, 77	mpcom 38	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087  ∀wal 1538   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  {csn 4626  Fincfn 8985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-1o 8506  df-en 8986  df-fin 8989

This theorem is referenced by:  diffi  9215  pwssfi  9217  fnfi  9218  f1domfi  9221  domfi  9229  ssfid  9301  infi  9302  finresfin  9304  findcard3  9318  findcard3OLD  9319  unfir  9346  f1fi  9352  imafi  9353  pwfilem  9356  xpfi  9358  fofinf1o  9372  cnvfiALT  9379  mapfi  9388  ixpfi2  9390  mptfi  9391  cnvimamptfin  9393  suppssfifsupp  9420  snopfsupp  9431  fsuppres  9433  sniffsupp  9440  elfiun  9470  oemapvali  9724  ackbij2lem1  10258  ackbij1lem11  10269  fin23lem26  10365  fin23lem23  10366  fin23lem21  10379  fin11a  10423  isfin1-3  10426  axcclem  10497  ssnn0fi  14026  hashun3  14423  hashss  14448  hashssdif  14451  hashsslei  14465  hashreshashfun  14478  hashbclem  14491  hashf1lem2  14495  seqcoll2  14504  pr2pwpr  14518  fsumless  15832  cvgcmpce  15854  qshash  15863  incexclem  15872  incexc  15873  incexc2  15874  fprodmodd  16033  sumeven  16424  sumodd  16425  bitsfi  16474  bitsinv1  16479  bitsinvp1  16486  sadcaddlem  16494  sadadd2lem  16496  sadadd3  16498  sadaddlem  16503  sadasslem  16507  sadeq  16509  phicl2  16805  phibnd  16808  hashdvds  16812  phiprmpw  16813  phimullem  16816  eulerthlem2  16819  eulerth  16820  phisum  16828  sumhash  16934  prmreclem2  16955  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  1arith  16965  hashbccl  17041  prmgaplem3  17091  mndpsuppfi  18779  lagsubg  19213  symgfisg  19486  symggen2  19489  odcl2  19583  sylow1lem2  19617  sylow1lem3  19618  sylow1lem4  19619  sylow1lem5  19620  pgpssslw  19632  sylow2alem2  19636  sylow2a  19637  sylow2blem3  19640  sylow3lem3  19647  sylow3lem6  19650  gsumval3lem1  19923  gsumval3lem2  19924  gsumval3  19925  gsumpt  19980  ablfacrplem  20085  ablfacrp2  20087  ablfac1c  20091  ablfac1eulem  20092  ablfac1eu  20093  dsmmfi  21758  mplsubg  22022  mpllss  22023  psrbagsn  22087  psr1baslem  22186  submabas  22584  mdetdiaglem  22604  maducoeval2  22646  fctop  23011  restfpw  23187  fincmp  23401  cmpfi  23416  bwth  23418  finlocfin  23528  lfinpfin  23532  locfincmp  23534  1stckgenlem  23561  ptbasfi  23589  ptcnplem  23629  ptcmpfi  23821  cfinfil  23901  ufinffr  23937  fin1aufil  23940  tsmsres  24152  ovoliunlem1  25537  ovolicc2lem4  25555  ovolicc2lem5  25556  i1fima  25713  i1fd  25716  itg1cl  25720  itg1ge0  25721  i1f0  25722  i1f1  25725  i1fmul  25731  itg1addlem4  25734  itg1mulc  25739  itg10a  25745  itg1ge0a  25746  itg1climres  25749  plyexmo  26355  aannenlem2  26371  aalioulem2  26375  birthday  26997  wilthlem2  27112  ppifi  27149  prmdvdsfi  27150  ppiprm  27194  chtprm  27196  chtdif  27201  efchtdvds  27202  ppidif  27206  ppiltx  27220  mumul  27224  sqff1o  27225  musum  27234  ppiub  27248  vmasum  27260  logfac2  27261  dchrabs  27304  dchrptlem1  27308  dchrptlem2  27309  dchrpt  27311  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  chebbnd1lem1  27513  chtppilimlem1  27517  rpvmasum2  27556  dchrisum0re  27557  rplogsum  27571  dirith2  27572  cusgrfi  29476  hashwwlksnext  29934  relfi  32615  imafi2  32723  unifi3  32724  ffsrn  32740  xrge0tsmsd  33065  gsumle  33101  rmfsupp2  33242  hasheuni  34086  carsgclctunlem1  34319  sibfof  34342  sitgclg  34344  oddpwdc  34356  eulerpartlems  34362  eulerpartlemb  34370  eulerpartlemmf  34377  eulerpartlemgf  34381  eulerpartlemgs2  34382  coinfliplem  34481  coinflippv  34486  ballotlemfelz  34493  ballotlemfp1  34494  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemiex  34504  ballotlemsup  34507  ballotlemfg  34528  ballotlemfrc  34529  ballotlemfrceq  34531  ballotth  34540  breprexpnat  34649  hgt750lemb  34671  hgt750leme  34673  fisshasheq  35120  deranglem  35171  subfacp1lem3  35187  subfacp1lem5  35189  subfacp1lem6  35190  erdszelem2  35197  erdszelem8  35203  erdsze2lem2  35209  snmlff  35334  mvrsfpw  35511  finminlem  36319  topdifinffinlem  37348  matunitlindflem1  37623  poimirlem9  37636  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem30  37657  poimirlem32  37659  itg2addnclem2  37679  nnubfi  37757  nninfnub  37758  sstotbnd2  37781  cntotbnd  37803  sticksstones1  42147  rencldnfilem  42831  jm2.22  43007  jm2.23  43008  filnm  43102  disjinfi  45197  fsumiunss  45590  fprodexp  45609  fprodabs2  45610  mccllem  45612  sumnnodd  45645  fprodcncf  45915  dvnprodlem2  45962  fourierdlem25  46147  fourierdlem37  46159  fourierdlem51  46172  fourierdlem79  46200  fouriersw  46246  etransclem16  46265  etransclem24  46273  etransclem33  46282  etransclem44  46293  sge0resplit  46421  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  carageniuncllem2  46537  hsphoidmvle2  46600  hsphoidmvle  46601  hoidmvlelem4  46613  hoidmvlelem5  46614  upwrdfi  46902  fmtnoinf  47523  perfectALTVlem2  47709  rmsuppfi  48288  scmsuppfi  48290  suppmptcfin  48292