Step | Hyp | Ref
| Expression |
1 | | caofcan.2 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝑇) |
2 | | ffn 6045 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝑇 → 𝐹 Fn 𝐴) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝐴) |
4 | | caofcan.3 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝐴⟶𝑆) |
5 | | ffn 6045 |
. . . . . . 7
⊢ (𝐺:𝐴⟶𝑆 → 𝐺 Fn 𝐴) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 Fn 𝐴) |
7 | | caofcan.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
8 | | inidm 3822 |
. . . . . 6
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
9 | | eqidd 2623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘𝑤) = (𝐹‘𝑤)) |
10 | | eqidd 2623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) = (𝐺‘𝑤)) |
11 | 3, 6, 7, 7, 8, 9, 10 | ofval 6906 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝐹 ∘𝑓 𝑅𝐺)‘𝑤) = ((𝐹‘𝑤)𝑅(𝐺‘𝑤))) |
12 | | caofcan.4 |
. . . . . . 7
⊢ (𝜑 → 𝐻:𝐴⟶𝑆) |
13 | | ffn 6045 |
. . . . . . 7
⊢ (𝐻:𝐴⟶𝑆 → 𝐻 Fn 𝐴) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻 Fn 𝐴) |
15 | | eqidd 2623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐻‘𝑤) = (𝐻‘𝑤)) |
16 | 3, 14, 7, 7, 8, 9, 15 | ofval 6906 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝐹 ∘𝑓 𝑅𝐻)‘𝑤) = ((𝐹‘𝑤)𝑅(𝐻‘𝑤))) |
17 | 11, 16 | eqeq12d 2637 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (((𝐹 ∘𝑓 𝑅𝐺)‘𝑤) = ((𝐹 ∘𝑓 𝑅𝐻)‘𝑤) ↔ ((𝐹‘𝑤)𝑅(𝐺‘𝑤)) = ((𝐹‘𝑤)𝑅(𝐻‘𝑤)))) |
18 | | simpl 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝜑) |
19 | 1 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘𝑤) ∈ 𝑇) |
20 | 4 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) ∈ 𝑆) |
21 | 12 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐻‘𝑤) ∈ 𝑆) |
22 | | caofcan.5 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦) = (𝑥𝑅𝑧) ↔ 𝑦 = 𝑧)) |
23 | 22 | caovcang 6835 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐹‘𝑤) ∈ 𝑇 ∧ (𝐺‘𝑤) ∈ 𝑆 ∧ (𝐻‘𝑤) ∈ 𝑆)) → (((𝐹‘𝑤)𝑅(𝐺‘𝑤)) = ((𝐹‘𝑤)𝑅(𝐻‘𝑤)) ↔ (𝐺‘𝑤) = (𝐻‘𝑤))) |
24 | 18, 19, 20, 21, 23 | syl13anc 1328 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (((𝐹‘𝑤)𝑅(𝐺‘𝑤)) = ((𝐹‘𝑤)𝑅(𝐻‘𝑤)) ↔ (𝐺‘𝑤) = (𝐻‘𝑤))) |
25 | 17, 24 | bitrd 268 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (((𝐹 ∘𝑓 𝑅𝐺)‘𝑤) = ((𝐹 ∘𝑓 𝑅𝐻)‘𝑤) ↔ (𝐺‘𝑤) = (𝐻‘𝑤))) |
26 | 25 | ralbidva 2985 |
. 2
⊢ (𝜑 → (∀𝑤 ∈ 𝐴 ((𝐹 ∘𝑓 𝑅𝐺)‘𝑤) = ((𝐹 ∘𝑓 𝑅𝐻)‘𝑤) ↔ ∀𝑤 ∈ 𝐴 (𝐺‘𝑤) = (𝐻‘𝑤))) |
27 | 3, 6, 7, 7, 8 | offn 6908 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) Fn 𝐴) |
28 | 3, 14, 7, 7, 8 | offn 6908 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐻) Fn 𝐴) |
29 | | eqfnfv 6311 |
. . 3
⊢ (((𝐹 ∘𝑓
𝑅𝐺) Fn 𝐴 ∧ (𝐹 ∘𝑓 𝑅𝐻) Fn 𝐴) → ((𝐹 ∘𝑓 𝑅𝐺) = (𝐹 ∘𝑓 𝑅𝐻) ↔ ∀𝑤 ∈ 𝐴 ((𝐹 ∘𝑓 𝑅𝐺)‘𝑤) = ((𝐹 ∘𝑓 𝑅𝐻)‘𝑤))) |
30 | 27, 28, 29 | syl2anc 693 |
. 2
⊢ (𝜑 → ((𝐹 ∘𝑓 𝑅𝐺) = (𝐹 ∘𝑓 𝑅𝐻) ↔ ∀𝑤 ∈ 𝐴 ((𝐹 ∘𝑓 𝑅𝐺)‘𝑤) = ((𝐹 ∘𝑓 𝑅𝐻)‘𝑤))) |
31 | | eqfnfv 6311 |
. . 3
⊢ ((𝐺 Fn 𝐴 ∧ 𝐻 Fn 𝐴) → (𝐺 = 𝐻 ↔ ∀𝑤 ∈ 𝐴 (𝐺‘𝑤) = (𝐻‘𝑤))) |
32 | 6, 14, 31 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝐺 = 𝐻 ↔ ∀𝑤 ∈ 𝐴 (𝐺‘𝑤) = (𝐻‘𝑤))) |
33 | 26, 30, 32 | 3bitr4d 300 |
1
⊢ (𝜑 → ((𝐹 ∘𝑓 𝑅𝐺) = (𝐹 ∘𝑓 𝑅𝐻) ↔ 𝐺 = 𝐻)) |