Proof of Theorem symgcom
Step | Hyp | Ref
| Expression |
1 | | symgcom.4 |
. . . 4
⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴) |
2 | 1 | reseq2d 5851 |
. . 3
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑋 ∘ 𝑌) ↾ 𝐴)) |
3 | | resundi 5865 |
. . . 4
⊢ ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹)) |
4 | | resco 6114 |
. . . . . . 7
⊢ ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑋 ∘ (𝑌 ↾ 𝐸)) |
5 | | symgcom.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
6 | | symgcom.g |
. . . . . . . . . . . . . . 15
⊢ 𝐺 = (SymGrp‘𝐴) |
7 | | symgcom.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝐺) |
8 | 6, 7 | symgbasf1o 18767 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∈ 𝐵 → 𝑌:𝐴–1-1-onto→𝐴) |
9 | 5, 8 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌:𝐴–1-1-onto→𝐴) |
10 | | f1ocnv 6673 |
. . . . . . . . . . . . 13
⊢ (𝑌:𝐴–1-1-onto→𝐴 → ◡𝑌:𝐴–1-1-onto→𝐴) |
11 | | f1ofun 6663 |
. . . . . . . . . . . . 13
⊢ (◡𝑌:𝐴–1-1-onto→𝐴 → Fun ◡𝑌) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun ◡𝑌) |
13 | | f1ofn 6662 |
. . . . . . . . . . . . . 14
⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌 Fn 𝐴) |
14 | | fnresdm 6496 |
. . . . . . . . . . . . . 14
⊢ (𝑌 Fn 𝐴 → (𝑌 ↾ 𝐴) = 𝑌) |
15 | 9, 13, 14 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 ↾ 𝐴) = 𝑌) |
16 | | f1ofo 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌:𝐴–onto→𝐴) |
17 | 9, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌:𝐴–onto→𝐴) |
18 | | foeq1 6629 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ↾ 𝐴) = 𝑌 → ((𝑌 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑌:𝐴–onto→𝐴)) |
19 | 18 | biimpar 481 |
. . . . . . . . . . . . 13
⊢ (((𝑌 ↾ 𝐴) = 𝑌 ∧ 𝑌:𝐴–onto→𝐴) → (𝑌 ↾ 𝐴):𝐴–onto→𝐴) |
20 | 15, 17, 19 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ↾ 𝐴):𝐴–onto→𝐴) |
21 | | symgcom.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹)) |
22 | | f1oi 6698 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ 𝐹):𝐹–1-1-onto→𝐹 |
23 | | f1ofo 6668 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹–onto→𝐹) |
24 | 22, 23 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( I ↾ 𝐹):𝐹–onto→𝐹) |
25 | | foeq1 6629 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) → ((𝑌 ↾ 𝐹):𝐹–onto→𝐹 ↔ ( I ↾ 𝐹):𝐹–onto→𝐹)) |
26 | 25 | biimpar 481 |
. . . . . . . . . . . . 13
⊢ (((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) ∧ ( I ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ 𝐹):𝐹–onto→𝐹) |
27 | 21, 24, 26 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ↾ 𝐹):𝐹–onto→𝐹) |
28 | | resdif 6681 |
. . . . . . . . . . . 12
⊢ ((Fun
◡𝑌 ∧ (𝑌 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑌 ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹)) |
29 | 12, 20, 27, 28 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹)) |
30 | | ssun2 4087 |
. . . . . . . . . . . . . . 15
⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹) |
31 | 30, 1 | sseqtrid 3953 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ⊆ 𝐴) |
32 | | incom 4115 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∩ 𝐹) = (𝐹 ∩ 𝐸) |
33 | | symgcom.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅) |
34 | 32, 33 | eqtr3id 2792 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∩ 𝐸) = ∅) |
35 | | uncom 4067 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∪ 𝐹) = (𝐹 ∪ 𝐸) |
36 | 35, 1 | eqtr3id 2792 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∪ 𝐸) = 𝐴) |
37 | | uneqdifeq 4404 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) → ((𝐹 ∪ 𝐸) = 𝐴 ↔ (𝐴 ∖ 𝐹) = 𝐸)) |
38 | 37 | biimpa 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) ∧ (𝐹 ∪ 𝐸) = 𝐴) → (𝐴 ∖ 𝐹) = 𝐸) |
39 | 31, 34, 36, 38 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∖ 𝐹) = 𝐸) |
40 | 39 | reseq2d 5851 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)) = (𝑌 ↾ 𝐸)) |
41 | 40, 39, 39 | f1oeq123d 6655 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹) ↔ (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸)) |
42 | 29, 41 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸) |
43 | | f1of 6661 |
. . . . . . . . . 10
⊢ ((𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸 → (𝑌 ↾ 𝐸):𝐸⟶𝐸) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸⟶𝐸) |
45 | 44 | frnd 6553 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑌 ↾ 𝐸) ⊆ 𝐸) |
46 | | cores 6113 |
. . . . . . . 8
⊢ (ran
(𝑌 ↾ 𝐸) ⊆ 𝐸 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸))) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸))) |
48 | 4, 47 | eqtr4id 2797 |
. . . . . 6
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸))) |
49 | | symgcom.1 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸)) |
50 | 49 | coeq1d 5730 |
. . . . . 6
⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸))) |
51 | | fcoi2 6594 |
. . . . . . 7
⊢ ((𝑌 ↾ 𝐸):𝐸⟶𝐸 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸)) |
52 | 44, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸)) |
53 | 48, 50, 52 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑌 ↾ 𝐸)) |
54 | | resco 6114 |
. . . . . 6
⊢ ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ∘ (𝑌 ↾ 𝐹)) |
55 | 21 | coeq2d 5731 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐹))) |
56 | | coires1 6128 |
. . . . . . 7
⊢ (𝑋 ∘ ( I ↾ 𝐹)) = (𝑋 ↾ 𝐹) |
57 | 55, 56 | eqtrdi 2794 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ↾ 𝐹)) |
58 | 54, 57 | syl5eq 2790 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ↾ 𝐹)) |
59 | 53, 58 | uneq12d 4078 |
. . . 4
⊢ (𝜑 → (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹))) |
60 | 3, 59 | syl5eq 2790 |
. . 3
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹))) |
61 | | symgcom.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
62 | 6, 7 | symgbasf1o 18767 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → 𝑋:𝐴–1-1-onto→𝐴) |
63 | 61, 62 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋:𝐴–1-1-onto→𝐴) |
64 | | f1oco 6683 |
. . . . 5
⊢ ((𝑋:𝐴–1-1-onto→𝐴 ∧ 𝑌:𝐴–1-1-onto→𝐴) → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴) |
65 | 63, 9, 64 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴) |
66 | | f1ofn 6662 |
. . . 4
⊢ ((𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴 → (𝑋 ∘ 𝑌) Fn 𝐴) |
67 | | fnresdm 6496 |
. . . 4
⊢ ((𝑋 ∘ 𝑌) Fn 𝐴 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌)) |
68 | 65, 66, 67 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌)) |
69 | 2, 60, 68 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑋 ∘ 𝑌)) |
70 | 1 | reseq2d 5851 |
. . 3
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ∘ 𝑋) ↾ 𝐴)) |
71 | | resundi 5865 |
. . . 4
⊢ ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹)) |
72 | | resco 6114 |
. . . . . 6
⊢ ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ∘ (𝑋 ↾ 𝐸)) |
73 | 49 | coeq2d 5731 |
. . . . . . 7
⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ∘ ( I ↾ 𝐸))) |
74 | | coires1 6128 |
. . . . . . 7
⊢ (𝑌 ∘ ( I ↾ 𝐸)) = (𝑌 ↾ 𝐸) |
75 | 73, 74 | eqtrdi 2794 |
. . . . . 6
⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ↾ 𝐸)) |
76 | 72, 75 | syl5eq 2790 |
. . . . 5
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ↾ 𝐸)) |
77 | | resco 6114 |
. . . . . . 7
⊢ ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑌 ∘ (𝑋 ↾ 𝐹)) |
78 | | f1ocnv 6673 |
. . . . . . . . . . . . 13
⊢ (𝑋:𝐴–1-1-onto→𝐴 → ◡𝑋:𝐴–1-1-onto→𝐴) |
79 | | f1ofun 6663 |
. . . . . . . . . . . . 13
⊢ (◡𝑋:𝐴–1-1-onto→𝐴 → Fun ◡𝑋) |
80 | 63, 78, 79 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun ◡𝑋) |
81 | | f1ofn 6662 |
. . . . . . . . . . . . . 14
⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋 Fn 𝐴) |
82 | | fnresdm 6496 |
. . . . . . . . . . . . . 14
⊢ (𝑋 Fn 𝐴 → (𝑋 ↾ 𝐴) = 𝑋) |
83 | 63, 81, 82 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ↾ 𝐴) = 𝑋) |
84 | | f1ofo 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋:𝐴–onto→𝐴) |
85 | 63, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋:𝐴–onto→𝐴) |
86 | | foeq1 6629 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ↾ 𝐴) = 𝑋 → ((𝑋 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑋:𝐴–onto→𝐴)) |
87 | 86 | biimpar 481 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ↾ 𝐴) = 𝑋 ∧ 𝑋:𝐴–onto→𝐴) → (𝑋 ↾ 𝐴):𝐴–onto→𝐴) |
88 | 83, 85, 87 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ↾ 𝐴):𝐴–onto→𝐴) |
89 | | f1oi 6698 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ 𝐸):𝐸–1-1-onto→𝐸 |
90 | | f1ofo 6668 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐸):𝐸–1-1-onto→𝐸 → ( I ↾ 𝐸):𝐸–onto→𝐸) |
91 | 89, 90 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( I ↾ 𝐸):𝐸–onto→𝐸) |
92 | | foeq1 6629 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) → ((𝑋 ↾ 𝐸):𝐸–onto→𝐸 ↔ ( I ↾ 𝐸):𝐸–onto→𝐸)) |
93 | 92 | biimpar 481 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) ∧ ( I ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ 𝐸):𝐸–onto→𝐸) |
94 | 49, 91, 93 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ↾ 𝐸):𝐸–onto→𝐸) |
95 | | resdif 6681 |
. . . . . . . . . . . 12
⊢ ((Fun
◡𝑋 ∧ (𝑋 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑋 ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸)) |
96 | 80, 88, 94, 95 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸)) |
97 | | ssun1 4086 |
. . . . . . . . . . . . . . 15
⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹) |
98 | 97, 1 | sseqtrid 3953 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ⊆ 𝐴) |
99 | | uneqdifeq 4404 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) → ((𝐸 ∪ 𝐹) = 𝐴 ↔ (𝐴 ∖ 𝐸) = 𝐹)) |
100 | 99 | biimpa 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) ∧ (𝐸 ∪ 𝐹) = 𝐴) → (𝐴 ∖ 𝐸) = 𝐹) |
101 | 98, 33, 1, 100 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∖ 𝐸) = 𝐹) |
102 | 101 | reseq2d 5851 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)) = (𝑋 ↾ 𝐹)) |
103 | 102, 101,
101 | f1oeq123d 6655 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸) ↔ (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹)) |
104 | 96, 103 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹) |
105 | | f1of 6661 |
. . . . . . . . . 10
⊢ ((𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹 → (𝑋 ↾ 𝐹):𝐹⟶𝐹) |
106 | 104, 105 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹⟶𝐹) |
107 | 106 | frnd 6553 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑋 ↾ 𝐹) ⊆ 𝐹) |
108 | | cores 6113 |
. . . . . . . 8
⊢ (ran
(𝑋 ↾ 𝐹) ⊆ 𝐹 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹))) |
109 | 107, 108 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹))) |
110 | 77, 109 | eqtr4id 2797 |
. . . . . 6
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹))) |
111 | 21 | coeq1d 5730 |
. . . . . 6
⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹))) |
112 | | fcoi2 6594 |
. . . . . . 7
⊢ ((𝑋 ↾ 𝐹):𝐹⟶𝐹 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹)) |
113 | 106, 112 | syl 17 |
. . . . . 6
⊢ (𝜑 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹)) |
114 | 110, 111,
113 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑋 ↾ 𝐹)) |
115 | 76, 114 | uneq12d 4078 |
. . . 4
⊢ (𝜑 → (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹))) |
116 | 71, 115 | syl5eq 2790 |
. . 3
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹))) |
117 | | f1oco 6683 |
. . . . 5
⊢ ((𝑌:𝐴–1-1-onto→𝐴 ∧ 𝑋:𝐴–1-1-onto→𝐴) → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴) |
118 | 9, 63, 117 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴) |
119 | | f1ofn 6662 |
. . . 4
⊢ ((𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴 → (𝑌 ∘ 𝑋) Fn 𝐴) |
120 | | fnresdm 6496 |
. . . 4
⊢ ((𝑌 ∘ 𝑋) Fn 𝐴 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋)) |
121 | 118, 119,
120 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋)) |
122 | 70, 116, 121 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑌 ∘ 𝑋)) |
123 | 69, 122 | eqtr3d 2779 |
1
⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋)) |