Metamath Proof Explorer

Theorem symgcom

Description: Two permutations X and Y commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023)

Ref Expression
Hypotheses symgcom.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
symgcom.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
symgcom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
symgcom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
symgcom.1 ⊢ ( 𝜑 → ( 𝑋 ↾ 𝐸 ) = ( I ↾ 𝐸 ) )
symgcom.2 ⊢ ( 𝜑 → ( 𝑌 ↾ 𝐹 ) = ( I ↾ 𝐹 ) )
symgcom.3 ⊢ ( 𝜑 → ( 𝐸 ∩ 𝐹 ) = ∅ )
symgcom.4 ⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) = 𝐴 )
Assertion symgcom ( 𝜑 → ( 𝑋 ∘ 𝑌 ) = ( 𝑌 ∘ 𝑋 ) )

Proof

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