Step |
Hyp |
Ref |
Expression |
1 |
|
caofref.1 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
2 |
|
caofref.2 |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 ) |
3 |
|
caofcom.3 |
⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 ) |
4 |
|
caofcom.4 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝑅 𝑦 ) = ( 𝑦 𝑅 𝑥 ) ) |
5 |
2
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ) |
6 |
3
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) |
7 |
5 6
|
jca |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) ) |
8 |
4
|
caovcomg |
⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) |
9 |
7 8
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) |
10 |
9
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) ) |
11 |
2
|
feqmptd |
⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) ) |
12 |
3
|
feqmptd |
⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) ) |
13 |
1 5 6 11 12
|
offval2 |
⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) ) |
14 |
1 6 5 12 11
|
offval2 |
⊢ ( 𝜑 → ( 𝐺 ∘f 𝑅 𝐹 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) ) |
15 |
10 13 14
|
3eqtr4d |
⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝐺 ∘f 𝑅 𝐹 ) ) |