Theorem ssfi 9077

Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5298, see ssfiALT 9078. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5298. (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 5256	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ Fin) → 𝐵 ∈ V)
2	1	ancoms 458	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V)
3		sseq1 3955	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
4		eleq1 2819	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin) ↔ (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
6	5	imbi2d 340	. . . 4 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))))
7		sseq2 3956	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ ∅))
8	7	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
9	8	albidv 1921	. . . . . 6 ⊢ (𝑥 = ∅ → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10		sseq2 3956	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝑦))
11	10	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
12	11	albidv 1921	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
13		sseq2 3956	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
14	13	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
15	14	albidv 1921	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16		sseq2 3956	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝐴))
17	16	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
18	17	albidv 1921	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
19		ss0 4347	. . . . . . . 8 ⊢ (𝑏 ⊆ ∅ → 𝑏 = ∅)
20		0fi 8959	. . . . . . . 8 ⊢ ∅ ∈ Fin
21	19, 20	eqeltrdi 2839	. . . . . . 7 ⊢ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
22	21	ax-gen 1796	. . . . . 6 ⊢ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23		sseq1 3955	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑦 ↔ 𝑐 ⊆ 𝑦))
24		eleq1w 2814	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
25	23, 24	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ (𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin)))
26	25	cbvalvw 2037	. . . . . . . . 9 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
27		simp1 1136	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
28		snssi 4755	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑏 → {𝑧} ⊆ 𝑏)
29		undif 4427	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
30	28, 29	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31		uncom 4103	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
32	30, 31	eqtr3di 2781	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑏 → 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33		uncom 4103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
34	33	sseq2i 3959	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35		ssundif 4433	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
36	34, 35	sylbb 219	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
37	32, 36	anim12ci 614	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38	37	3adant1 1130	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39		3anass 1094	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
40	27, 38, 39	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41		vex 3440	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ∈ V
42	41	difexi 5263	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∖ {𝑧}) ∈ V
43		sseq1 3955	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ⊆ 𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44		eleq1 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
45	43, 44	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
46	42, 45	spcv 3555	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
47	46	imp 406	. . . . . . . . . . . . . 14 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48		snfi 8960	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
49		unfi 9075	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
50	47, 48, 49	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51		eleq1 2819	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
52	51	biimparc 479	. . . . . . . . . . . . 13 ⊢ ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
53	50, 52	stoic3 1777	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
54	40, 53	syl 17	. . . . . . . . . . 11 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55	54	3expib 1122	. . . . . . . . . 10 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
56	55	alrimiv 1928	. . . . . . . . 9 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
57	26, 56	sylbi 217	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58		disjsn 4659	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑏)
59		disjssun 4413	. . . . . . . . . . . . 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 1812	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65		exmid 894	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏)
66	65	jctl 523	. . . . . . . . . . 11 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67		andir 1010	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
68	66, 67	sylib 218	. . . . . . . . . 10 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69		pm3.44 961	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
70	68, 69	syl5 34	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
71	70	alanimi 1817	. . . . . . . 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 9069	. . . . 5 ⊢ (𝐴 ∈ Fin → ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
75	74	19.21bi 2192	. . . 4 ⊢ (𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
76	6, 75	vtoclg 3507	. . 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 847   ∧ w3a 1086  ∀wal 1539   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ∖ cdif 3894   ∪ cun 3895   ∩ cin 3896   ⊆ wss 3897  ∅c0 4278  {csn 4571  Fincfn 8864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-om 7792  df-1o 8380  df-en 8865  df-fin 8868

This theorem is referenced by:  diffi  9079  pwssfi  9081  fnfi  9082  f1domfi  9085  domfi  9093  ssfid  9148  infi  9149  finresfin  9151  findcard3  9162  unfir  9187  f1fi  9193  imafi  9194  pwfilem  9197  xpfi  9199  fofinf1o  9211  cnvfiALT  9218  mapfi  9227  ixpfi2  9229  mptfi  9230  cnvimamptfin  9232  suppssfifsupp  9259  snopfsupp  9270  fsuppres  9272  sniffsupp  9279  elfiun  9309  oemapvali  9569  ackbij2lem1  10104  ackbij1lem11  10115  fin23lem26  10211  fin23lem23  10212  fin23lem21  10225  fin11a  10269  isfin1-3  10272  axcclem  10343  ssnn0fi  13887  hashun3  14286  hashss  14311  hashssdif  14314  hashsslei  14328  hashreshashfun  14341  hashbclem  14354  hashf1lem2  14358  seqcoll2  14367  pr2pwpr  14381  fsumless  15698  cvgcmpce  15720  qshash  15729  incexclem  15738  incexc  15739  incexc2  15740  fprodmodd  15899  sumeven  16293  sumodd  16294  bitsfi  16343  bitsinv1  16348  bitsinvp1  16355  sadcaddlem  16363  sadadd2lem  16365  sadadd3  16367  sadaddlem  16372  sadasslem  16376  sadeq  16378  phicl2  16674  phibnd  16677  hashdvds  16681  phiprmpw  16682  phimullem  16685  eulerthlem2  16688  eulerth  16689  phisum  16697  sumhash  16803  prmreclem2  16824  prmreclem3  16825  prmreclem4  16826  prmreclem5  16827  1arith  16834  hashbccl  16910  prmgaplem3  16960  chnflenfi  18529  mndpsuppfi  18669  lagsubg  19102  symgfisg  19375  symggen2  19378  odcl2  19472  sylow1lem2  19506  sylow1lem3  19507  sylow1lem4  19508  sylow1lem5  19509  pgpssslw  19521  sylow2alem2  19525  sylow2a  19526  sylow2blem3  19529  sylow3lem3  19536  sylow3lem6  19539  gsumval3lem1  19812  gsumval3lem2  19813  gsumval3  19814  gsumpt  19869  ablfacrplem  19974  ablfacrp2  19976  ablfac1c  19980  ablfac1eulem  19981  ablfac1eu  19982  gsumle  20052  dsmmfi  21670  mplsubg  21934  mpllss  21935  psrbagsn  21993  psr1baslem  22092  submabas  22488  mdetdiaglem  22508  maducoeval2  22550  fctop  22914  restfpw  23089  fincmp  23303  cmpfi  23318  bwth  23320  finlocfin  23430  lfinpfin  23434  locfincmp  23436  1stckgenlem  23463  ptbasfi  23491  ptcnplem  23531  ptcmpfi  23723  cfinfil  23803  ufinffr  23839  fin1aufil  23842  tsmsres  24054  ovoliunlem1  25425  ovolicc2lem4  25443  ovolicc2lem5  25444  i1fima  25601  i1fd  25604  itg1cl  25608  itg1ge0  25609  i1f0  25610  i1f1  25613  i1fmul  25619  itg1addlem4  25622  itg1mulc  25627  itg10a  25633  itg1ge0a  25634  itg1climres  25637  plyexmo  26243  aannenlem2  26259  aalioulem2  26263  birthday  26886  wilthlem2  27001  ppifi  27038  prmdvdsfi  27039  ppiprm  27083  chtprm  27085  chtdif  27090  efchtdvds  27091  ppidif  27095  ppiltx  27109  mumul  27113  sqff1o  27114  musum  27123  ppiub  27137  vmasum  27149  logfac2  27150  dchrabs  27193  dchrptlem1  27197  dchrptlem2  27198  dchrpt  27200  lgsquadlem1  27313  lgsquadlem2  27314  lgsquadlem3  27315  chebbnd1lem1  27402  chtppilimlem1  27406  rpvmasum2  27445  dchrisum0re  27446  rplogsum  27460  dirith2  27461  cusgrfi  29432  hashwwlksnext  29887  relfi  32574  imafi2  32685  unifi3  32686  ffsrn  32703  xrge0tsmsd  33034  rmfsupp2  33197  hasheuni  34090  carsgclctunlem1  34322  sibfof  34345  sitgclg  34347  oddpwdc  34359  eulerpartlems  34365  eulerpartlemb  34373  eulerpartlemmf  34380  eulerpartlemgf  34384  eulerpartlemgs2  34385  coinfliplem  34484  coinflippv  34489  ballotlemfelz  34496  ballotlemfp1  34497  ballotlemfc0  34498  ballotlemfcc  34499  ballotlemiex  34507  ballotlemsup  34510  ballotlemfg  34531  ballotlemfrc  34532  ballotlemfrceq  34534  ballotth  34543  breprexpnat  34639  hgt750lemb  34661  hgt750leme  34663  r1omfi  35108  fisshasheq  35151  deranglem  35202  subfacp1lem3  35218  subfacp1lem5  35220  subfacp1lem6  35221  erdszelem2  35228  erdszelem8  35234  erdsze2lem2  35240  snmlff  35365  mvrsfpw  35542  finminlem  36352  topdifinffinlem  37381  matunitlindflem1  37656  poimirlem9  37669  poimirlem26  37686  poimirlem27  37687  poimirlem28  37688  poimirlem30  37690  poimirlem32  37692  itg2addnclem2  37712  nnubfi  37790  nninfnub  37791  sstotbnd2  37814  cntotbnd  37836  sticksstones1  42179  rencldnfilem  42853  jm2.22  43028  jm2.23  43029  filnm  43123  disjinfi  45229  fsumiunss  45615  fprodexp  45634  fprodabs2  45635  mccllem  45637  sumnnodd  45670  fprodcncf  45938  dvnprodlem2  45985  fourierdlem25  46170  fourierdlem37  46182  fourierdlem51  46195  fourierdlem79  46223  fouriersw  46269  etransclem16  46288  etransclem24  46296  etransclem33  46305  etransclem44  46316  sge0resplit  46444  sge0iunmptlemfi  46451  sge0iunmptlemre  46453  carageniuncllem2  46560  hsphoidmvle2  46623  hsphoidmvle  46624  hoidmvlelem4  46636  hoidmvlelem5  46637  sinnpoly  46922  fmtnoinf  47567  perfectALTVlem2  47753  rmsuppfi  48403  scmsuppfi  48405  suppmptcfin  48407