Step | Hyp | Ref
| Expression |
1 | | mrsubvr.v |
. . . . . . 7
⊢ 𝑉 = (mVR‘𝑇) |
2 | | mrsubvr.r |
. . . . . . 7
⊢ 𝑅 = (mREx‘𝑇) |
3 | | mrsubvr.s |
. . . . . . 7
⊢ 𝑆 = (mRSubst‘𝑇) |
4 | 1, 2, 3 | mrsubff 33045 |
. . . . . 6
⊢ (𝑇 ∈ V → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅)) |
5 | 4 | ffnd 6505 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
6 | | eleq1w 2815 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑣 → (𝑥 ∈ dom 𝑓 ↔ 𝑣 ∈ dom 𝑓)) |
7 | | fveq2 6674 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑣 → (𝑓‘𝑥) = (𝑓‘𝑣)) |
8 | | s1eq 14043 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑣 → 〈“𝑥”〉 = 〈“𝑣”〉) |
9 | 6, 7, 8 | ifbieq12d 4442 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑣 → if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉) = if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
10 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) = (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) |
11 | | fvex 6687 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓‘𝑣) ∈ V |
12 | | s1cli 14048 |
. . . . . . . . . . . . . . . . . . 19
⊢
〈“𝑣”〉 ∈ Word V |
13 | 12 | elexi 3417 |
. . . . . . . . . . . . . . . . . 18
⊢
〈“𝑣”〉 ∈ V |
14 | 11, 13 | ifex 4464 |
. . . . . . . . . . . . . . . . 17
⊢ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉) ∈ V |
15 | 9, 10, 14 | fvmpt 6775 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ 𝑉 → ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣) = if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
16 | 15 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑣 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣) = if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
17 | 16 | ifeq1da 4445 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉) = if(𝑣 ∈ 𝑉, if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉), 〈“𝑣”〉)) |
18 | | ifan 4467 |
. . . . . . . . . . . . . 14
⊢ if((𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓), (𝑓‘𝑣), 〈“𝑣”〉) = if(𝑣 ∈ 𝑉, if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉), 〈“𝑣”〉) |
19 | 17, 18 | eqtr4di 2791 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉) = if((𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓), (𝑓‘𝑣), 〈“𝑣”〉)) |
20 | | elpmi 8456 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) → (𝑓:dom 𝑓⟶𝑅 ∧ dom 𝑓 ⊆ 𝑉)) |
21 | 20 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑓:dom 𝑓⟶𝑅 ∧ dom 𝑓 ⊆ 𝑉)) |
22 | 21 | simprd 499 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → dom 𝑓 ⊆ 𝑉) |
23 | 22 | sseld 3876 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑣 ∈ dom 𝑓 → 𝑣 ∈ 𝑉)) |
24 | 23 | pm4.71rd 566 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑣 ∈ dom 𝑓 ↔ (𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓))) |
25 | 24 | bicomd 226 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓) ↔ 𝑣 ∈ dom 𝑓)) |
26 | 25 | ifbid 4437 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → if((𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓), (𝑓‘𝑣), 〈“𝑣”〉) = if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
27 | 19, 26 | eqtr2d 2774 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉) = if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) |
28 | 27 | mpteq2dv 5126 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) = (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉))) |
29 | 28 | coeq1d 5704 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒) = ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) |
30 | 29 | oveq2d 7186 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) = ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) |
31 | 30 | mpteq2dv 5126 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
32 | | eqid 2738 |
. . . . . . . . . 10
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
33 | | eqid 2738 |
. . . . . . . . . 10
⊢
(freeMnd‘((mCN‘𝑇) ∪ 𝑉)) = (freeMnd‘((mCN‘𝑇) ∪ 𝑉)) |
34 | 32, 1, 2, 3, 33 | mrsubfval 33041 |
. . . . . . . . 9
⊢ ((𝑓:dom 𝑓⟶𝑅 ∧ dom 𝑓 ⊆ 𝑉) → (𝑆‘𝑓) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
35 | 21, 34 | syl 17 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘𝑓) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
36 | 21 | simpld 498 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → 𝑓:dom 𝑓⟶𝑅) |
37 | 36 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) → 𝑓:dom 𝑓⟶𝑅) |
38 | 37 | ffvelrnda 6861 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ 𝑅) |
39 | | elun2 4067 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∈ ((mCN‘𝑇) ∪ 𝑉)) |
40 | 39 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 𝑥 ∈ ((mCN‘𝑇) ∪ 𝑉)) |
41 | 40 | s1cld 14046 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 〈“𝑥”〉 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
42 | 32, 1, 2 | mrexval 33034 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
43 | 42 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
44 | 41, 43 | eleqtrrd 2836 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 〈“𝑥”〉 ∈ 𝑅) |
45 | 38, 44 | ifclda 4449 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) → if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉) ∈ 𝑅) |
46 | 45 | fmpttd 6889 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)):𝑉⟶𝑅) |
47 | | ssid 3899 |
. . . . . . . . 9
⊢ 𝑉 ⊆ 𝑉 |
48 | 32, 1, 2, 3, 33 | mrsubfval 33041 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
49 | 46, 47, 48 | sylancl 589 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
50 | 31, 35, 49 | 3eqtr4d 2783 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘𝑓) = (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)))) |
51 | 5 | adantr 484 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
52 | | mapsspm 8486 |
. . . . . . . . 9
⊢ (𝑅 ↑m 𝑉) ⊆ (𝑅 ↑pm 𝑉) |
53 | 52 | a1i 11 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑅 ↑m 𝑉) ⊆ (𝑅 ↑pm 𝑉)) |
54 | 2 | fvexi 6688 |
. . . . . . . . . 10
⊢ 𝑅 ∈ V |
55 | 1 | fvexi 6688 |
. . . . . . . . . 10
⊢ 𝑉 ∈ V |
56 | 54, 55 | elmap 8481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) ∈ (𝑅 ↑m 𝑉) ↔ (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)):𝑉⟶𝑅) |
57 | 46, 56 | sylibr 237 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) ∈ (𝑅 ↑m 𝑉)) |
58 | | fnfvima 7006 |
. . . . . . . 8
⊢ ((𝑆 Fn (𝑅 ↑pm 𝑉) ∧ (𝑅 ↑m 𝑉) ⊆ (𝑅 ↑pm 𝑉) ∧ (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) ∈ (𝑅 ↑m 𝑉)) → (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
59 | 51, 53, 57, 58 | syl3anc 1372 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
60 | 50, 59 | eqeltrd 2833 |
. . . . . 6
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘𝑓) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
61 | 60 | ralrimiva 3096 |
. . . . 5
⊢ (𝑇 ∈ V → ∀𝑓 ∈ (𝑅 ↑pm 𝑉)(𝑆‘𝑓) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
62 | | ffnfv 6892 |
. . . . 5
⊢ (𝑆:(𝑅 ↑pm 𝑉)⟶(𝑆 “ (𝑅 ↑m 𝑉)) ↔ (𝑆 Fn (𝑅 ↑pm 𝑉) ∧ ∀𝑓 ∈ (𝑅 ↑pm 𝑉)(𝑆‘𝑓) ∈ (𝑆 “ (𝑅 ↑m 𝑉)))) |
63 | 5, 61, 62 | sylanbrc 586 |
. . . 4
⊢ (𝑇 ∈ V → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑆 “ (𝑅 ↑m 𝑉))) |
64 | 63 | frnd 6512 |
. . 3
⊢ (𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑m 𝑉))) |
65 | 3 | rnfvprc 6668 |
. . . 4
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
66 | | 0ss 4285 |
. . . 4
⊢ ∅
⊆ (𝑆 “ (𝑅 ↑m 𝑉)) |
67 | 65, 66 | eqsstrdi 3931 |
. . 3
⊢ (¬
𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑m 𝑉))) |
68 | 64, 67 | pm2.61i 185 |
. 2
⊢ ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑m 𝑉)) |
69 | | imassrn 5914 |
. 2
⊢ (𝑆 “ (𝑅 ↑m 𝑉)) ⊆ ran 𝑆 |
70 | 68, 69 | eqssi 3893 |
1
⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑m 𝑉)) |