Theorem resscntz 14160

Description: Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.)

Hypotheses

Ref	Expression
resscntz.p	⊢ 𝐻 = (𝐺 ↾s 𝐴)
resscntz.z	⊢ 𝑍 = (Cntz‘𝐺)
resscntz.y	⊢ 𝑌 = (Cntz‘𝐻)

Assertion

Ref	Expression
resscntz	⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴))

Proof of Theorem resscntz

Dummy variables 𝑥 𝑦 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		resscntz.y	. . . . . . 7 ⊢ 𝑌 = (Cntz‘𝐻)
2	1	cntzm 14155	. . . . . 6 ⊢ (𝑥 ∈ (𝑌‘𝑆) → ∃𝑤 𝑤 ∈ 𝐻)
3		resscntz.p	. . . . . . . 8 ⊢ 𝐻 = (𝐺 ↾s 𝐴)
4	3	ressmex 13472	. . . . . . 7 ⊢ (𝑤 ∈ 𝐻 → (𝐺 ∈ V ∧ 𝐴 ∈ V))
5	4	exlimiv 1651	. . . . . 6 ⊢ (∃𝑤 𝑤 ∈ 𝐻 → (𝐺 ∈ V ∧ 𝐴 ∈ V))
6	2, 5	syl 14	. . . . 5 ⊢ (𝑥 ∈ (𝑌‘𝑆) → (𝐺 ∈ V ∧ 𝐴 ∈ V))
7	6	simpld 112	. . . 4 ⊢ (𝑥 ∈ (𝑌‘𝑆) → 𝐺 ∈ V)
8	7	a1i 9	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑥 ∈ (𝑌‘𝑆) → 𝐺 ∈ V))
9		simpr 110	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴)) → 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴))
10	9	elin1d 3418	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴)) → 𝑥 ∈ (𝑍‘𝑆))
11		eqid 2238	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
12		resscntz.z	. . . . . . 7 ⊢ 𝑍 = (Cntz‘𝐺)
13	11, 12	cntzrcl 14153	. . . . . 6 ⊢ (𝑥 ∈ (𝑍‘𝑆) → (𝐺 ∈ V ∧ 𝑆 ⊆ (Base‘𝐺)))
14	10, 13	syl 14	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴)) → (𝐺 ∈ V ∧ 𝑆 ⊆ (Base‘𝐺)))
15	14	simpld 112	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴)) → 𝐺 ∈ V)
16	15	ex 115	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝐺 ∈ V))
17		eqid 2238	. . . . . . . . 9 ⊢ (Base‘𝐻) = (Base‘𝐻)
18	17, 1	cntzrcl 14153	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑌‘𝑆) → (𝐻 ∈ V ∧ 𝑆 ⊆ (Base‘𝐻)))
19	18	simprd 114	. . . . . . 7 ⊢ (𝑥 ∈ (𝑌‘𝑆) → 𝑆 ⊆ (Base‘𝐻))
20	3	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → 𝐻 = (𝐺 ↾s 𝐴))
21		eqidd 2239	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (Base‘𝐺) = (Base‘𝐺))
22		simpr 110	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → 𝐺 ∈ V)
23		simpll 531	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → 𝐴 ∈ 𝑉)
24	20, 21, 22, 23	ressbasssd 13476	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (Base‘𝐻) ⊆ (Base‘𝐺))
25	19, 24	sylan9ssr 3262	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) ∧ 𝑥 ∈ (𝑌‘𝑆)) → 𝑆 ⊆ (Base‘𝐺))
26	25	ex 115	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (𝑥 ∈ (𝑌‘𝑆) → 𝑆 ⊆ (Base‘𝐺)))
27		elinel1 3415	. . . . . . 7 ⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝑥 ∈ (𝑍‘𝑆))
28	13	simprd 114	. . . . . . 7 ⊢ (𝑥 ∈ (𝑍‘𝑆) → 𝑆 ⊆ (Base‘𝐺))
29	27, 28	syl 14	. . . . . 6 ⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝑆 ⊆ (Base‘𝐺))
30	29	a1i 9	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) → 𝑆 ⊆ (Base‘𝐺)))
31		elin 3412	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴 ∩ (Base‘𝐺)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)))
32	20, 21, 22, 23	ressbasd 13474	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (𝐴 ∩ (Base‘𝐺)) = (Base‘𝐻))
33	32	eleq2d 2308	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (𝑥 ∈ (𝐴 ∩ (Base‘𝐺)) ↔ 𝑥 ∈ (Base‘𝐻)))
34	31, 33	bitr3id 194	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ↔ 𝑥 ∈ (Base‘𝐻)))
35		eqidd 2239	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (+g‘𝐺) = (+g‘𝐺))
36	20, 35, 23, 22	ressplusgd 13536	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (+g‘𝐺) = (+g‘𝐻))
37	36	oveqd 6102	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦))
38	36	oveqd 6102	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (𝑦(+g‘𝐺)𝑥) = (𝑦(+g‘𝐻)𝑥))
39	37, 38	eqeq12d 2253	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → ((𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))
40	39	ralbidv 2550	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥) ↔ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)))
41	34, 40	anbi12d 477	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥))))
42		anass 405	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))))
43	41, 42	bitr3di 195	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → ((𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))))
44	43	adantlr 481	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) ∧ 𝐺 ∈ V) → ((𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))))
45		simpllr 540	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) ∧ 𝐺 ∈ V) → 𝑆 ⊆ 𝐴)
46		simplr 533	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) ∧ 𝐺 ∈ V) → 𝑆 ⊆ (Base‘𝐺))
47		ssin 3453	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ (Base‘𝐺)) ↔ 𝑆 ⊆ (𝐴 ∩ (Base‘𝐺)))
48	32	sseq2d 3278	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (𝑆 ⊆ (𝐴 ∩ (Base‘𝐺)) ↔ 𝑆 ⊆ (Base‘𝐻)))
49	48	adantlr 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) ∧ 𝐺 ∈ V) → (𝑆 ⊆ (𝐴 ∩ (Base‘𝐺)) ↔ 𝑆 ⊆ (Base‘𝐻)))
50	47, 49	bitrid 192	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) ∧ 𝐺 ∈ V) → ((𝑆 ⊆ 𝐴 ∧ 𝑆 ⊆ (Base‘𝐺)) ↔ 𝑆 ⊆ (Base‘𝐻)))
51	45, 46, 50	mpbi2and 956	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) ∧ 𝐺 ∈ V) → 𝑆 ⊆ (Base‘𝐻))
52		eqid 2238	. . . . . . . . . 10 ⊢ (+g‘𝐻) = (+g‘𝐻)
53	17, 52, 1	elcntz 14148	. . . . . . . . 9 ⊢ (𝑆 ⊆ (Base‘𝐻) → (𝑥 ∈ (𝑌‘𝑆) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥))))
54	51, 53	syl 14	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) ∧ 𝐺 ∈ V) → (𝑥 ∈ (𝑌‘𝑆) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)𝑥))))
55		elin 3412	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ (𝑍‘𝑆) ∧ 𝑥 ∈ 𝐴))
56	55	biancomi 270	. . . . . . . . . 10 ⊢ (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝑍‘𝑆)))
57		eqid 2238	. . . . . . . . . . . . 13 ⊢ (+g‘𝐺) = (+g‘𝐺)
58	11, 57, 12	elcntz 14148	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ (Base‘𝐺) → (𝑥 ∈ (𝑍‘𝑆) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))))
59	58	adantl 277	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ (𝑍‘𝑆) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))))
60	59	anbi2d 468	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝑍‘𝑆)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))))
61	56, 60	bitrid 192	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))))
62	61	adantr 276	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) ∧ 𝐺 ∈ V) → (𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))))
63	44, 54, 62	3bitr4d 220	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) ∧ 𝐺 ∈ V) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴)))
64	63	ex 115	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝐺 ∈ V → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴))))
65	64	impancom 260	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (𝑆 ⊆ (Base‘𝐺) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴))))
66	26, 30, 65	pm5.21ndd 717	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) ∧ 𝐺 ∈ V) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴)))
67	66	ex 115	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝐺 ∈ V → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴))))
68	8, 16, 67	pm5.21ndd 717	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑥 ∈ (𝑌‘𝑆) ↔ 𝑥 ∈ ((𝑍‘𝑆) ∩ 𝐴)))
69	68	eqrdv 2236	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402  ∃wex 1545   ∈ wcel 2209  ∀wral 2528  Vcvv 2821   ∩ cin 3219   ⊆ wss 3220  ‘cfv 5377  (class class class)co 6085  Basecbs 13404   ↾_s cress 13405  +_gcplusg 13484  Cntzccntz 14140

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-cnex 8271  ax-resscn 8272  ax-1cn 8273  ax-1re 8274  ax-icn 8275  ax-addcl 8276  ax-addrcl 8277  ax-mulcl 8278  ax-addcom 8280  ax-addass 8282  ax-i2m1 8285  ax-0lt1 8286  ax-0id 8288  ax-rnegex 8289  ax-pre-ltirr 8292  ax-pre-ltadd 8296

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-ov 6088  df-oprab 6089  df-mpo 6090  df-pnf 8363  df-mnf 8364  df-ltxr 8366  df-inn 9308  df-2 9366  df-ndx 13407  df-slot 13408  df-base 13410  df-sets 13411  df-iress 13412  df-plusg 13497  df-cntz 14142

This theorem is used by: (None)