| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | caofcan.2 | . . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝑇) | 
| 2 | 1 | ffnd 6736 | . . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| 3 |  | caofcan.3 | . . . . . . 7
⊢ (𝜑 → 𝐺:𝐴⟶𝑆) | 
| 4 | 3 | ffnd 6736 | . . . . . 6
⊢ (𝜑 → 𝐺 Fn 𝐴) | 
| 5 |  | caofcan.1 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 6 |  | inidm 4226 | . . . . . 6
⊢ (𝐴 ∩ 𝐴) = 𝐴 | 
| 7 |  | eqidd 2737 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘𝑤) = (𝐹‘𝑤)) | 
| 8 |  | eqidd 2737 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) = (𝐺‘𝑤)) | 
| 9 | 2, 4, 5, 5, 6, 7, 8 | ofval 7709 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝐹 ∘f 𝑅𝐺)‘𝑤) = ((𝐹‘𝑤)𝑅(𝐺‘𝑤))) | 
| 10 |  | caofcan.4 | . . . . . . 7
⊢ (𝜑 → 𝐻:𝐴⟶𝑆) | 
| 11 | 10 | ffnd 6736 | . . . . . 6
⊢ (𝜑 → 𝐻 Fn 𝐴) | 
| 12 |  | eqidd 2737 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐻‘𝑤) = (𝐻‘𝑤)) | 
| 13 | 2, 11, 5, 5, 6, 7, 12 | ofval 7709 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝐹 ∘f 𝑅𝐻)‘𝑤) = ((𝐹‘𝑤)𝑅(𝐻‘𝑤))) | 
| 14 | 9, 13 | eqeq12d 2752 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (((𝐹 ∘f 𝑅𝐺)‘𝑤) = ((𝐹 ∘f 𝑅𝐻)‘𝑤) ↔ ((𝐹‘𝑤)𝑅(𝐺‘𝑤)) = ((𝐹‘𝑤)𝑅(𝐻‘𝑤)))) | 
| 15 |  | simpl 482 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝜑) | 
| 16 | 1 | ffvelcdmda 7103 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘𝑤) ∈ 𝑇) | 
| 17 | 3 | ffvelcdmda 7103 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) ∈ 𝑆) | 
| 18 | 10 | ffvelcdmda 7103 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐻‘𝑤) ∈ 𝑆) | 
| 19 |  | caofcan.5 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦) = (𝑥𝑅𝑧) ↔ 𝑦 = 𝑧)) | 
| 20 | 19 | caovcang 7635 | . . . . 5
⊢ ((𝜑 ∧ ((𝐹‘𝑤) ∈ 𝑇 ∧ (𝐺‘𝑤) ∈ 𝑆 ∧ (𝐻‘𝑤) ∈ 𝑆)) → (((𝐹‘𝑤)𝑅(𝐺‘𝑤)) = ((𝐹‘𝑤)𝑅(𝐻‘𝑤)) ↔ (𝐺‘𝑤) = (𝐻‘𝑤))) | 
| 21 | 15, 16, 17, 18, 20 | syl13anc 1373 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (((𝐹‘𝑤)𝑅(𝐺‘𝑤)) = ((𝐹‘𝑤)𝑅(𝐻‘𝑤)) ↔ (𝐺‘𝑤) = (𝐻‘𝑤))) | 
| 22 | 14, 21 | bitrd 279 | . . 3
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (((𝐹 ∘f 𝑅𝐺)‘𝑤) = ((𝐹 ∘f 𝑅𝐻)‘𝑤) ↔ (𝐺‘𝑤) = (𝐻‘𝑤))) | 
| 23 | 22 | ralbidva 3175 | . 2
⊢ (𝜑 → (∀𝑤 ∈ 𝐴 ((𝐹 ∘f 𝑅𝐺)‘𝑤) = ((𝐹 ∘f 𝑅𝐻)‘𝑤) ↔ ∀𝑤 ∈ 𝐴 (𝐺‘𝑤) = (𝐻‘𝑤))) | 
| 24 | 2, 4, 5, 5, 6 | offn 7711 | . . 3
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) Fn 𝐴) | 
| 25 | 2, 11, 5, 5, 6 | offn 7711 | . . 3
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐻) Fn 𝐴) | 
| 26 |  | eqfnfv 7050 | . . 3
⊢ (((𝐹 ∘f 𝑅𝐺) Fn 𝐴 ∧ (𝐹 ∘f 𝑅𝐻) Fn 𝐴) → ((𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f 𝑅𝐻) ↔ ∀𝑤 ∈ 𝐴 ((𝐹 ∘f 𝑅𝐺)‘𝑤) = ((𝐹 ∘f 𝑅𝐻)‘𝑤))) | 
| 27 | 24, 25, 26 | syl2anc 584 | . 2
⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f 𝑅𝐻) ↔ ∀𝑤 ∈ 𝐴 ((𝐹 ∘f 𝑅𝐺)‘𝑤) = ((𝐹 ∘f 𝑅𝐻)‘𝑤))) | 
| 28 |  | eqfnfv 7050 | . . 3
⊢ ((𝐺 Fn 𝐴 ∧ 𝐻 Fn 𝐴) → (𝐺 = 𝐻 ↔ ∀𝑤 ∈ 𝐴 (𝐺‘𝑤) = (𝐻‘𝑤))) | 
| 29 | 4, 11, 28 | syl2anc 584 | . 2
⊢ (𝜑 → (𝐺 = 𝐻 ↔ ∀𝑤 ∈ 𝐴 (𝐺‘𝑤) = (𝐻‘𝑤))) | 
| 30 | 23, 27, 29 | 3bitr4d 311 | 1
⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f 𝑅𝐻) ↔ 𝐺 = 𝐻)) |