Theorem ixpfi2 8418

Description: A Cartesian product of finite sets such that all but finitely many are singletons is finite. (Note that 𝐵(𝑥) and 𝐷(𝑥) are both possibly dependent on 𝑥.) (Contributed by Mario Carneiro, 25-Jan-2015.)

Hypotheses

Ref	Expression
ixpfi2.1	⊢ (𝜑 → 𝐶 ∈ Fin)
ixpfi2.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin)
ixpfi2.3	⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝐵 ⊆ {𝐷})

Assertion

Ref	Expression
ixpfi2	⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ∈ Fin)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝐷(𝑥)

Proof of Theorem ixpfi2

Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ixpfi2.1	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Fin)
2		inss2 3982	. . . 4 ⊢ (𝐴 ∩ 𝐶) ⊆ 𝐶
3		ssfi 8334	. . . 4 ⊢ ((𝐶 ∈ Fin ∧ (𝐴 ∩ 𝐶) ⊆ 𝐶) → (𝐴 ∩ 𝐶) ∈ Fin)
4	1, 2, 3	sylancl 574	. . 3 ⊢ (𝜑 → (𝐴 ∩ 𝐶) ∈ Fin)
5		inss1 3981	. . . 4 ⊢ (𝐴 ∩ 𝐶) ⊆ 𝐴
6		ixpfi2.2	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin)
7	6	ralrimiva 3115	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin)
8		ssralv 3815	. . . 4 ⊢ ((𝐴 ∩ 𝐶) ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝐵 ∈ Fin → ∀𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ Fin))
9	5, 7, 8	mpsyl 68	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ Fin)
10		ixpfi 8417	. . 3 ⊢ (((𝐴 ∩ 𝐶) ∈ Fin ∧ ∀𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ Fin) → X𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ Fin)
11	4, 9, 10	syl2anc 573	. 2 ⊢ (𝜑 → X𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ Fin)
12		resixp 8095	. . . . 5 ⊢ (((𝐴 ∩ 𝐶) ⊆ 𝐴 ∧ 𝑓 ∈ X𝑥 ∈ 𝐴 𝐵) → (𝑓 ↾ (𝐴 ∩ 𝐶)) ∈ X𝑥 ∈ (𝐴 ∩ 𝐶)𝐵)
13	5, 12	mpan 670	. . . 4 ⊢ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 → (𝑓 ↾ (𝐴 ∩ 𝐶)) ∈ X𝑥 ∈ (𝐴 ∩ 𝐶)𝐵)
14	13	a1i 11	. . 3 ⊢ (𝜑 → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 → (𝑓 ↾ (𝐴 ∩ 𝐶)) ∈ X𝑥 ∈ (𝐴 ∩ 𝐶)𝐵))
15		simprl 754	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → 𝑓 ∈ X𝑥 ∈ 𝐴 𝐵)
16		vex 3354	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
17	16	elixp 8067	. . . . . . . . . 10 ⊢ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵))
18	15, 17	sylib 208	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵))
19	18	simprd 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)
20		simprr 756	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)
21		vex 3354	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
22	21	elixp 8067	. . . . . . . . . 10 ⊢ (𝑔 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵))
23	20, 22	sylib 208	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵))
24	23	simprd 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵)
25		r19.26 3212	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) ↔ (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵))
26		difss 3888	. . . . . . . . . . 11 ⊢ (𝐴 ∖ 𝐶) ⊆ 𝐴
27		ssralv 3815	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ 𝐶) ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝐴 ∖ 𝐶)((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵)))
28	26, 27	ax-mp 5	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝐴 ∖ 𝐶)((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵))
29		ixpfi2.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝐵 ⊆ {𝐷})
30	29	sseld 3751	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → ((𝑓‘𝑥) ∈ 𝐵 → (𝑓‘𝑥) ∈ {𝐷}))
31		elsni 4333	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑥) ∈ {𝐷} → (𝑓‘𝑥) = 𝐷)
32	30, 31	syl6 35	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → ((𝑓‘𝑥) ∈ 𝐵 → (𝑓‘𝑥) = 𝐷))
33	29	sseld 3751	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → ((𝑔‘𝑥) ∈ 𝐵 → (𝑔‘𝑥) ∈ {𝐷}))
34		elsni 4333	. . . . . . . . . . . . . . 15 ⊢ ((𝑔‘𝑥) ∈ {𝐷} → (𝑔‘𝑥) = 𝐷)
35	33, 34	syl6 35	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → ((𝑔‘𝑥) ∈ 𝐵 → (𝑔‘𝑥) = 𝐷))
36	32, 35	anim12d 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → (((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ((𝑓‘𝑥) = 𝐷 ∧ (𝑔‘𝑥) = 𝐷)))
37		eqtr3 2792	. . . . . . . . . . . . 13 ⊢ (((𝑓‘𝑥) = 𝐷 ∧ (𝑔‘𝑥) = 𝐷) → (𝑓‘𝑥) = (𝑔‘𝑥))
38	36, 37	syl6 35	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → (((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → (𝑓‘𝑥) = (𝑔‘𝑥)))
39	38	ralimdva 3111	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑥 ∈ (𝐴 ∖ 𝐶)((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝐴 ∖ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥)))
40	39	adantr 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → (∀𝑥 ∈ (𝐴 ∖ 𝐶)((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝐴 ∖ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥)))
41	28, 40	syl5 34	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → (∀𝑥 ∈ 𝐴 ((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝐴 ∖ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥)))
42	25, 41	syl5bir 233	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → ((∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵) → ∀𝑥 ∈ (𝐴 ∖ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥)))
43	19, 24, 42	mp2and 679	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → ∀𝑥 ∈ (𝐴 ∖ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥))
44	43	biantrud 521	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → (∀𝑥 ∈ (𝐴 ∩ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥) ↔ (∀𝑥 ∈ (𝐴 ∩ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥) ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥))))
45		fvres 6346	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝑓 ↾ (𝐴 ∩ 𝐶))‘𝑥) = (𝑓‘𝑥))
46		fvres 6346	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝑔 ↾ (𝐴 ∩ 𝐶))‘𝑥) = (𝑔‘𝑥))
47	45, 46	eqeq12d 2786	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → (((𝑓 ↾ (𝐴 ∩ 𝐶))‘𝑥) = ((𝑔 ↾ (𝐴 ∩ 𝐶))‘𝑥) ↔ (𝑓‘𝑥) = (𝑔‘𝑥)))
48	47	ralbiia 3128	. . . . . 6 ⊢ (∀𝑥 ∈ (𝐴 ∩ 𝐶)((𝑓 ↾ (𝐴 ∩ 𝐶))‘𝑥) = ((𝑔 ↾ (𝐴 ∩ 𝐶))‘𝑥) ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥))
49		inundif 4188	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐴 ∖ 𝐶)) = 𝐴
50	49	raleqi 3291	. . . . . . 7 ⊢ (∀𝑥 ∈ ((𝐴 ∩ 𝐶) ∪ (𝐴 ∖ 𝐶))(𝑓‘𝑥) = (𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = (𝑔‘𝑥))
51		ralunb 3945	. . . . . . 7 ⊢ (∀𝑥 ∈ ((𝐴 ∩ 𝐶) ∪ (𝐴 ∖ 𝐶))(𝑓‘𝑥) = (𝑔‘𝑥) ↔ (∀𝑥 ∈ (𝐴 ∩ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥) ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥)))
52	50, 51	bitr3i 266	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = (𝑔‘𝑥) ↔ (∀𝑥 ∈ (𝐴 ∩ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥) ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐶)(𝑓‘𝑥) = (𝑔‘𝑥)))
53	44, 48, 52	3bitr4g 303	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → (∀𝑥 ∈ (𝐴 ∩ 𝐶)((𝑓 ↾ (𝐴 ∩ 𝐶))‘𝑥) = ((𝑔 ↾ (𝐴 ∩ 𝐶))‘𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = (𝑔‘𝑥)))
54	18	simpld 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → 𝑓 Fn 𝐴)
55		fnssres 6142	. . . . . . 7 ⊢ ((𝑓 Fn 𝐴 ∧ (𝐴 ∩ 𝐶) ⊆ 𝐴) → (𝑓 ↾ (𝐴 ∩ 𝐶)) Fn (𝐴 ∩ 𝐶))
56	54, 5, 55	sylancl 574	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → (𝑓 ↾ (𝐴 ∩ 𝐶)) Fn (𝐴 ∩ 𝐶))
57	23	simpld 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → 𝑔 Fn 𝐴)
58		fnssres 6142	. . . . . . 7 ⊢ ((𝑔 Fn 𝐴 ∧ (𝐴 ∩ 𝐶) ⊆ 𝐴) → (𝑔 ↾ (𝐴 ∩ 𝐶)) Fn (𝐴 ∩ 𝐶))
59	57, 5, 58	sylancl 574	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → (𝑔 ↾ (𝐴 ∩ 𝐶)) Fn (𝐴 ∩ 𝐶))
60		eqfnfv 6452	. . . . . 6 ⊢ (((𝑓 ↾ (𝐴 ∩ 𝐶)) Fn (𝐴 ∩ 𝐶) ∧ (𝑔 ↾ (𝐴 ∩ 𝐶)) Fn (𝐴 ∩ 𝐶)) → ((𝑓 ↾ (𝐴 ∩ 𝐶)) = (𝑔 ↾ (𝐴 ∩ 𝐶)) ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)((𝑓 ↾ (𝐴 ∩ 𝐶))‘𝑥) = ((𝑔 ↾ (𝐴 ∩ 𝐶))‘𝑥)))
61	56, 59, 60	syl2anc 573	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → ((𝑓 ↾ (𝐴 ∩ 𝐶)) = (𝑔 ↾ (𝐴 ∩ 𝐶)) ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)((𝑓 ↾ (𝐴 ∩ 𝐶))‘𝑥) = ((𝑔 ↾ (𝐴 ∩ 𝐶))‘𝑥)))
62		eqfnfv 6452	. . . . . 6 ⊢ ((𝑓 Fn 𝐴 ∧ 𝑔 Fn 𝐴) → (𝑓 = 𝑔 ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = (𝑔‘𝑥)))
63	54, 57, 62	syl2anc 573	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → (𝑓 = 𝑔 ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = (𝑔‘𝑥)))
64	53, 61, 63	3bitr4d 300	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵)) → ((𝑓 ↾ (𝐴 ∩ 𝐶)) = (𝑔 ↾ (𝐴 ∩ 𝐶)) ↔ 𝑓 = 𝑔))
65	64	ex 397	. . 3 ⊢ (𝜑 → ((𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵) → ((𝑓 ↾ (𝐴 ∩ 𝐶)) = (𝑔 ↾ (𝐴 ∩ 𝐶)) ↔ 𝑓 = 𝑔)))
66	14, 65	dom2lem 8147	. 2 ⊢ (𝜑 → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ↦ (𝑓 ↾ (𝐴 ∩ 𝐶))):X𝑥 ∈ 𝐴 𝐵–1-1→X𝑥 ∈ (𝐴 ∩ 𝐶)𝐵)
67		f1fi 8407	. 2 ⊢ ((X𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ Fin ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 ↦ (𝑓 ↾ (𝐴 ∩ 𝐶))):X𝑥 ∈ 𝐴 𝐵–1-1→X𝑥 ∈ (𝐴 ∩ 𝐶)𝐵) → X𝑥 ∈ 𝐴 𝐵 ∈ Fin)
68	11, 66, 67	syl2anc 573	1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ∀wral 3061   ∖ cdif 3720   ∪ cun 3721   ∩ cin 3722   ⊆ wss 3723  {csn 4316   ↦ cmpt 4863   ↾ cres 5251   Fn wfn 6024  –1-1→wf1 6026  ‘cfv 6029  Xcixp 8060  Fincfn 8107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-2o 7712  df-oadd 7715  df-er 7894  df-map 8009  df-pm 8010  df-ixp 8061  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111

This theorem is referenced by:  psrbaglefi  19580  eulerpartlemb  30763