Theorem tendoset 42007

Description: The set of trace-preserving endomorphisms on the set of translations for a fiducial co-atom 𝑊. (Contributed by NM, 8-Jun-2013.)

Hypotheses

Ref	Expression
tendoset.l	⊢ ≤ = (le‘𝐾)
tendoset.h	⊢ 𝐻 = (LHyp‘𝐾)
tendoset.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
tendoset.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
tendoset.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)

Assertion

Ref	Expression
tendoset	⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐸 = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})

Distinct variable groups:   𝑓,𝑠,𝑔,𝐾   𝑇,𝑓,𝑔,𝑠   𝑊,𝑠,𝑓,𝑔

Allowed substitution hints:   𝑅(𝑓, 𝑔, 𝑠)   𝐸(𝑓, 𝑔, 𝑠)   𝐻(𝑓, 𝑔, 𝑠)   ≤ (𝑓, 𝑔, 𝑠)   𝑉(𝑓, 𝑔, 𝑠)

Proof of Theorem tendoset

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		tendoset.e	. 2 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
2		tendoset.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
3		tendoset.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
4	2, 3	tendofset 42006	. . . 4 ⊢ (𝐾 ∈ 𝑉 → (TEndo‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))}))
5	4	fveq1d 6907	. . 3 ⊢ (𝐾 ∈ 𝑉 → ((TEndo‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})‘𝑊))
6		fveq2 6905	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊))
7	6, 6	feq23d 6723	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ↔ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)))
8	6	raleqdv 3323	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔))))
9	6, 8	raleqbidv 3338	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔))))
10		fveq2 6905	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = ((trL‘𝐾)‘𝑊))
11		tendoset.r	. . . . . . . . . . 11 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
12	10, 11	eqtr4di 2816	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = 𝑅)
13	12	fveq1d 6907	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) = (𝑅‘(𝑠‘𝑓)))
14	12	fveq1d 6907	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (((trL‘𝐾)‘𝑤)‘𝑓) = (𝑅‘𝑓))
15	13, 14	breq12d 5119	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓) ↔ (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)))
16	6, 15	raleqbidv 3338	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)))
17	7, 9, 16	3anbi123d 1465	. . . . . 6 ⊢ (𝑤 = 𝑊 → ((𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓)) ↔ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))))
18	17	abbidv 2829	. . . . 5 ⊢ (𝑤 = 𝑊 → {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))} = {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})
19		eqid 2763	. . . . 5 ⊢ (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))}) = (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})
20		fvex 6918	. . . . . . . 8 ⊢ ((LTrn‘𝐾)‘𝑊) ∈ V
21	20, 20	mapval 8883	. . . . . . 7 ⊢ (((LTrn‘𝐾)‘𝑊) ↑m ((LTrn‘𝐾)‘𝑊)) = {𝑠 ∣ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)}
22		ovex 7473	. . . . . . 7 ⊢ (((LTrn‘𝐾)‘𝑊) ↑m ((LTrn‘𝐾)‘𝑊)) ∈ V
23	21, 22	eqeltrri 2861	. . . . . 6 ⊢ {𝑠 ∣ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)} ∈ V
24		simp1 1154	. . . . . . 7 ⊢ ((𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)) → 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊))
25	24	ss2abi 3994	. . . . . 6 ⊢ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} ⊆ {𝑠 ∣ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)}
26	23, 25	ssexi 5288	. . . . 5 ⊢ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} ∈ V
27	18, 19, 26	fvmpt 7013	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})‘𝑊) = {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})
28		tendoset.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
29	28, 28	feq23i 6722	. . . . . 6 ⊢ (𝑠:𝑇⟶𝑇 ↔ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊))
30	28	raleqi 3321	. . . . . . 7 ⊢ (∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)))
31	28, 30	raleqbii 3336	. . . . . 6 ⊢ (∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)))
32	28	raleqi 3321	. . . . . 6 ⊢ (∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))
33	29, 31, 32	3anbi123i 1173	. . . . 5 ⊢ ((𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)) ↔ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)))
34	33	abbii 2830	. . . 4 ⊢ {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} = {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))}
35	27, 34	eqtr4di 2816	. . 3 ⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})‘𝑊) = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})
36	5, 35	sylan9eq 2818	. 2 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → ((TEndo‘𝐾)‘𝑊) = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})
37	1, 36	eqtrid 2810	1 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐸 = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  {cab 2741  ∀wral 3080  Vcvv 3454   class class class wbr 5106   ↦ cmpt 5189   ∘ ccom 5659  ⟶wf 6551  ‘cfv 6555  (class class class)co 7440   ↑_m cmap 8872  lecple 17461  LHypclh 41232  LTrncltrn 41349  trLctrl 41406  TEndoctendo 42000

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-oprab 7444  df-mpo 7445  df-map 8874  df-tendo 42003

This theorem is used by:  istendo  42008