Step | Hyp | Ref
| Expression |
1 | | simplr 769 |
. . . . . 6
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) ∧ 𝑦 ∈ 𝐴) → (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) |
2 | 1 | fveq1d 6719 |
. . . . 5
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) ∧ 𝑦 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑦) = ((𝐻 ∘ 𝐹)‘𝑦)) |
3 | | simpl1 1193 |
. . . . . . 7
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → 𝐹:𝐴–onto→𝐵) |
4 | | fof 6633 |
. . . . . . 7
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → 𝐹:𝐴⟶𝐵) |
6 | | fvco3 6810 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑦 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝐺‘(𝐹‘𝑦))) |
7 | 5, 6 | sylan 583 |
. . . . 5
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) ∧ 𝑦 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝐺‘(𝐹‘𝑦))) |
8 | | fvco3 6810 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑦 ∈ 𝐴) → ((𝐻 ∘ 𝐹)‘𝑦) = (𝐻‘(𝐹‘𝑦))) |
9 | 5, 8 | sylan 583 |
. . . . 5
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) ∧ 𝑦 ∈ 𝐴) → ((𝐻 ∘ 𝐹)‘𝑦) = (𝐻‘(𝐹‘𝑦))) |
10 | 2, 7, 9 | 3eqtr3d 2785 |
. . . 4
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) ∧ 𝑦 ∈ 𝐴) → (𝐺‘(𝐹‘𝑦)) = (𝐻‘(𝐹‘𝑦))) |
11 | 10 | ralrimiva 3105 |
. . 3
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → ∀𝑦 ∈ 𝐴 (𝐺‘(𝐹‘𝑦)) = (𝐻‘(𝐹‘𝑦))) |
12 | | fveq2 6717 |
. . . . . 6
⊢ ((𝐹‘𝑦) = 𝑥 → (𝐺‘(𝐹‘𝑦)) = (𝐺‘𝑥)) |
13 | | fveq2 6717 |
. . . . . 6
⊢ ((𝐹‘𝑦) = 𝑥 → (𝐻‘(𝐹‘𝑦)) = (𝐻‘𝑥)) |
14 | 12, 13 | eqeq12d 2753 |
. . . . 5
⊢ ((𝐹‘𝑦) = 𝑥 → ((𝐺‘(𝐹‘𝑦)) = (𝐻‘(𝐹‘𝑦)) ↔ (𝐺‘𝑥) = (𝐻‘𝑥))) |
15 | 14 | cbvfo 7099 |
. . . 4
⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑦 ∈ 𝐴 (𝐺‘(𝐹‘𝑦)) = (𝐻‘(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = (𝐻‘𝑥))) |
16 | 3, 15 | syl 17 |
. . 3
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → (∀𝑦 ∈ 𝐴 (𝐺‘(𝐹‘𝑦)) = (𝐻‘(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = (𝐻‘𝑥))) |
17 | 11, 16 | mpbid 235 |
. 2
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = (𝐻‘𝑥)) |
18 | | eqfnfv 6852 |
. . . 4
⊢ ((𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) → (𝐺 = 𝐻 ↔ ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = (𝐻‘𝑥))) |
19 | 18 | 3adant1 1132 |
. . 3
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) → (𝐺 = 𝐻 ↔ ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = (𝐻‘𝑥))) |
20 | 19 | adantr 484 |
. 2
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → (𝐺 = 𝐻 ↔ ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = (𝐻‘𝑥))) |
21 | 17, 20 | mpbird 260 |
1
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → 𝐺 = 𝐻) |