Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋)) |
2 | | fvexd 6203 |
. . . . . . 7
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (unifTop‘𝑈) ∈ V) |
3 | | elfvex 6221 |
. . . . . . . . 9
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V) |
4 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V) |
5 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) |
6 | 4, 5 | ssexd 4805 |
. . . . . . 7
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V) |
7 | | elrest 16088 |
. . . . . . 7
⊢
(((unifTop‘𝑈)
∈ V ∧ 𝐴 ∈ V)
→ (𝑏 ∈
((unifTop‘𝑈)
↾t 𝐴)
↔ ∃𝑎 ∈
(unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))) |
8 | 2, 6, 7 | syl2anc 693 |
. . . . . 6
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))) |
9 | 8 | biimpa 501 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)) |
10 | | inss2 3834 |
. . . . . . 7
⊢ (𝑎 ∩ 𝐴) ⊆ 𝐴 |
11 | | sseq1 3626 |
. . . . . . 7
⊢ (𝑏 = (𝑎 ∩ 𝐴) → (𝑏 ⊆ 𝐴 ↔ (𝑎 ∩ 𝐴) ⊆ 𝐴)) |
12 | 10, 11 | mpbiri 248 |
. . . . . 6
⊢ (𝑏 = (𝑎 ∩ 𝐴) → 𝑏 ⊆ 𝐴) |
13 | 12 | rexlimivw 3029 |
. . . . 5
⊢
(∃𝑎 ∈
(unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴) → 𝑏 ⊆ 𝐴) |
14 | 9, 13 | syl 17 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → 𝑏 ⊆ 𝐴) |
15 | | simp-5l 808 |
. . . . . . . . . 10
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑈 ∈ (UnifOn‘𝑋)) |
16 | 15 | ad2antrr 762 |
. . . . . . . . 9
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋)) |
17 | 6 | ad6antr 772 |
. . . . . . . . . 10
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝐴 ∈ V) |
18 | | xpexg 6960 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) → (𝐴 × 𝐴) ∈ V) |
19 | 17, 17, 18 | syl2anc 693 |
. . . . . . . . 9
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → (𝐴 × 𝐴) ∈ V) |
20 | | simplr 792 |
. . . . . . . . 9
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝑢 ∈ 𝑈) |
21 | | elrestr 16089 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑢 ∈ 𝑈) → (𝑢 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴))) |
22 | 16, 19, 20, 21 | syl3anc 1326 |
. . . . . . . 8
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → (𝑢 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴))) |
23 | | inss1 3833 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑢 |
24 | | imass1 5500 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑢 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑢 “ {𝑥})) |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑢 “ {𝑥}) |
26 | | sstr 3611 |
. . . . . . . . . . . 12
⊢ ((((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑢 “ {𝑥}) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑎) |
27 | 25, 26 | mpan 706 |
. . . . . . . . . . 11
⊢ ((𝑢 “ {𝑥}) ⊆ 𝑎 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑎) |
28 | | imassrn 5477 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ ran (𝑢 ∩ (𝐴 × 𝐴)) |
29 | | rnin 5542 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑢 ∩ (𝐴 × 𝐴)) ⊆ (ran 𝑢 ∩ ran (𝐴 × 𝐴)) |
30 | 28, 29 | sstri 3612 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (ran 𝑢 ∩ ran (𝐴 × 𝐴)) |
31 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑢 ∩ ran (𝐴 × 𝐴)) ⊆ ran (𝐴 × 𝐴) |
32 | 30, 31 | sstri 3612 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ ran (𝐴 × 𝐴) |
33 | | rnxpid 5567 |
. . . . . . . . . . . . 13
⊢ ran
(𝐴 × 𝐴) = 𝐴 |
34 | 32, 33 | sseqtri 3637 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝐴 |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑢 “ {𝑥}) ⊆ 𝑎 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝐴) |
36 | 27, 35 | ssind 3837 |
. . . . . . . . . 10
⊢ ((𝑢 “ {𝑥}) ⊆ 𝑎 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑎 ∩ 𝐴)) |
37 | 36 | adantl 482 |
. . . . . . . . 9
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑎 ∩ 𝐴)) |
38 | | simpllr 799 |
. . . . . . . . 9
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝑏 = (𝑎 ∩ 𝐴)) |
39 | 37, 38 | sseqtr4d 3642 |
. . . . . . . 8
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑏) |
40 | | imaeq1 5461 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) → (𝑣 “ {𝑥}) = ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥})) |
41 | 40 | sseq1d 3632 |
. . . . . . . . 9
⊢ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) → ((𝑣 “ {𝑥}) ⊆ 𝑏 ↔ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑏)) |
42 | 41 | rspcev 3309 |
. . . . . . . 8
⊢ (((𝑢 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑏) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏) |
43 | 22, 39, 42 | syl2anc 693 |
. . . . . . 7
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏) |
44 | | simplr 792 |
. . . . . . . 8
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑎 ∈ (unifTop‘𝑈)) |
45 | | inss1 3833 |
. . . . . . . . 9
⊢ (𝑎 ∩ 𝐴) ⊆ 𝑎 |
46 | | simpllr 799 |
. . . . . . . . . 10
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑥 ∈ 𝑏) |
47 | | simpr 477 |
. . . . . . . . . 10
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑏 = (𝑎 ∩ 𝐴)) |
48 | 46, 47 | eleqtrd 2703 |
. . . . . . . . 9
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑥 ∈ (𝑎 ∩ 𝐴)) |
49 | 45, 48 | sseldi 3601 |
. . . . . . . 8
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑥 ∈ 𝑎) |
50 | | elutop 22037 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑎 ∈ (unifTop‘𝑈) ↔ (𝑎 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑎 ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎))) |
51 | 50 | simplbda 654 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ (unifTop‘𝑈)) → ∀𝑥 ∈ 𝑎 ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎) |
52 | 51 | r19.21bi 2932 |
. . . . . . . 8
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑥 ∈ 𝑎) → ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎) |
53 | 15, 44, 49, 52 | syl21anc 1325 |
. . . . . . 7
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎) |
54 | 43, 53 | r19.29a 3078 |
. . . . . 6
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏) |
55 | 9 | adantr 481 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)) |
56 | 54, 55 | r19.29a 3078 |
. . . . 5
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏) |
57 | 56 | ralrimiva 2966 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏) |
58 | | trust 22033 |
. . . . . 6
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴)) |
59 | | elutop 22037 |
. . . . . 6
⊢ ((𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏))) |
60 | 58, 59 | syl 17 |
. . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏))) |
61 | 60 | biimpar 502 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)) → 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) |
62 | 1, 14, 57, 61 | syl12anc 1324 |
. . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) |
63 | 62 | ex 450 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) → 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))) |
64 | 63 | ssrdv 3609 |
1
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) |