Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
2 | | eqid 2610 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
3 | | eqid 2610 |
. . . . . 6
⊢
(comp‘𝐶) =
(comp‘𝐶) |
4 | | setcepi.h |
. . . . . 6
⊢ 𝐸 = (Epi‘𝐶) |
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 | epihom 16225 |
. . . . 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 | | frn 5966 |
. . . . 5
⊢ (𝐹:𝑋⟶𝑌 → ran 𝐹 ⊆ 𝑌) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹 ⊆ 𝑌) |
21 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑋⟶𝑌 → 𝐹 Fn 𝑋) |
22 | 18, 21 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 Fn 𝑋) |
23 | | fnfvelrn 6264 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ran 𝐹) |
24 | 22, 23 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ran 𝐹) |
25 | 24 | iftrued 4044 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥 ∈ 𝑋) → if((𝐹‘𝑥) ∈ ran 𝐹, 1𝑜, ∅) =
1𝑜) |
26 | 25 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑥 ∈ 𝑋 ↦ if((𝐹‘𝑥) ∈ ran 𝐹, 1𝑜, ∅)) = (𝑥 ∈ 𝑋 ↦
1𝑜)) |
27 | 18 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ 𝑌) |
28 | 18 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
29 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜,
∅))) |
30 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝐹‘𝑥) → (𝑎 ∈ ran 𝐹 ↔ (𝐹‘𝑥) ∈ ran 𝐹)) |
31 | 30 | ifbid 4058 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝐹‘𝑥) → if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) =
if((𝐹‘𝑥) ∈ ran 𝐹, 1𝑜,
∅)) |
32 | 27, 28, 29, 31 | fmptco 6303 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∘
𝐹) = (𝑥 ∈ 𝑋 ↦ if((𝐹‘𝑥) ∈ ran 𝐹, 1𝑜,
∅))) |
33 | | fconstmpt 5085 |
. . . . . . . . . . . . 13
⊢ (𝑌 ×
{1𝑜}) = (𝑎 ∈ 𝑌 ↦
1𝑜) |
34 | 33 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1𝑜}) = (𝑎 ∈ 𝑌 ↦
1𝑜)) |
35 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝐹‘𝑥) → 1𝑜 =
1𝑜) |
36 | 27, 28, 34, 35 | fmptco 6303 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1𝑜}) ∘
𝐹) = (𝑥 ∈ 𝑋 ↦
1𝑜)) |
37 | 26, 32, 36 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∘
𝐹) = ((𝑌 × {1𝑜}) ∘
𝐹)) |
38 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑈 ∈ 𝑉) |
39 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋 ∈ 𝑈) |
40 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ∈ 𝑈) |
41 | | setcepi.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2𝑜
∈ 𝑈) |
42 | 41 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 2𝑜 ∈ 𝑈) |
43 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜,
∅)) |
44 | | 1onn 7606 |
. . . . . . . . . . . . . . . . . 18
⊢
1𝑜 ∈ ω |
45 | 44 | elexi 3186 |
. . . . . . . . . . . . . . . . 17
⊢
1𝑜 ∈ V |
46 | 45 | prid2 4242 |
. . . . . . . . . . . . . . . 16
⊢
1𝑜 ∈ {∅,
1𝑜} |
47 | | df2o3 7460 |
. . . . . . . . . . . . . . . 16
⊢
2𝑜 = {∅,
1𝑜} |
48 | 46, 47 | eleqtrri 2687 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ∈ 2𝑜 |
49 | | 0ex 4718 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ V |
50 | 49 | prid1 4241 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ {∅, 1𝑜} |
51 | 50, 47 | eleqtrri 2687 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ 2𝑜 |
52 | 48, 51 | keepel 4105 |
. . . . . . . . . . . . . 14
⊢ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈
2𝑜 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑌 → if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈
2𝑜) |
54 | 43, 53 | fmpti 6291 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)):𝑌⟶2𝑜 |
55 | 54 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)):𝑌⟶2𝑜) |
56 | 6, 38, 3, 39, 40, 42, 18, 55 | setcco 16556 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜,
∅))(〈𝑋, 𝑌〉(comp‘𝐶)2𝑜)𝐹) = ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∘
𝐹)) |
57 | | fconst6g 6007 |
. . . . . . . . . . . 12
⊢
(1𝑜 ∈ 2𝑜 → (𝑌 ×
{1𝑜}):𝑌⟶2𝑜) |
58 | 48, 57 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1𝑜}):𝑌⟶2𝑜) |
59 | 6, 38, 3, 39, 40, 42, 18, 58 | setcco 16556 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 ×
{1𝑜})(〈𝑋, 𝑌〉(comp‘𝐶)2𝑜)𝐹) = ((𝑌 × {1𝑜}) ∘
𝐹)) |
60 | 37, 56, 59 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜,
∅))(〈𝑋, 𝑌〉(comp‘𝐶)2𝑜)𝐹) = ((𝑌 ×
{1𝑜})(〈𝑋, 𝑌〉(comp‘𝐶)2𝑜)𝐹)) |
61 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐶 ∈ Cat) |
62 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋 ∈ (Base‘𝐶)) |
63 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ∈ (Base‘𝐶)) |
64 | 41, 10 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ (𝜑 → 2𝑜
∈ (Base‘𝐶)) |
65 | 64 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 2𝑜 ∈
(Base‘𝐶)) |
66 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 ∈ (𝑋𝐸𝑌)) |
67 | 6, 38, 2, 40, 42 | elsetchom 16554 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∈
(𝑌(Hom ‘𝐶)2𝑜) ↔
(𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)):𝑌⟶2𝑜)) |
68 | 55, 67 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∈
(𝑌(Hom ‘𝐶)2𝑜)) |
69 | 6, 38, 2, 40, 42 | elsetchom 16554 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1𝑜}) ∈
(𝑌(Hom ‘𝐶)2𝑜) ↔
(𝑌 ×
{1𝑜}):𝑌⟶2𝑜)) |
70 | 58, 69 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1𝑜}) ∈
(𝑌(Hom ‘𝐶)2𝑜)) |
71 | 1, 2, 3, 4, 61, 62, 63, 65, 66, 68, 70 | epii 16226 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜,
∅))(〈𝑋, 𝑌〉(comp‘𝐶)2𝑜)𝐹) = ((𝑌 ×
{1𝑜})(〈𝑋, 𝑌〉(comp‘𝐶)2𝑜)𝐹) ↔ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑌 ×
{1𝑜}))) |
72 | 60, 71 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑌 ×
{1𝑜})) |
73 | 72, 33 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦
1𝑜)) |
74 | 52 | rgenw 2908 |
. . . . . . . 8
⊢
∀𝑎 ∈
𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈
2𝑜 |
75 | | mpteqb 6207 |
. . . . . . . 8
⊢
(∀𝑎 ∈
𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈
2𝑜 → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦ 1𝑜) ↔
∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) =
1𝑜)) |
76 | 74, 75 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦ 1𝑜) ↔
∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) =
1𝑜) |
77 | 73, 76 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) =
1𝑜) |
78 | | 1n0 7462 |
. . . . . . . . . 10
⊢
1𝑜 ≠ ∅ |
79 | 78 | nesymi 2839 |
. . . . . . . . 9
⊢ ¬
∅ = 1𝑜 |
80 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
𝑎 ∈ ran 𝐹 → if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) =
∅) |
81 | 80 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (¬
𝑎 ∈ ran 𝐹 → (if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) =
1𝑜 ↔ ∅ = 1𝑜)) |
82 | 79, 81 | mtbiri 316 |
. . . . . . . 8
⊢ (¬
𝑎 ∈ ran 𝐹 → ¬ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) =
1𝑜) |
83 | 82 | con4i 112 |
. . . . . . 7
⊢ (if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) =
1𝑜 → 𝑎 ∈ ran 𝐹) |
84 | 83 | ralimi 2936 |
. . . . . 6
⊢
(∀𝑎 ∈
𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) =
1𝑜 → ∀𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹) |
85 | 77, 84 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹) |
86 | | dfss3 3558 |
. . . . 5
⊢ (𝑌 ⊆ ran 𝐹 ↔ ∀𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹) |
87 | 85, 86 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ⊆ ran 𝐹) |
88 | 20, 87 | eqssd 3585 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹 = 𝑌) |
89 | | dffo2 6032 |
. . 3
⊢ (𝐹:𝑋–onto→𝑌 ↔ (𝐹:𝑋⟶𝑌 ∧ ran 𝐹 = 𝑌)) |
90 | 18, 88, 89 | sylanbrc 695 |
. 2
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹:𝑋–onto→𝑌) |
91 | | fof 6028 |
. . . . 5
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
92 | 91 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝐹:𝑋⟶𝑌) |
93 | 16 | biimpar 501 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
94 | 92, 93 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
95 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝑈 = (Base‘𝐶)) |
96 | 95 | eleq2d 2673 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ 𝑈 ↔ 𝑧 ∈ (Base‘𝐶))) |
97 | 5 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑈 ∈ 𝑉) |
98 | 9 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑋 ∈ 𝑈) |
99 | 12 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑌 ∈ 𝑈) |
100 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ 𝑈) |
101 | 92 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋⟶𝑌) |
102 | | simprrl 800 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)) |
103 | 6, 97, 2, 99, 100 | elsetchom 16554 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ 𝑔:𝑌⟶𝑧)) |
104 | 102, 103 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔:𝑌⟶𝑧) |
105 | 6, 97, 3, 98, 99, 100, 101, 104 | setcco 16556 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (𝑔 ∘ 𝐹)) |
106 | | simprrr 801 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)) |
107 | 6, 97, 2, 99, 100 | elsetchom 16554 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (ℎ ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ ℎ:𝑌⟶𝑧)) |
108 | 106, 107 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ℎ:𝑌⟶𝑧) |
109 | 6, 97, 3, 98, 99, 100, 101, 108 | setcco 16556 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ ∘ 𝐹)) |
110 | 105, 109 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) ↔ (𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹))) |
111 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋–onto→𝑌) |
112 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝑔:𝑌⟶𝑧 → 𝑔 Fn 𝑌) |
113 | 104, 112 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 Fn 𝑌) |
114 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (ℎ:𝑌⟶𝑧 → ℎ Fn 𝑌) |
115 | 108, 114 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ℎ Fn 𝑌) |
116 | | cocan2 6447 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑔 Fn 𝑌 ∧ ℎ Fn 𝑌) → ((𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹) ↔ 𝑔 = ℎ)) |
117 | 111, 113,
115, 116 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹) ↔ 𝑔 = ℎ)) |
118 | 117 | biimpd 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹) → 𝑔 = ℎ)) |
119 | 110, 118 | sylbid 229 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)) |
120 | 119 | anassrs 678 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝑧 ∈ 𝑈) ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)) |
121 | 120 | ralrimivva 2954 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝑧 ∈ 𝑈) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)) |
122 | 121 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ 𝑈 → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))) |
123 | 96, 122 | sylbird 249 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ (Base‘𝐶) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))) |
124 | 123 | ralrimiv 2948 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)) |
125 | 1, 2, 3, 4, 8, 11,
13 | isepi2 16224 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)))) |
126 | 125 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)))) |
127 | 94, 124, 126 | mpbir2and 959 |
. 2
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝐹 ∈ (𝑋𝐸𝑌)) |
128 | 90, 127 | impbida 873 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋–onto→𝑌)) |