Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
2 | | eqid 2610 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
3 | | eqid 2610 |
. . . . . 6
⊢
(comp‘𝐶) =
(comp‘𝐶) |
4 | | setcmon.h |
. . . . . 6
⊢ 𝑀 = (Mono‘𝐶) |
5 | | setcmon.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
6 | | setcmon.c |
. . . . . . . 8
⊢ 𝐶 = (SetCat‘𝑈) |
7 | 6 | setccat 16558 |
. . . . . . 7
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
8 | 5, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ Cat) |
9 | | setcmon.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
10 | 6, 5 | setcbas 16551 |
. . . . . . 7
⊢ (𝜑 → 𝑈 = (Base‘𝐶)) |
11 | 9, 10 | eleqtrd 2690 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) |
12 | | setcmon.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
13 | 12, 10 | eleqtrd 2690 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) |
14 | 1, 2, 3, 4, 8, 11,
13 | monhom 16218 |
. . . . 5
⊢ (𝜑 → (𝑋𝑀𝑌) ⊆ (𝑋(Hom ‘𝐶)𝑌)) |
15 | 14 | sselda 3568 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
16 | 6, 5, 2, 9, 12 | elsetchom 16554 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ↔ 𝐹:𝑋⟶𝑌)) |
17 | 16 | biimpa 500 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) → 𝐹:𝑋⟶𝑌) |
18 | 15, 17 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) → 𝐹:𝑋⟶𝑌) |
19 | | simprr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
20 | 19 | sneqd 4137 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → {(𝐹‘𝑥)} = {(𝐹‘𝑦)}) |
21 | 20 | xpeq2d 5063 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝑋 × {(𝐹‘𝑥)}) = (𝑋 × {(𝐹‘𝑦)})) |
22 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝐹:𝑋⟶𝑌) |
23 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶𝑌 → 𝐹 Fn 𝑋) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝐹 Fn 𝑋) |
25 | | simprll 798 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑥 ∈ 𝑋) |
26 | | fcoconst 6307 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐹 ∘ (𝑋 × {𝑥})) = (𝑋 × {(𝐹‘𝑥)})) |
27 | 24, 25, 26 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐹 ∘ (𝑋 × {𝑥})) = (𝑋 × {(𝐹‘𝑥)})) |
28 | | simprlr 799 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑦 ∈ 𝑋) |
29 | | fcoconst 6307 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹 ∘ (𝑋 × {𝑦})) = (𝑋 × {(𝐹‘𝑦)})) |
30 | 24, 28, 29 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐹 ∘ (𝑋 × {𝑦})) = (𝑋 × {(𝐹‘𝑦)})) |
31 | 21, 27, 30 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐹 ∘ (𝑋 × {𝑥})) = (𝐹 ∘ (𝑋 × {𝑦}))) |
32 | 5 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑈 ∈ 𝑉) |
33 | 9 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑋 ∈ 𝑈) |
34 | 12 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑌 ∈ 𝑈) |
35 | | fconst6g 6007 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 → (𝑋 × {𝑥}):𝑋⟶𝑋) |
36 | 25, 35 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝑋 × {𝑥}):𝑋⟶𝑋) |
37 | 6, 32, 3, 33, 33, 34, 36, 22 | setcco 16556 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(𝑋 × {𝑥})) = (𝐹 ∘ (𝑋 × {𝑥}))) |
38 | | fconst6g 6007 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑋 → (𝑋 × {𝑦}):𝑋⟶𝑋) |
39 | 28, 38 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝑋 × {𝑦}):𝑋⟶𝑋) |
40 | 6, 32, 3, 33, 33, 34, 39, 22 | setcco 16556 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(𝑋 × {𝑦})) = (𝐹 ∘ (𝑋 × {𝑦}))) |
41 | 31, 37, 40 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(𝑋 × {𝑥})) = (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(𝑋 × {𝑦}))) |
42 | 8 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝐶 ∈ Cat) |
43 | 11 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑋 ∈ (Base‘𝐶)) |
44 | 13 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑌 ∈ (Base‘𝐶)) |
45 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝐹 ∈ (𝑋𝑀𝑌)) |
46 | 6, 32, 2, 33, 33 | elsetchom 16554 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑋 × {𝑥}) ∈ (𝑋(Hom ‘𝐶)𝑋) ↔ (𝑋 × {𝑥}):𝑋⟶𝑋)) |
47 | 36, 46 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝑋 × {𝑥}) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
48 | 6, 32, 2, 33, 33 | elsetchom 16554 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑋 × {𝑦}) ∈ (𝑋(Hom ‘𝐶)𝑋) ↔ (𝑋 × {𝑦}):𝑋⟶𝑋)) |
49 | 39, 48 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝑋 × {𝑦}) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
50 | 1, 2, 3, 4, 42, 43, 44, 43, 45, 47, 49 | moni 16219 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(𝑋 × {𝑥})) = (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(𝑋 × {𝑦})) ↔ (𝑋 × {𝑥}) = (𝑋 × {𝑦}))) |
51 | 41, 50 | mpbid 221 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝑋 × {𝑥}) = (𝑋 × {𝑦})) |
52 | 51 | fveq1d 6105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑋 × {𝑥})‘𝑥) = ((𝑋 × {𝑦})‘𝑥)) |
53 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
54 | 53 | fvconst2 6374 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 → ((𝑋 × {𝑥})‘𝑥) = 𝑥) |
55 | 25, 54 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑋 × {𝑥})‘𝑥) = 𝑥) |
56 | | vex 3176 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
57 | 56 | fvconst2 6374 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 → ((𝑋 × {𝑦})‘𝑥) = 𝑦) |
58 | 25, 57 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑋 × {𝑦})‘𝑥) = 𝑦) |
59 | 52, 55, 58 | 3eqtr3d 2652 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → 𝑥 = 𝑦) |
60 | 59 | expr 641 |
. . . 4
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
61 | 60 | ralrimivva 2954 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
62 | | dff13 6416 |
. . 3
⊢ (𝐹:𝑋–1-1→𝑌 ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
63 | 18, 61, 62 | sylanbrc 695 |
. 2
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝑀𝑌)) → 𝐹:𝑋–1-1→𝑌) |
64 | | f1f 6014 |
. . . 4
⊢ (𝐹:𝑋–1-1→𝑌 → 𝐹:𝑋⟶𝑌) |
65 | 16 | biimpar 501 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
66 | 64, 65 | sylan2 490 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
67 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) → 𝑈 = (Base‘𝐶)) |
68 | 67 | eleq2d 2673 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) → (𝑧 ∈ 𝑈 ↔ 𝑧 ∈ (Base‘𝐶))) |
69 | 5 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → 𝑈 ∈ 𝑉) |
70 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → 𝑧 ∈ 𝑈) |
71 | 9 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → 𝑋 ∈ 𝑈) |
72 | 12 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → 𝑌 ∈ 𝑈) |
73 | | simprrl 800 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) |
74 | 6, 69, 2, 70, 71 | elsetchom 16554 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↔ 𝑔:𝑧⟶𝑋)) |
75 | 73, 74 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → 𝑔:𝑧⟶𝑋) |
76 | 64 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → 𝐹:𝑋⟶𝑌) |
77 | 6, 69, 3, 70, 71, 72, 75, 76 | setcco 16556 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹 ∘ 𝑔)) |
78 | | simprrr 801 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)) |
79 | 6, 69, 2, 70, 71 | elsetchom 16554 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → (ℎ ∈ (𝑧(Hom ‘𝐶)𝑋) ↔ ℎ:𝑧⟶𝑋)) |
80 | 78, 79 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → ℎ:𝑧⟶𝑋) |
81 | 6, 69, 3, 70, 71, 72, 80, 76 | setcco 16556 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) = (𝐹 ∘ ℎ)) |
82 | 77, 81 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → ((𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) ↔ (𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ))) |
83 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → 𝐹:𝑋–1-1→𝑌) |
84 | | cocan1 6446 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑋–1-1→𝑌 ∧ 𝑔:𝑧⟶𝑋 ∧ ℎ:𝑧⟶𝑋) → ((𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ) ↔ 𝑔 = ℎ)) |
85 | 83, 75, 80, 84 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → ((𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ) ↔ 𝑔 = ℎ)) |
86 | 85 | biimpd 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → ((𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ) → 𝑔 = ℎ)) |
87 | 82, 86 | sylbid 229 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)))) → ((𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)) |
88 | 87 | anassrs 678 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑧 ∈ 𝑈) ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑋))) → ((𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)) |
89 | 88 | ralrimivva 2954 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑧 ∈ 𝑈) → ∀𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)((𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)) |
90 | 89 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) → (𝑧 ∈ 𝑈 → ∀𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)((𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ))) |
91 | 68, 90 | sylbird 249 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) → (𝑧 ∈ (Base‘𝐶) → ∀𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)((𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ))) |
92 | 91 | ralrimiv 2948 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) → ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)((𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)) |
93 | 1, 2, 3, 4, 8, 11,
13 | ismon2 16217 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)((𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)))) |
94 | 93 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑋)((𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉(comp‘𝐶)𝑌)ℎ) → 𝑔 = ℎ)))) |
95 | 66, 92, 94 | mpbir2and 959 |
. 2
⊢ ((𝜑 ∧ 𝐹:𝑋–1-1→𝑌) → 𝐹 ∈ (𝑋𝑀𝑌)) |
96 | 63, 95 | impbida 873 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ 𝐹:𝑋–1-1→𝑌)) |