Proof of Theorem symgcom
Step | Hyp | Ref
| Expression |
1 | | symgcom.4 |
. . . 4
⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴) |
2 | 1 | reseq2d 5853 |
. . 3
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑋 ∘ 𝑌) ↾ 𝐴)) |
3 | | resundi 5867 |
. . . 4
⊢ ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹)) |
4 | | symgcom.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
5 | | symgcom.g |
. . . . . . . . . . . . . . 15
⊢ 𝐺 = (SymGrp‘𝐴) |
6 | | symgcom.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝐺) |
7 | 5, 6 | symgbasf1o 18503 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∈ 𝐵 → 𝑌:𝐴–1-1-onto→𝐴) |
8 | 4, 7 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌:𝐴–1-1-onto→𝐴) |
9 | | f1ocnv 6627 |
. . . . . . . . . . . . 13
⊢ (𝑌:𝐴–1-1-onto→𝐴 → ◡𝑌:𝐴–1-1-onto→𝐴) |
10 | | f1ofun 6617 |
. . . . . . . . . . . . 13
⊢ (◡𝑌:𝐴–1-1-onto→𝐴 → Fun ◡𝑌) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun ◡𝑌) |
12 | | f1ofn 6616 |
. . . . . . . . . . . . . 14
⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌 Fn 𝐴) |
13 | | fnresdm 6466 |
. . . . . . . . . . . . . 14
⊢ (𝑌 Fn 𝐴 → (𝑌 ↾ 𝐴) = 𝑌) |
14 | 8, 12, 13 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 ↾ 𝐴) = 𝑌) |
15 | | f1ofo 6622 |
. . . . . . . . . . . . . 14
⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌:𝐴–onto→𝐴) |
16 | 8, 15 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌:𝐴–onto→𝐴) |
17 | | foeq1 6586 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ↾ 𝐴) = 𝑌 → ((𝑌 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑌:𝐴–onto→𝐴)) |
18 | 17 | biimpar 480 |
. . . . . . . . . . . . 13
⊢ (((𝑌 ↾ 𝐴) = 𝑌 ∧ 𝑌:𝐴–onto→𝐴) → (𝑌 ↾ 𝐴):𝐴–onto→𝐴) |
19 | 14, 16, 18 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ↾ 𝐴):𝐴–onto→𝐴) |
20 | | symgcom.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹)) |
21 | | f1oi 6652 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ 𝐹):𝐹–1-1-onto→𝐹 |
22 | | f1ofo 6622 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹–onto→𝐹) |
23 | 21, 22 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( I ↾ 𝐹):𝐹–onto→𝐹) |
24 | | foeq1 6586 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) → ((𝑌 ↾ 𝐹):𝐹–onto→𝐹 ↔ ( I ↾ 𝐹):𝐹–onto→𝐹)) |
25 | 24 | biimpar 480 |
. . . . . . . . . . . . 13
⊢ (((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) ∧ ( I ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ 𝐹):𝐹–onto→𝐹) |
26 | 20, 23, 25 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ↾ 𝐹):𝐹–onto→𝐹) |
27 | | resdif 6635 |
. . . . . . . . . . . 12
⊢ ((Fun
◡𝑌 ∧ (𝑌 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑌 ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹)) |
28 | 11, 19, 26, 27 | syl3anc 1367 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹)) |
29 | | ssun2 4149 |
. . . . . . . . . . . . . . 15
⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹) |
30 | 29, 1 | sseqtrid 4019 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ⊆ 𝐴) |
31 | | incom 4178 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∩ 𝐹) = (𝐹 ∩ 𝐸) |
32 | | symgcom.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅) |
33 | 31, 32 | syl5eqr 2870 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∩ 𝐸) = ∅) |
34 | | uncom 4129 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∪ 𝐹) = (𝐹 ∪ 𝐸) |
35 | 34, 1 | syl5eqr 2870 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∪ 𝐸) = 𝐴) |
36 | | uneqdifeq 4438 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) → ((𝐹 ∪ 𝐸) = 𝐴 ↔ (𝐴 ∖ 𝐹) = 𝐸)) |
37 | 36 | biimpa 479 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) ∧ (𝐹 ∪ 𝐸) = 𝐴) → (𝐴 ∖ 𝐹) = 𝐸) |
38 | 30, 33, 35, 37 | syl21anc 835 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∖ 𝐹) = 𝐸) |
39 | 38 | reseq2d 5853 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)) = (𝑌 ↾ 𝐸)) |
40 | 39, 38, 38 | f1oeq123d 6610 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹) ↔ (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸)) |
41 | 28, 40 | mpbid 234 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸) |
42 | | f1of 6615 |
. . . . . . . . . 10
⊢ ((𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸 → (𝑌 ↾ 𝐸):𝐸⟶𝐸) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸⟶𝐸) |
44 | 43 | frnd 6521 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑌 ↾ 𝐸) ⊆ 𝐸) |
45 | | cores 6102 |
. . . . . . . 8
⊢ (ran
(𝑌 ↾ 𝐸) ⊆ 𝐸 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸))) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸))) |
47 | | resco 6103 |
. . . . . . 7
⊢ ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑋 ∘ (𝑌 ↾ 𝐸)) |
48 | 46, 47 | syl6reqr 2875 |
. . . . . 6
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸))) |
49 | | symgcom.1 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸)) |
50 | 49 | coeq1d 5732 |
. . . . . 6
⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸))) |
51 | | fcoi2 6553 |
. . . . . . 7
⊢ ((𝑌 ↾ 𝐸):𝐸⟶𝐸 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸)) |
52 | 43, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸)) |
53 | 48, 50, 52 | 3eqtrd 2860 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑌 ↾ 𝐸)) |
54 | | resco 6103 |
. . . . . 6
⊢ ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ∘ (𝑌 ↾ 𝐹)) |
55 | 20 | coeq2d 5733 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐹))) |
56 | | coires1 6117 |
. . . . . . 7
⊢ (𝑋 ∘ ( I ↾ 𝐹)) = (𝑋 ↾ 𝐹) |
57 | 55, 56 | syl6eq 2872 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ↾ 𝐹)) |
58 | 54, 57 | syl5eq 2868 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ↾ 𝐹)) |
59 | 53, 58 | uneq12d 4140 |
. . . 4
⊢ (𝜑 → (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹))) |
60 | 3, 59 | syl5eq 2868 |
. . 3
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹))) |
61 | | symgcom.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
62 | 5, 6 | symgbasf1o 18503 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → 𝑋:𝐴–1-1-onto→𝐴) |
63 | 61, 62 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋:𝐴–1-1-onto→𝐴) |
64 | | f1oco 6637 |
. . . . 5
⊢ ((𝑋:𝐴–1-1-onto→𝐴 ∧ 𝑌:𝐴–1-1-onto→𝐴) → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴) |
65 | 63, 8, 64 | syl2anc 586 |
. . . 4
⊢ (𝜑 → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴) |
66 | | f1ofn 6616 |
. . . 4
⊢ ((𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴 → (𝑋 ∘ 𝑌) Fn 𝐴) |
67 | | fnresdm 6466 |
. . . 4
⊢ ((𝑋 ∘ 𝑌) Fn 𝐴 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌)) |
68 | 65, 66, 67 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌)) |
69 | 2, 60, 68 | 3eqtr3d 2864 |
. 2
⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑋 ∘ 𝑌)) |
70 | 1 | reseq2d 5853 |
. . 3
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ∘ 𝑋) ↾ 𝐴)) |
71 | | resundi 5867 |
. . . 4
⊢ ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹)) |
72 | | resco 6103 |
. . . . . 6
⊢ ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ∘ (𝑋 ↾ 𝐸)) |
73 | 49 | coeq2d 5733 |
. . . . . . 7
⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ∘ ( I ↾ 𝐸))) |
74 | | coires1 6117 |
. . . . . . 7
⊢ (𝑌 ∘ ( I ↾ 𝐸)) = (𝑌 ↾ 𝐸) |
75 | 73, 74 | syl6eq 2872 |
. . . . . 6
⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ↾ 𝐸)) |
76 | 72, 75 | syl5eq 2868 |
. . . . 5
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ↾ 𝐸)) |
77 | | f1ocnv 6627 |
. . . . . . . . . . . . 13
⊢ (𝑋:𝐴–1-1-onto→𝐴 → ◡𝑋:𝐴–1-1-onto→𝐴) |
78 | | f1ofun 6617 |
. . . . . . . . . . . . 13
⊢ (◡𝑋:𝐴–1-1-onto→𝐴 → Fun ◡𝑋) |
79 | 63, 77, 78 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun ◡𝑋) |
80 | | f1ofn 6616 |
. . . . . . . . . . . . . 14
⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋 Fn 𝐴) |
81 | | fnresdm 6466 |
. . . . . . . . . . . . . 14
⊢ (𝑋 Fn 𝐴 → (𝑋 ↾ 𝐴) = 𝑋) |
82 | 63, 80, 81 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ↾ 𝐴) = 𝑋) |
83 | | f1ofo 6622 |
. . . . . . . . . . . . . 14
⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋:𝐴–onto→𝐴) |
84 | 63, 83 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋:𝐴–onto→𝐴) |
85 | | foeq1 6586 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ↾ 𝐴) = 𝑋 → ((𝑋 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑋:𝐴–onto→𝐴)) |
86 | 85 | biimpar 480 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ↾ 𝐴) = 𝑋 ∧ 𝑋:𝐴–onto→𝐴) → (𝑋 ↾ 𝐴):𝐴–onto→𝐴) |
87 | 82, 84, 86 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ↾ 𝐴):𝐴–onto→𝐴) |
88 | | f1oi 6652 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ 𝐸):𝐸–1-1-onto→𝐸 |
89 | | f1ofo 6622 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐸):𝐸–1-1-onto→𝐸 → ( I ↾ 𝐸):𝐸–onto→𝐸) |
90 | 88, 89 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( I ↾ 𝐸):𝐸–onto→𝐸) |
91 | | foeq1 6586 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) → ((𝑋 ↾ 𝐸):𝐸–onto→𝐸 ↔ ( I ↾ 𝐸):𝐸–onto→𝐸)) |
92 | 91 | biimpar 480 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) ∧ ( I ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ 𝐸):𝐸–onto→𝐸) |
93 | 49, 90, 92 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ↾ 𝐸):𝐸–onto→𝐸) |
94 | | resdif 6635 |
. . . . . . . . . . . 12
⊢ ((Fun
◡𝑋 ∧ (𝑋 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑋 ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸)) |
95 | 79, 87, 93, 94 | syl3anc 1367 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸)) |
96 | | ssun1 4148 |
. . . . . . . . . . . . . . 15
⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹) |
97 | 96, 1 | sseqtrid 4019 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ⊆ 𝐴) |
98 | | uneqdifeq 4438 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) → ((𝐸 ∪ 𝐹) = 𝐴 ↔ (𝐴 ∖ 𝐸) = 𝐹)) |
99 | 98 | biimpa 479 |
. . . . . . . . . . . . . 14
⊢ (((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) ∧ (𝐸 ∪ 𝐹) = 𝐴) → (𝐴 ∖ 𝐸) = 𝐹) |
100 | 97, 32, 1, 99 | syl21anc 835 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∖ 𝐸) = 𝐹) |
101 | 100 | reseq2d 5853 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)) = (𝑋 ↾ 𝐹)) |
102 | 101, 100,
100 | f1oeq123d 6610 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸) ↔ (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹)) |
103 | 95, 102 | mpbid 234 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹) |
104 | | f1of 6615 |
. . . . . . . . . 10
⊢ ((𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹 → (𝑋 ↾ 𝐹):𝐹⟶𝐹) |
105 | 103, 104 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹⟶𝐹) |
106 | 105 | frnd 6521 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑋 ↾ 𝐹) ⊆ 𝐹) |
107 | | cores 6102 |
. . . . . . . 8
⊢ (ran
(𝑋 ↾ 𝐹) ⊆ 𝐹 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹))) |
108 | 106, 107 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹))) |
109 | | resco 6103 |
. . . . . . 7
⊢ ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑌 ∘ (𝑋 ↾ 𝐹)) |
110 | 108, 109 | syl6reqr 2875 |
. . . . . 6
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹))) |
111 | 20 | coeq1d 5732 |
. . . . . 6
⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹))) |
112 | | fcoi2 6553 |
. . . . . . 7
⊢ ((𝑋 ↾ 𝐹):𝐹⟶𝐹 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹)) |
113 | 105, 112 | syl 17 |
. . . . . 6
⊢ (𝜑 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹)) |
114 | 110, 111,
113 | 3eqtrd 2860 |
. . . . 5
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑋 ↾ 𝐹)) |
115 | 76, 114 | uneq12d 4140 |
. . . 4
⊢ (𝜑 → (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹))) |
116 | 71, 115 | syl5eq 2868 |
. . 3
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹))) |
117 | | f1oco 6637 |
. . . . 5
⊢ ((𝑌:𝐴–1-1-onto→𝐴 ∧ 𝑋:𝐴–1-1-onto→𝐴) → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴) |
118 | 8, 63, 117 | syl2anc 586 |
. . . 4
⊢ (𝜑 → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴) |
119 | | f1ofn 6616 |
. . . 4
⊢ ((𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴 → (𝑌 ∘ 𝑋) Fn 𝐴) |
120 | | fnresdm 6466 |
. . . 4
⊢ ((𝑌 ∘ 𝑋) Fn 𝐴 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋)) |
121 | 118, 119,
120 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋)) |
122 | 70, 116, 121 | 3eqtr3d 2864 |
. 2
⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑌 ∘ 𝑋)) |
123 | 69, 122 | eqtr3d 2858 |
1
⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋)) |