Theorem ssfi 9198

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 9199. (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 5324	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ Fin) → 𝐵 ∈ V)
2	1	ancoms 457	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V)
3		sseq1 4002	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
4		eleq1 2813	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
5	3, 4	imbi12d 343	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin) ↔ (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
6	5	imbi2d 339	. . . 4 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))))
7		sseq2 4003	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ ∅))
8	7	imbi1d 340	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
9	8	albidv 1915	. . . . . 6 ⊢ (𝑥 = ∅ → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10		sseq2 4003	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝑦))
11	10	imbi1d 340	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
12	11	albidv 1915	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
13		sseq2 4003	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
14	13	imbi1d 340	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
15	14	albidv 1915	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16		sseq2 4003	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝐴))
17	16	imbi1d 340	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
18	17	albidv 1915	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
19		ss0 4400	. . . . . . . 8 ⊢ (𝑏 ⊆ ∅ → 𝑏 = ∅)
20		0fin 9196	. . . . . . . 8 ⊢ ∅ ∈ Fin
21	19, 20	eqeltrdi 2833	. . . . . . 7 ⊢ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
22	21	ax-gen 1789	. . . . . 6 ⊢ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23		sseq1 4002	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑦 ↔ 𝑐 ⊆ 𝑦))
24		eleq1w 2808	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
25	23, 24	imbi12d 343	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ (𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin)))
26	25	cbvalvw 2031	. . . . . . . . 9 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
27		simp1 1133	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
28		snssi 4813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑏 → {𝑧} ⊆ 𝑏)
29		undif 4483	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
30	28, 29	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31		uncom 4150	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
32	30, 31	eqtr3di 2780	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑏 → 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33		uncom 4150	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
34	33	sseq2i 4006	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35		ssundif 4489	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
36	34, 35	sylbb 218	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
37	32, 36	anim12ci 612	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38	37	3adant1 1127	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39		3anass 1092	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
40	27, 38, 39	sylanbrc 581	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41		vex 3465	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ∈ V
42	41	difexi 5331	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∖ {𝑧}) ∈ V
43		sseq1 4002	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ⊆ 𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44		eleq1 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
45	43, 44	imbi12d 343	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
46	42, 45	spcv 3589	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
47	46	imp 405	. . . . . . . . . . . . . 14 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48		snfi 9069	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
49		unfi 9197	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
50	47, 48, 49	sylancl 584	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51		eleq1 2813	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
52	51	biimparc 478	. . . . . . . . . . . . 13 ⊢ ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
53	50, 52	stoic3 1770	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
54	40, 53	syl 17	. . . . . . . . . . 11 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55	54	3expib 1119	. . . . . . . . . 10 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
56	55	alrimiv 1922	. . . . . . . . 9 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
57	26, 56	sylbi 216	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58		disjsn 4717	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑏)
59		disjssun 4469	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦))
60	58, 59	sylbir 234	. . . . . . . . . . . 12 ⊢ (¬ 𝑧 ∈ 𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦))
61	60	biimpa 475	. . . . . . . . . . 11 ⊢ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏 ⊆ 𝑦)
62	34, 61	sylan2b 592	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ⊆ 𝑦)
63	62	imim1i 63	. . . . . . . . 9 ⊢ ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
64	63	alimi 1805	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65		exmid 892	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏)
66	65	jctl 522	. . . . . . . . . . 11 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67		andir 1006	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
68	66, 67	sylib 217	. . . . . . . . . 10 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69		pm3.44 957	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
70	68, 69	syl5 34	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
71	70	alanimi 1810	. . . . . . . 8 ⊢ ((∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
72	57, 64, 71	syl2anc 582	. . . . . . 7 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
73	72	a1i 11	. . . . . 6 ⊢ (𝑦 ∈ Fin → (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
74	9, 12, 15, 18, 22, 73	findcard2 9189	. . . . 5 ⊢ (𝐴 ∈ Fin → ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
75	74	19.21bi 2177	. . . 4 ⊢ (𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
76	6, 75	vtoclg 3532	. . 3 ⊢ (𝐵 ∈ V → (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
77	76	impd 409	. 2 ⊢ (𝐵 ∈ V → ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin))
78	2, 77	mpcom 38	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084  ∀wal 1531   = wceq 1533   ∈ wcel 2098  Vcvv 3461   ∖ cdif 3941   ∪ cun 3942   ∩ cin 3943   ⊆ wss 3944  ∅c0 4322  {csn 4630  Fincfn 8964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-om 7872  df-1o 8487  df-en 8965  df-fin 8968

This theorem is referenced by:  pwfilem  9202  diffi  9204  fnfi  9206  f1domfi  9209  domfi  9217  ssfid  9292  infi  9293  finresfin  9295  findcard3  9310  findcard3OLD  9311  unfir  9339  xpfi  9343  fofinf1o  9353  cnvfiALT  9360  f1fi  9365  imafiALT  9371  mapfi  9374  ixpfi2  9376  mptfi  9377  cnvimamptfin  9379  suppssfifsupp  9405  snopfsupp  9416  fsuppres  9418  sniffsupp  9425  elfiun  9455  oemapvali  9709  ackbij2lem1  10244  ackbij1lem11  10255  fin23lem26  10350  fin23lem23  10351  fin23lem21  10364  fin11a  10408  isfin1-3  10411  axcclem  10482  ssnn0fi  13986  hashun3  14379  hashss  14404  hashssdif  14407  hashsslei  14421  hashreshashfun  14434  hashbclem  14447  hashf1lem2  14453  seqcoll2  14462  pr2pwpr  14476  fsumless  15778  cvgcmpce  15800  qshash  15809  incexclem  15818  incexc  15819  incexc2  15820  fprodmodd  15977  sumeven  16367  sumodd  16368  bitsfi  16415  bitsinv1  16420  bitsinvp1  16427  sadcaddlem  16435  sadadd2lem  16437  sadadd3  16439  sadaddlem  16444  sadasslem  16448  sadeq  16450  phicl2  16740  phibnd  16743  hashdvds  16747  phiprmpw  16748  phimullem  16751  eulerthlem2  16754  eulerth  16755  phisum  16762  sumhash  16868  prmreclem2  16889  prmreclem3  16890  prmreclem4  16891  prmreclem5  16892  1arith  16899  hashbccl  16975  prmgaplem3  17025  lagsubg  19158  symgfisg  19435  symggen2  19438  odcl2  19532  sylow1lem2  19566  sylow1lem3  19567  sylow1lem4  19568  sylow1lem5  19569  pgpssslw  19581  sylow2alem2  19585  sylow2a  19586  sylow2blem3  19589  sylow3lem3  19596  sylow3lem6  19599  gsumval3lem1  19872  gsumval3lem2  19873  gsumval3  19874  gsumpt  19929  ablfacrplem  20034  ablfacrp2  20036  ablfac1c  20040  ablfac1eulem  20041  ablfac1eu  20042  dsmmfi  21689  mplsubg  21964  mpllss  21965  psrbagsn  22029  psr1baslem  22127  submabas  22524  mdetdiaglem  22544  maducoeval2  22586  fctop  22951  restfpw  23127  fincmp  23341  cmpfi  23356  bwth  23358  finlocfin  23468  lfinpfin  23472  locfincmp  23474  1stckgenlem  23501  ptbasfi  23529  ptcnplem  23569  ptcmpfi  23761  cfinfil  23841  ufinffr  23877  fin1aufil  23880  tsmsres  24092  ovoliunlem1  25475  ovolicc2lem4  25493  ovolicc2lem5  25494  i1fima  25651  i1fd  25654  itg1cl  25658  itg1ge0  25659  i1f0  25660  i1f1  25663  i1fmul  25669  itg1addlem4  25672  itg1addlem4OLD  25673  itg1mulc  25678  itg10a  25684  itg1ge0a  25685  itg1climres  25688  plyexmo  26293  aannenlem2  26309  aalioulem2  26313  birthday  26931  wilthlem2  27046  ppifi  27083  prmdvdsfi  27084  ppiprm  27128  chtprm  27130  chtdif  27135  efchtdvds  27136  ppidif  27140  ppiltx  27154  mumul  27158  sqff1o  27159  musum  27168  ppiub  27182  vmasum  27194  logfac2  27195  dchrabs  27238  dchrptlem1  27242  dchrptlem2  27243  dchrpt  27245  lgsquadlem1  27358  lgsquadlem2  27359  lgsquadlem3  27360  chebbnd1lem1  27447  chtppilimlem1  27451  rpvmasum2  27490  dchrisum0re  27491  rplogsum  27505  dirith2  27506  cusgrfi  29344  hashwwlksnext  29797  relfi  32471  imafi2  32575  unifi3  32576  ffsrn  32593  xrge0tsmsd  32861  gsumle  32894  rmfsupp2  33038  hasheuni  33832  carsgclctunlem1  34065  sibfof  34088  sitgclg  34090  oddpwdc  34102  eulerpartlems  34108  eulerpartlemb  34116  eulerpartlemmf  34123  eulerpartlemgf  34127  eulerpartlemgs2  34128  coinfliplem  34226  coinflippv  34231  ballotlemfelz  34238  ballotlemfp1  34239  ballotlemfc0  34240  ballotlemfcc  34241  ballotlemiex  34249  ballotlemsup  34252  ballotlemfg  34273  ballotlemfrc  34274  ballotlemfrceq  34276  ballotth  34285  breprexpnat  34394  hgt750lemb  34416  hgt750leme  34418  fisshasheq  34852  deranglem  34904  subfacp1lem3  34920  subfacp1lem5  34922  subfacp1lem6  34923  erdszelem2  34930  erdszelem8  34936  erdsze2lem2  34942  snmlff  35067  mvrsfpw  35244  finminlem  35930  topdifinffinlem  36954  matunitlindflem1  37217  poimirlem9  37230  poimirlem26  37247  poimirlem27  37248  poimirlem28  37249  poimirlem30  37251  poimirlem32  37253  itg2addnclem2  37273  nnubfi  37351  nninfnub  37352  sstotbnd2  37375  cntotbnd  37397  sticksstones1  41746  rencldnfilem  42379  jm2.22  42555  jm2.23  42556  filnm  42653  pwssfi  44548  disjinfi  44701  fsumiunss  45098  fprodexp  45117  fprodabs2  45118  mccllem  45120  sumnnodd  45153  fprodcncf  45423  dvmptfprod  45468  dvnprodlem1  45469  dvnprodlem2  45470  fourierdlem25  45655  fourierdlem37  45667  fourierdlem51  45680  fourierdlem79  45708  fouriersw  45754  etransclem16  45773  etransclem24  45781  etransclem33  45790  etransclem44  45801  sge0resplit  45929  sge0iunmptlemfi  45936  sge0iunmptlemre  45938  carageniuncllem2  46045  hsphoidmvle2  46108  hsphoidmvle  46109  hoidmvlelem4  46121  hoidmvlelem5  46122  upwrdfi  46408  fmtnoinf  47010  perfectALTVlem2  47196  rmsuppfi  47620  mndpsuppfi  47622  scmsuppfi  47624  suppmptcfin  47626