Step | Hyp | Ref
| Expression |
1 | | eqid 2795 |
. 2
⊢ (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))) |
2 | | mapfien.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) |
3 | | f1of 6488 |
. . . . . . 7
⊢ (𝐺:𝐵–1-1-onto→𝐷 → 𝐺:𝐵⟶𝐷) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺:𝐵⟶𝐷) |
5 | 4 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝐺:𝐵⟶𝐷) |
6 | | breq1 4969 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑓 → (𝑥 finSupp 𝑍 ↔ 𝑓 finSupp 𝑍)) |
7 | | mapfien.s |
. . . . . . . . . 10
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} |
8 | 6, 7 | elrab2 3622 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑓 finSupp 𝑍)) |
9 | 8 | simplbi 498 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑆 → 𝑓 ∈ (𝐵 ↑𝑚 𝐴)) |
10 | 9 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝑓 ∈ (𝐵 ↑𝑚 𝐴)) |
11 | | elmapi 8283 |
. . . . . . 7
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝐴) → 𝑓:𝐴⟶𝐵) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝑓:𝐴⟶𝐵) |
13 | | mapfien.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) |
14 | | f1of 6488 |
. . . . . . . 8
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝐹:𝐶⟶𝐴) |
17 | | fco 6404 |
. . . . . 6
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝐹:𝐶⟶𝐴) → (𝑓 ∘ 𝐹):𝐶⟶𝐵) |
18 | 12, 16, 17 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝑓 ∘ 𝐹):𝐶⟶𝐵) |
19 | | fco 6404 |
. . . . 5
⊢ ((𝐺:𝐵⟶𝐷 ∧ (𝑓 ∘ 𝐹):𝐶⟶𝐵) → (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷) |
20 | 5, 18, 19 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷) |
21 | | mapfien.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ V) |
22 | | mapfien.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ V) |
23 | 21, 22 | elmapd 8275 |
. . . . 5
⊢ (𝜑 → ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑𝑚 𝐶) ↔ (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷)) |
24 | 23 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑𝑚 𝐶) ↔ (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷)) |
25 | 20, 24 | mpbird 258 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑𝑚 𝐶)) |
26 | | mapfien.t |
. . . 4
⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑𝑚 𝐶) ∣ 𝑥 finSupp 𝑊} |
27 | | mapfien.w |
. . . 4
⊢ 𝑊 = (𝐺‘𝑍) |
28 | | mapfien.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ V) |
29 | | mapfien.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ V) |
30 | | mapfien.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
31 | 7, 26, 27, 13, 2, 28, 29, 22, 21, 30 | mapfienlem1 8719 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊) |
32 | | breq1 4969 |
. . . 4
⊢ (𝑥 = (𝐺 ∘ (𝑓 ∘ 𝐹)) → (𝑥 finSupp 𝑊 ↔ (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊)) |
33 | 32, 26 | elrab2 3622 |
. . 3
⊢ ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ 𝑇 ↔ ((𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ (𝐷 ↑𝑚 𝐶) ∧ (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊)) |
34 | 25, 31, 33 | sylanbrc 583 |
. 2
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) ∈ 𝑇) |
35 | 7, 26, 27, 13, 2, 28, 29, 22, 21, 30 | mapfienlem3 8721 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∈ 𝑆) |
36 | | coass 5998 |
. . . . . 6
⊢ (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) = ((◡𝐺 ∘ 𝑔) ∘ (◡𝐹 ∘ 𝐹)) |
37 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝐹:𝐶–1-1-onto→𝐴) |
38 | | f1ococnv1 6516 |
. . . . . . . . 9
⊢ (𝐹:𝐶–1-1-onto→𝐴 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐶)) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐶)) |
40 | 39 | coeq2d 5624 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) ∘ (◡𝐹 ∘ 𝐹)) = ((◡𝐺 ∘ 𝑔) ∘ ( I ↾ 𝐶))) |
41 | | f1ocnv 6500 |
. . . . . . . . . . . 12
⊢ (𝐺:𝐵–1-1-onto→𝐷 → ◡𝐺:𝐷–1-1-onto→𝐵) |
42 | | f1of 6488 |
. . . . . . . . . . . 12
⊢ (◡𝐺:𝐷–1-1-onto→𝐵 → ◡𝐺:𝐷⟶𝐵) |
43 | 2, 41, 42 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝐺:𝐷⟶𝐵) |
44 | 43 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ◡𝐺:𝐷⟶𝐵) |
45 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → 𝑔 ∈ 𝑇) |
46 | | breq1 4969 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑔 → (𝑥 finSupp 𝑊 ↔ 𝑔 finSupp 𝑊)) |
47 | 46, 26 | elrab2 3622 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ 𝑇 ↔ (𝑔 ∈ (𝐷 ↑𝑚 𝐶) ∧ 𝑔 finSupp 𝑊)) |
48 | 45, 47 | sylib 219 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → (𝑔 ∈ (𝐷 ↑𝑚 𝐶) ∧ 𝑔 finSupp 𝑊)) |
49 | 48 | simpld 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → 𝑔 ∈ (𝐷 ↑𝑚 𝐶)) |
50 | | elmapi 8283 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ (𝐷 ↑𝑚 𝐶) → 𝑔:𝐶⟶𝐷) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → 𝑔:𝐶⟶𝐷) |
52 | | fco 6404 |
. . . . . . . . . 10
⊢ ((◡𝐺:𝐷⟶𝐵 ∧ 𝑔:𝐶⟶𝐷) → (◡𝐺 ∘ 𝑔):𝐶⟶𝐵) |
53 | 44, 51, 52 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → (◡𝐺 ∘ 𝑔):𝐶⟶𝐵) |
54 | 53 | adantrl 712 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (◡𝐺 ∘ 𝑔):𝐶⟶𝐵) |
55 | | fcoi1 6425 |
. . . . . . . 8
⊢ ((◡𝐺 ∘ 𝑔):𝐶⟶𝐵 → ((◡𝐺 ∘ 𝑔) ∘ ( I ↾ 𝐶)) = (◡𝐺 ∘ 𝑔)) |
56 | 54, 55 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) ∘ ( I ↾ 𝐶)) = (◡𝐺 ∘ 𝑔)) |
57 | 40, 56 | eqtrd 2831 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) ∘ (◡𝐹 ∘ 𝐹)) = (◡𝐺 ∘ 𝑔)) |
58 | 36, 57 | syl5eq 2843 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) = (◡𝐺 ∘ 𝑔)) |
59 | 58 | eqeq2d 2805 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((𝑓 ∘ 𝐹) = (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) ↔ (𝑓 ∘ 𝐹) = (◡𝐺 ∘ 𝑔))) |
60 | | coass 5998 |
. . . . . . 7
⊢ ((◡𝐺 ∘ 𝐺) ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) |
61 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝐺:𝐵–1-1-onto→𝐷) |
62 | | f1ococnv1 6516 |
. . . . . . . . . 10
⊢ (𝐺:𝐵–1-1-onto→𝐷 → (◡𝐺 ∘ 𝐺) = ( I ↾ 𝐵)) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (◡𝐺 ∘ 𝐺) = ( I ↾ 𝐵)) |
64 | 63 | coeq1d 5623 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝐺) ∘ (𝑓 ∘ 𝐹)) = (( I ↾ 𝐵) ∘ (𝑓 ∘ 𝐹))) |
65 | 18 | adantrr 713 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (𝑓 ∘ 𝐹):𝐶⟶𝐵) |
66 | | fcoi2 6426 |
. . . . . . . . 9
⊢ ((𝑓 ∘ 𝐹):𝐶⟶𝐵 → (( I ↾ 𝐵) ∘ (𝑓 ∘ 𝐹)) = (𝑓 ∘ 𝐹)) |
67 | 65, 66 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (( I ↾ 𝐵) ∘ (𝑓 ∘ 𝐹)) = (𝑓 ∘ 𝐹)) |
68 | 64, 67 | eqtrd 2831 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝐺) ∘ (𝑓 ∘ 𝐹)) = (𝑓 ∘ 𝐹)) |
69 | 60, 68 | syl5eqr 2845 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∘ 𝐹)) |
70 | 69 | eqeq2d 2805 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ (◡𝐺 ∘ 𝑔) = (𝑓 ∘ 𝐹))) |
71 | | eqcom 2802 |
. . . . 5
⊢ ((◡𝐺 ∘ 𝑔) = (𝑓 ∘ 𝐹) ↔ (𝑓 ∘ 𝐹) = (◡𝐺 ∘ 𝑔)) |
72 | 70, 71 | syl6bb 288 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ (𝑓 ∘ 𝐹) = (◡𝐺 ∘ 𝑔))) |
73 | 59, 72 | bitr4d 283 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((𝑓 ∘ 𝐹) = (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) ↔ (◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))))) |
74 | | f1ofo 6495 |
. . . . 5
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴) |
75 | 37, 74 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝐹:𝐶–onto→𝐴) |
76 | | ffn 6387 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
77 | 10, 11, 76 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → 𝑓 Fn 𝐴) |
78 | 77 | adantrr 713 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝑓 Fn 𝐴) |
79 | | f1ocnv 6500 |
. . . . . . . . 9
⊢ (𝐹:𝐶–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐶) |
80 | | f1of 6488 |
. . . . . . . . 9
⊢ (◡𝐹:𝐴–1-1-onto→𝐶 → ◡𝐹:𝐴⟶𝐶) |
81 | 13, 79, 80 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ◡𝐹:𝐴⟶𝐶) |
82 | 81 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ◡𝐹:𝐴⟶𝐶) |
83 | | fco 6404 |
. . . . . . 7
⊢ (((◡𝐺 ∘ 𝑔):𝐶⟶𝐵 ∧ ◡𝐹:𝐴⟶𝐶) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹):𝐴⟶𝐵) |
84 | 53, 82, 83 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹):𝐴⟶𝐵) |
85 | 84 | ffnd 6388 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) Fn 𝐴) |
86 | 85 | adantrl 712 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) Fn 𝐴) |
87 | | cocan2 6918 |
. . . 4
⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑓 Fn 𝐴 ∧ ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) Fn 𝐴) → ((𝑓 ∘ 𝐹) = (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) ↔ 𝑓 = ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹))) |
88 | 75, 78, 86, 87 | syl3anc 1364 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((𝑓 ∘ 𝐹) = (((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∘ 𝐹) ↔ 𝑓 = ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹))) |
89 | 2, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → ◡𝐺:𝐷–1-1-onto→𝐵) |
90 | 89 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ◡𝐺:𝐷–1-1-onto→𝐵) |
91 | | f1of1 6487 |
. . . . 5
⊢ (◡𝐺:𝐷–1-1-onto→𝐵 → ◡𝐺:𝐷–1-1→𝐵) |
92 | 90, 91 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ◡𝐺:𝐷–1-1→𝐵) |
93 | 51 | adantrl 712 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → 𝑔:𝐶⟶𝐷) |
94 | 20 | adantrr 713 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷) |
95 | | cocan1 6917 |
. . . 4
⊢ ((◡𝐺:𝐷–1-1→𝐵 ∧ 𝑔:𝐶⟶𝐷 ∧ (𝐺 ∘ (𝑓 ∘ 𝐹)):𝐶⟶𝐷) → ((◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ 𝑔 = (𝐺 ∘ (𝑓 ∘ 𝐹)))) |
96 | 92, 93, 94, 95 | syl3anc 1364 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → ((◡𝐺 ∘ 𝑔) = (◡𝐺 ∘ (𝐺 ∘ (𝑓 ∘ 𝐹))) ↔ 𝑔 = (𝐺 ∘ (𝑓 ∘ 𝐹)))) |
97 | 73, 88, 96 | 3bitr3d 310 |
. 2
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇)) → (𝑓 = ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ↔ 𝑔 = (𝐺 ∘ (𝑓 ∘ 𝐹)))) |
98 | 1, 34, 35, 97 | f1o2d 7262 |
1
⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))):𝑆–1-1-onto→𝑇) |