Theorem ssfi 9240

Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5383, see ssfiALT 9241. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5383. (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 5341	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ Fin) → 𝐵 ∈ V)
2	1	ancoms 458	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V)
3		sseq1 4034	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
4		eleq1 2832	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin) ↔ (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
6	5	imbi2d 340	. . . 4 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))))
7		sseq2 4035	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ ∅))
8	7	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
9	8	albidv 1919	. . . . . 6 ⊢ (𝑥 = ∅ → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10		sseq2 4035	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝑦))
11	10	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
12	11	albidv 1919	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin)))
13		sseq2 4035	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
14	13	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
15	14	albidv 1919	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16		sseq2 4035	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝐴))
17	16	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
18	17	albidv 1919	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)))
19		ss0 4425	. . . . . . . 8 ⊢ (𝑏 ⊆ ∅ → 𝑏 = ∅)
20		0fi 9108	. . . . . . . 8 ⊢ ∅ ∈ Fin
21	19, 20	eqeltrdi 2852	. . . . . . 7 ⊢ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
22	21	ax-gen 1793	. . . . . 6 ⊢ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23		sseq1 4034	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑦 ↔ 𝑐 ⊆ 𝑦))
24		eleq1w 2827	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
25	23, 24	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ (𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin)))
26	25	cbvalvw 2035	. . . . . . . . 9 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
27		simp1 1136	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))
28		snssi 4833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑏 → {𝑧} ⊆ 𝑏)
29		undif 4505	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
30	28, 29	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31		uncom 4181	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
32	30, 31	eqtr3di 2795	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑏 → 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33		uncom 4181	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
34	33	sseq2i 4038	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35		ssundif 4511	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
36	34, 35	sylbb 219	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
37	32, 36	anim12ci 613	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38	37	3adant1 1130	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39		3anass 1095	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
40	27, 38, 39	sylanbrc 582	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41		vex 3492	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ∈ V
42	41	difexi 5348	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∖ {𝑧}) ∈ V
43		sseq1 4034	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ⊆ 𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44		eleq1 2832	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
45	43, 44	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
46	42, 45	spcv 3618	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
47	46	imp 406	. . . . . . . . . . . . . 14 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48		snfi 9109	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
49		unfi 9238	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
50	47, 48, 49	sylancl 585	. . . . . . . . . . . . 13 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51		eleq1 2832	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
52	51	biimparc 479	. . . . . . . . . . . . 13 ⊢ ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
53	50, 52	stoic3 1774	. . . . . . . . . . . 12 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
54	40, 53	syl 17	. . . . . . . . . . 11 ⊢ ((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55	54	3expib 1122	. . . . . . . . . 10 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
56	55	alrimiv 1926	. . . . . . . . 9 ⊢ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
57	26, 56	sylbi 217	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58		disjsn 4736	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑏)
59		disjssun 4491	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦))
60	58, 59	sylbir 235	. . . . . . . . . . . 12 ⊢ (¬ 𝑧 ∈ 𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦))
61	60	biimpa 476	. . . . . . . . . . 11 ⊢ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏 ⊆ 𝑦)
62	34, 61	sylan2b 593	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ⊆ 𝑦)
63	62	imim1i 63	. . . . . . . . 9 ⊢ ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
64	63	alimi 1809	. . . . . . . 8 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65		exmid 893	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏)
66	65	jctl 523	. . . . . . . . . . 11 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67		andir 1009	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
68	66, 67	sylib 218	. . . . . . . . . 10 ⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69		pm3.44 960	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
70	68, 69	syl5 34	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
71	70	alanimi 1814	. . . . . . . 8 ⊢ ((∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
72	57, 64, 71	syl2anc 583	. . . . . . 7 ⊢ (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
73	72	a1i 11	. . . . . 6 ⊢ (𝑦 ∈ Fin → (∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
74	9, 12, 15, 18, 22, 73	findcard2 9230	. . . . 5 ⊢ (𝐴 ∈ Fin → ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
75	74	19.21bi 2190	. . . 4 ⊢ (𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))
76	6, 75	vtoclg 3566	. . 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 846   ∧ w3a 1087  ∀wal 1535   = wceq 1537   ∈ wcel 2108  Vcvv 3488   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  {csn 4648  Fincfn 9003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-om 7904  df-1o 8522  df-en 9004  df-fin 9007

This theorem is referenced by:  diffi  9242  fnfi  9244  f1domfi  9247  domfi  9255  ssfid  9329  infi  9330  finresfin  9332  findcard3  9346  findcard3OLD  9347  unfir  9374  f1fi  9380  imafi  9381  pwfilem  9384  xpfi  9386  fofinf1o  9400  cnvfiALT  9407  mapfi  9418  ixpfi2  9420  mptfi  9421  cnvimamptfin  9423  suppssfifsupp  9449  snopfsupp  9460  fsuppres  9462  sniffsupp  9469  elfiun  9499  oemapvali  9753  ackbij2lem1  10287  ackbij1lem11  10298  fin23lem26  10394  fin23lem23  10395  fin23lem21  10408  fin11a  10452  isfin1-3  10455  axcclem  10526  ssnn0fi  14036  hashun3  14433  hashss  14458  hashssdif  14461  hashsslei  14475  hashreshashfun  14488  hashbclem  14501  hashf1lem2  14505  seqcoll2  14514  pr2pwpr  14528  fsumless  15844  cvgcmpce  15866  qshash  15875  incexclem  15884  incexc  15885  incexc2  15886  fprodmodd  16045  sumeven  16435  sumodd  16436  bitsfi  16483  bitsinv1  16488  bitsinvp1  16495  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  sadasslem  16516  sadeq  16518  phicl2  16815  phibnd  16818  hashdvds  16822  phiprmpw  16823  phimullem  16826  eulerthlem2  16829  eulerth  16830  phisum  16837  sumhash  16943  prmreclem2  16964  prmreclem3  16965  prmreclem4  16966  prmreclem5  16967  1arith  16974  hashbccl  17050  prmgaplem3  17100  lagsubg  19235  symgfisg  19510  symggen2  19513  odcl2  19607  sylow1lem2  19641  sylow1lem3  19642  sylow1lem4  19643  sylow1lem5  19644  pgpssslw  19656  sylow2alem2  19660  sylow2a  19661  sylow2blem3  19664  sylow3lem3  19671  sylow3lem6  19674  gsumval3lem1  19947  gsumval3lem2  19948  gsumval3  19949  gsumpt  20004  ablfacrplem  20109  ablfacrp2  20111  ablfac1c  20115  ablfac1eulem  20116  ablfac1eu  20117  dsmmfi  21781  mplsubg  22045  mpllss  22046  psrbagsn  22110  psr1baslem  22207  submabas  22605  mdetdiaglem  22625  maducoeval2  22667  fctop  23032  restfpw  23208  fincmp  23422  cmpfi  23437  bwth  23439  finlocfin  23549  lfinpfin  23553  locfincmp  23555  1stckgenlem  23582  ptbasfi  23610  ptcnplem  23650  ptcmpfi  23842  cfinfil  23922  ufinffr  23958  fin1aufil  23961  tsmsres  24173  ovoliunlem1  25556  ovolicc2lem4  25574  ovolicc2lem5  25575  i1fima  25732  i1fd  25735  itg1cl  25739  itg1ge0  25740  i1f0  25741  i1f1  25744  i1fmul  25750  itg1addlem4  25753  itg1addlem4OLD  25754  itg1mulc  25759  itg10a  25765  itg1ge0a  25766  itg1climres  25769  plyexmo  26373  aannenlem2  26389  aalioulem2  26393  birthday  27015  wilthlem2  27130  ppifi  27167  prmdvdsfi  27168  ppiprm  27212  chtprm  27214  chtdif  27219  efchtdvds  27220  ppidif  27224  ppiltx  27238  mumul  27242  sqff1o  27243  musum  27252  ppiub  27266  vmasum  27278  logfac2  27279  dchrabs  27322  dchrptlem1  27326  dchrptlem2  27327  dchrpt  27329  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  chebbnd1lem1  27531  chtppilimlem1  27535  rpvmasum2  27574  dchrisum0re  27575  rplogsum  27589  dirith2  27590  cusgrfi  29494  hashwwlksnext  29947  relfi  32624  imafi2  32725  unifi3  32726  ffsrn  32743  xrge0tsmsd  33041  gsumle  33074  rmfsupp2  33218  hasheuni  34049  carsgclctunlem1  34282  sibfof  34305  sitgclg  34307  oddpwdc  34319  eulerpartlems  34325  eulerpartlemb  34333  eulerpartlemmf  34340  eulerpartlemgf  34344  eulerpartlemgs2  34345  coinfliplem  34443  coinflippv  34448  ballotlemfelz  34455  ballotlemfp1  34456  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemiex  34466  ballotlemsup  34469  ballotlemfg  34490  ballotlemfrc  34491  ballotlemfrceq  34493  ballotth  34502  breprexpnat  34611  hgt750lemb  34633  hgt750leme  34635  fisshasheq  35082  deranglem  35134  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  erdszelem2  35160  erdszelem8  35166  erdsze2lem2  35172  snmlff  35297  mvrsfpw  35474  finminlem  36284  topdifinffinlem  37313  matunitlindflem1  37576  poimirlem9  37589  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem30  37610  poimirlem32  37612  itg2addnclem2  37632  nnubfi  37710  nninfnub  37711  sstotbnd2  37734  cntotbnd  37756  sticksstones1  42103  rencldnfilem  42776  jm2.22  42952  jm2.23  42953  filnm  43047  pwssfi  44947  disjinfi  45099  fsumiunss  45496  fprodexp  45515  fprodabs2  45516  mccllem  45518  sumnnodd  45551  fprodcncf  45821  dvmptfprod  45866  dvnprodlem1  45867  dvnprodlem2  45868  fourierdlem25  46053  fourierdlem37  46065  fourierdlem51  46078  fourierdlem79  46106  fouriersw  46152  etransclem16  46171  etransclem24  46179  etransclem33  46188  etransclem44  46199  sge0resplit  46327  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  carageniuncllem2  46443  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmvlelem4  46519  hoidmvlelem5  46520  upwrdfi  46806  fmtnoinf  47410  perfectALTVlem2  47596  rmsuppfi  48098  mndpsuppfi  48100  scmsuppfi  48102  suppmptcfin  48104