Theorem tendoset 41266

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 41265	. . . 4 ⊢ (𝐾 ∈ 𝑉 → (TEndo‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))}))
5	4	fveq1d 6833	. . 3 ⊢ (𝐾 ∈ 𝑉 → ((TEndo‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})‘𝑊))
6		fveq2 6831	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊))
7	6, 6	feq23d 6654	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ↔ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)))
8	6	raleqdv 3299	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔))))
9	6, 8	raleqbidv 3315	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔))))
10		fveq2 6831	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = ((trL‘𝐾)‘𝑊))
11		tendoset.r	. . . . . . . . . . 11 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
12	10, 11	eqtr4di 2794	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = 𝑅)
13	12	fveq1d 6833	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) = (𝑅‘(𝑠‘𝑓)))
14	12	fveq1d 6833	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (((trL‘𝐾)‘𝑤)‘𝑓) = (𝑅‘𝑓))
15	13, 14	breq12d 5088	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓) ↔ (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)))
16	6, 15	raleqbidv 3315	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)))
17	7, 9, 16	3anbi123d 1445	. . . . . 6 ⊢ (𝑤 = 𝑊 → ((𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓)) ↔ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))))
18	17	abbidv 2807	. . . . 5 ⊢ (𝑤 = 𝑊 → {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))} = {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})
19		eqid 2741	. . . . 5 ⊢ (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))}) = (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})
20		fvex 6844	. . . . . . . 8 ⊢ ((LTrn‘𝐾)‘𝑊) ∈ V
21	20, 20	mapval 8779	. . . . . . 7 ⊢ (((LTrn‘𝐾)‘𝑊) ↑m ((LTrn‘𝐾)‘𝑊)) = {𝑠 ∣ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)}
22		ovex 7393	. . . . . . 7 ⊢ (((LTrn‘𝐾)‘𝑊) ↑m ((LTrn‘𝐾)‘𝑊)) ∈ V
23	21, 22	eqeltrri 2838	. . . . . 6 ⊢ {𝑠 ∣ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)} ∈ V
24		simp1 1143	. . . . . . 7 ⊢ ((𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)) → 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊))
25	24	ss2abi 4000	. . . . . 6 ⊢ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} ⊆ {𝑠 ∣ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)}
26	23, 25	ssexi 5253	. . . . 5 ⊢ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} ∈ V
27	18, 19, 26	fvmpt 6939	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})‘𝑊) = {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})
28		tendoset.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
29	28, 28	feq23i 6653	. . . . . 6 ⊢ (𝑠:𝑇⟶𝑇 ↔ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊))
30	28	raleqi 3297	. . . . . . 7 ⊢ (∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)))
31	28, 30	raleqbii 3313	. . . . . 6 ⊢ (∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)))
32	28	raleqi 3297	. . . . . 6 ⊢ (∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))
33	29, 31, 32	3anbi123i 1162	. . . . 5 ⊢ ((𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)) ↔ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)))
34	33	abbii 2808	. . . 4 ⊢ {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} = {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))}
35	27, 34	eqtr4di 2794	. . 3 ⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})‘𝑊) = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})
36	5, 35	sylan9eq 2796	. 2 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → ((TEndo‘𝐾)‘𝑊) = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})
37	1, 36	eqtrid 2788	1 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐸 = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))})

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121  {cab 2719  ∀wral 3055  Vcvv 3433   class class class wbr 5075   ↦ cmpt 5156   ∘ ccom 5625  ⟶wf 6485  ‘cfv 6489  (class class class)co 7360   ↑_m cmap 8767  lecple 17222  LHypclh 40491  LTrncltrn 40608  trLctrl 40665  TEndoctendo 41259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-oprab 7364  df-mpo 7365  df-map 8769  df-tendo 41262

This theorem is referenced by:  istendo  41267