Proof of Theorem xkocnv
Step | Hyp | Ref
| Expression |
1 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
2 | | xkohmeo.x |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
3 | 2 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐽 ∈ (TopOn‘𝑋)) |
4 | | xkohmeo.y |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
5 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐾 ∈ (TopOn‘𝑌)) |
6 | | txtopon 22335 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
7 | 2, 4, 6 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
8 | 7 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
9 | | xkohmeo.l |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ Top) |
10 | | toptopon2 21662 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
11 | 9, 10 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
12 | 11 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
13 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
14 | | cnf2 21993 |
. . . . . . . . . . . 12
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿) |
15 | 8, 12, 13, 14 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿) |
16 | 15 | ffnd 6499 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌)) |
17 | | fnov 7291 |
. . . . . . . . . 10
⊢ (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
18 | 16, 17 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
19 | 18, 13 | eqeltrrd 2834 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
20 | 3, 5, 19 | cnmpt2k 22432 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) |
21 | 20 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) |
22 | 1, 21 | eqeltrd 2833 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) |
23 | 18 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
24 | | eqid 2738 |
. . . . . . 7
⊢ 𝑋 = 𝑋 |
25 | | nfv 1920 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝜑 |
26 | | nfv 1920 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) |
27 | | nfmpt1 5125 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
28 | 27 | nfeq2 2916 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
29 | 26, 28 | nfan 1905 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
30 | 25, 29 | nfan 1905 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) |
31 | | nfv 1920 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝜑 |
32 | | nfv 1920 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) |
33 | | nfcv 2899 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦𝑋 |
34 | | nfmpt1 5125 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦(𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) |
35 | 33, 34 | nfmpt 5124 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
36 | 35 | nfeq2 2916 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
37 | 32, 36 | nfan 1905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
38 | 31, 37 | nfan 1905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) |
39 | | nfv 1920 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑥 ∈ 𝑋 |
40 | 38, 39 | nfan 1905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) |
41 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
42 | 41 | fveq1d 6670 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥)) |
43 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋) |
44 | | toponmax 21670 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾) |
45 | 4, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑌 ∈ 𝐾) |
46 | 45 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ∈ 𝐾) |
47 | 46 | mptexd 6991 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) |
48 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
49 | 48 | fvmpt2 6780 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
50 | 43, 47, 49 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
51 | 42, 50 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
52 | 51 | fveq1d 6670 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦)) |
53 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌) |
54 | | ovex 7197 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝑓𝑦) ∈ V |
55 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) |
56 | 55 | fvmpt2 6780 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦)) |
57 | 53, 54, 56 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦)) |
58 | 52, 57 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)) |
59 | 58 | expr 460 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) |
60 | 40, 59 | ralrimi 3127 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)) |
61 | | eqid 2738 |
. . . . . . . . . 10
⊢ 𝑌 = 𝑌 |
62 | 60, 61 | jctil 523 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) |
63 | 62 | ex 416 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))) |
64 | 30, 63 | ralrimi 3127 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) |
65 | | mpoeq123 7234 |
. . . . . . 7
⊢ ((𝑋 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
66 | 24, 64, 65 | sylancr 590 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
67 | 23, 66 | eqtr4d 2776 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
68 | 22, 67 | jca 515 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
69 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
70 | 2 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐽 ∈ (TopOn‘𝑋)) |
71 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ (TopOn‘𝑌)) |
72 | 11 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
73 | | xkohmeo.k |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
Comp) |
74 | 73 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ 𝑛-Locally
Comp) |
75 | | nllytop 22217 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ 𝑛-Locally Comp
→ 𝐾 ∈
Top) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ Top) |
77 | 9 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐿 ∈ Top) |
78 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾) |
79 | 78 | xkotopon 22344 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
80 | 76, 77, 79 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
81 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) |
82 | | cnf2 21993 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿)) |
83 | 70, 80, 81, 82 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿)) |
84 | 83 | feqmptd 6731 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥))) |
85 | 4 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌)) |
86 | 11 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
87 | 83 | ffvelrnda 6855 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿)) |
88 | | cnf2 21993 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔‘𝑥):𝑌⟶∪ 𝐿) |
89 | 85, 86, 87, 88 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥):𝑌⟶∪ 𝐿) |
90 | 89 | feqmptd 6731 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
91 | 90 | mpteq2dva 5122 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
92 | 84, 91 | eqtrd 2773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
93 | 92, 81 | eqeltrrd 2834 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) |
94 | 70, 71, 72, 74, 93 | cnmptk2 22430 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
95 | 94 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
96 | 69, 95 | eqeltrd 2833 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
97 | 92 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
98 | | nfv 1920 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) |
99 | | nfmpo1 7242 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
100 | 99 | nfeq2 2916 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
101 | 98, 100 | nfan 1905 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
102 | 25, 101 | nfan 1905 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
103 | | nfv 1920 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) |
104 | | nfmpo2 7243 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
105 | 104 | nfeq2 2916 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
106 | 103, 105 | nfan 1905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
107 | 31, 106 | nfan 1905 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
108 | 107, 39 | nfan 1905 |
. . . . . . . . 9
⊢
Ⅎ𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) |
109 | 69 | oveqd 7181 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦)) |
110 | | fvex 6681 |
. . . . . . . . . . . 12
⊢ ((𝑔‘𝑥)‘𝑦) ∈ V |
111 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
112 | 111 | ovmpt4g 7306 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ ((𝑔‘𝑥)‘𝑦) ∈ V) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦)) |
113 | 110, 112 | mp3an3 1451 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦)) |
114 | 109, 113 | sylan9eq 2793 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) |
115 | 114 | expr 460 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))) |
116 | 108, 115 | ralrimi 3127 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) |
117 | | mpteq12 5114 |
. . . . . . . 8
⊢ ((𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
118 | 61, 116, 117 | sylancr 590 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
119 | 102, 118 | mpteq2da 5121 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
120 | 97, 119 | eqtr4d 2776 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
121 | 96, 120 | jca 515 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) |
122 | 68, 121 | impbida 801 |
. . 3
⊢ (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))) |
123 | 122 | opabbidv 5093 |
. 2
⊢ (𝜑 → {〈𝑔, 𝑓〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {〈𝑔, 𝑓〉 ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))}) |
124 | | xkohmeo.f |
. . . . 5
⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
125 | | df-mpt 5108 |
. . . . 5
⊢ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) = {〈𝑓, 𝑔〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
126 | 124, 125 | eqtri 2761 |
. . . 4
⊢ 𝐹 = {〈𝑓, 𝑔〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
127 | 126 | cnveqi 5711 |
. . 3
⊢ ◡𝐹 = ◡{〈𝑓, 𝑔〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
128 | | cnvopab 5965 |
. . 3
⊢ ◡{〈𝑓, 𝑔〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {〈𝑔, 𝑓〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
129 | 127, 128 | eqtri 2761 |
. 2
⊢ ◡𝐹 = {〈𝑔, 𝑓〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
130 | | df-mpt 5108 |
. 2
⊢ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) = {〈𝑔, 𝑓〉 ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))} |
131 | 123, 129,
130 | 3eqtr4g 2798 |
1
⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |