| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 2 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 4 | | setcepi.h |
. . . . . 6
⊢ 𝐸 = (Epi‘𝐶) |
| 5 | | setcmon.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
| 6 | | setcmon.c |
. . . . . . . 8
⊢ 𝐶 = (SetCat‘𝑈) |
| 7 | 6 | setccat 18130 |
. . . . . . 7
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
| 8 | 5, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 9 | | setcmon.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
| 10 | 6, 5 | setcbas 18123 |
. . . . . . 7
⊢ (𝜑 → 𝑈 = (Base‘𝐶)) |
| 11 | 9, 10 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) |
| 12 | | setcmon.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
| 13 | 12, 10 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) |
| 14 | 1, 2, 3, 4, 8, 11,
13 | epihom 17786 |
. . . . 5
⊢ (𝜑 → (𝑋𝐸𝑌) ⊆ (𝑋(Hom ‘𝐶)𝑌)) |
| 15 | 14 | sselda 3983 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
| 16 | 6, 5, 2, 9, 12 | elsetchom 18126 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ↔ 𝐹:𝑋⟶𝑌)) |
| 17 | 16 | biimpa 476 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) → 𝐹:𝑋⟶𝑌) |
| 18 | 15, 17 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹:𝑋⟶𝑌) |
| 19 | 18 | frnd 6744 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹 ⊆ 𝑌) |
| 20 | 18 | ffnd 6737 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 Fn 𝑋) |
| 21 | | fnfvelrn 7100 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ran 𝐹) |
| 22 | 20, 21 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ran 𝐹) |
| 23 | 22 | iftrued 4533 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥 ∈ 𝑋) → if((𝐹‘𝑥) ∈ ran 𝐹, 1o, ∅) =
1o) |
| 24 | 23 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑥 ∈ 𝑋 ↦ if((𝐹‘𝑥) ∈ ran 𝐹, 1o, ∅)) = (𝑥 ∈ 𝑋 ↦ 1o)) |
| 25 | 18 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ 𝑌) |
| 26 | 18 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
| 27 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅))) |
| 28 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝐹‘𝑥) → (𝑎 ∈ ran 𝐹 ↔ (𝐹‘𝑥) ∈ ran 𝐹)) |
| 29 | 28 | ifbid 4549 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝐹‘𝑥) → if(𝑎 ∈ ran 𝐹, 1o, ∅) = if((𝐹‘𝑥) ∈ ran 𝐹, 1o, ∅)) |
| 30 | 25, 26, 27, 29 | fmptco 7149 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∘ 𝐹) = (𝑥 ∈ 𝑋 ↦ if((𝐹‘𝑥) ∈ ran 𝐹, 1o, ∅))) |
| 31 | | fconstmpt 5747 |
. . . . . . . . . . . . 13
⊢ (𝑌 × {1o}) =
(𝑎 ∈ 𝑌 ↦ 1o) |
| 32 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1o}) = (𝑎 ∈ 𝑌 ↦ 1o)) |
| 33 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝐹‘𝑥) → 1o =
1o) |
| 34 | 25, 26, 32, 33 | fmptco 7149 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1o}) ∘ 𝐹) = (𝑥 ∈ 𝑋 ↦ 1o)) |
| 35 | 24, 30, 34 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∘ 𝐹) = ((𝑌 × {1o}) ∘ 𝐹)) |
| 36 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑈 ∈ 𝑉) |
| 37 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋 ∈ 𝑈) |
| 38 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ∈ 𝑈) |
| 39 | | setcepi.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2o ∈ 𝑈) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 2o ∈ 𝑈) |
| 41 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) |
| 42 | | 1oex 8516 |
. . . . . . . . . . . . . . . . 17
⊢
1o ∈ V |
| 43 | 42 | prid2 4763 |
. . . . . . . . . . . . . . . 16
⊢
1o ∈ {∅, 1o} |
| 44 | | df2o3 8514 |
. . . . . . . . . . . . . . . 16
⊢
2o = {∅, 1o} |
| 45 | 43, 44 | eleqtrri 2840 |
. . . . . . . . . . . . . . 15
⊢
1o ∈ 2o |
| 46 | | 0ex 5307 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ V |
| 47 | 46 | prid1 4762 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ {∅, 1o} |
| 48 | 47, 44 | eleqtrri 2840 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ 2o |
| 49 | 45, 48 | ifcli 4573 |
. . . . . . . . . . . . . 14
⊢ if(𝑎 ∈ ran 𝐹, 1o, ∅) ∈
2o |
| 50 | 49 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑌 → if(𝑎 ∈ ran 𝐹, 1o, ∅) ∈
2o) |
| 51 | 41, 50 | fmpti 7132 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)):𝑌⟶2o |
| 52 | 51 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)):𝑌⟶2o) |
| 53 | 6, 36, 3, 37, 38, 40, 18, 52 | setcco 18128 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅))(〈𝑋, 𝑌〉(comp‘𝐶)2o)𝐹) = ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∘ 𝐹)) |
| 54 | | fconst6g 6797 |
. . . . . . . . . . . 12
⊢
(1o ∈ 2o → (𝑌 × {1o}):𝑌⟶2o) |
| 55 | 45, 54 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1o}):𝑌⟶2o) |
| 56 | 6, 36, 3, 37, 38, 40, 18, 55 | setcco 18128 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1o})(〈𝑋, 𝑌〉(comp‘𝐶)2o)𝐹) = ((𝑌 × {1o}) ∘ 𝐹)) |
| 57 | 35, 53, 56 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅))(〈𝑋, 𝑌〉(comp‘𝐶)2o)𝐹) = ((𝑌 × {1o})(〈𝑋, 𝑌〉(comp‘𝐶)2o)𝐹)) |
| 58 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐶 ∈ Cat) |
| 59 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋 ∈ (Base‘𝐶)) |
| 60 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ∈ (Base‘𝐶)) |
| 61 | 39, 10 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ (𝜑 → 2o ∈
(Base‘𝐶)) |
| 62 | 61 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 2o ∈
(Base‘𝐶)) |
| 63 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 ∈ (𝑋𝐸𝑌)) |
| 64 | 6, 36, 2, 38, 40 | elsetchom 18126 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∈ (𝑌(Hom ‘𝐶)2o) ↔ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)):𝑌⟶2o)) |
| 65 | 52, 64 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∈ (𝑌(Hom ‘𝐶)2o)) |
| 66 | 6, 36, 2, 38, 40 | elsetchom 18126 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1o}) ∈ (𝑌(Hom ‘𝐶)2o) ↔ (𝑌 × {1o}):𝑌⟶2o)) |
| 67 | 55, 66 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1o}) ∈ (𝑌(Hom ‘𝐶)2o)) |
| 68 | 1, 2, 3, 4, 58, 59, 60, 62, 63, 65, 67 | epii 17787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅))(〈𝑋, 𝑌〉(comp‘𝐶)2o)𝐹) = ((𝑌 × {1o})(〈𝑋, 𝑌〉(comp‘𝐶)2o)𝐹) ↔ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑌 ×
{1o}))) |
| 69 | 57, 68 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑌 ×
{1o})) |
| 70 | 69, 31 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎 ∈ 𝑌 ↦ 1o)) |
| 71 | 49 | rgenw 3065 |
. . . . . . . 8
⊢
∀𝑎 ∈
𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) ∈
2o |
| 72 | | mpteqb 7035 |
. . . . . . . 8
⊢
(∀𝑎 ∈
𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) ∈
2o → ((𝑎
∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎 ∈ 𝑌 ↦ 1o) ↔ ∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) =
1o)) |
| 73 | 71, 72 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎 ∈ 𝑌 ↦ 1o) ↔ ∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) =
1o) |
| 74 | 70, 73 | sylib 218 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) =
1o) |
| 75 | | 1n0 8526 |
. . . . . . . . . 10
⊢
1o ≠ ∅ |
| 76 | 75 | nesymi 2998 |
. . . . . . . . 9
⊢ ¬
∅ = 1o |
| 77 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑎 ∈ ran 𝐹 → if(𝑎 ∈ ran 𝐹, 1o, ∅) =
∅) |
| 78 | 77 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (¬
𝑎 ∈ ran 𝐹 → (if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o
↔ ∅ = 1o)) |
| 79 | 76, 78 | mtbiri 327 |
. . . . . . . 8
⊢ (¬
𝑎 ∈ ran 𝐹 → ¬ if(𝑎 ∈ ran 𝐹, 1o, ∅) =
1o) |
| 80 | 79 | con4i 114 |
. . . . . . 7
⊢ (if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o
→ 𝑎 ∈ ran 𝐹) |
| 81 | 80 | ralimi 3083 |
. . . . . 6
⊢
(∀𝑎 ∈
𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o
→ ∀𝑎 ∈
𝑌 𝑎 ∈ ran 𝐹) |
| 82 | 74, 81 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹) |
| 83 | | dfss3 3972 |
. . . . 5
⊢ (𝑌 ⊆ ran 𝐹 ↔ ∀𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹) |
| 84 | 82, 83 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ⊆ ran 𝐹) |
| 85 | 19, 84 | eqssd 4001 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹 = 𝑌) |
| 86 | | dffo2 6824 |
. . 3
⊢ (𝐹:𝑋–onto→𝑌 ↔ (𝐹:𝑋⟶𝑌 ∧ ran 𝐹 = 𝑌)) |
| 87 | 18, 85, 86 | sylanbrc 583 |
. 2
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹:𝑋–onto→𝑌) |
| 88 | | fof 6820 |
. . . . 5
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
| 89 | 88 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝐹:𝑋⟶𝑌) |
| 90 | 16 | biimpar 477 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
| 91 | 89, 90 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
| 92 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝑈 = (Base‘𝐶)) |
| 93 | 92 | eleq2d 2827 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ 𝑈 ↔ 𝑧 ∈ (Base‘𝐶))) |
| 94 | 5 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑈 ∈ 𝑉) |
| 95 | 9 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑋 ∈ 𝑈) |
| 96 | 12 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑌 ∈ 𝑈) |
| 97 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ 𝑈) |
| 98 | 89 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋⟶𝑌) |
| 99 | | simprrl 781 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)) |
| 100 | 6, 94, 2, 96, 97 | elsetchom 18126 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ 𝑔:𝑌⟶𝑧)) |
| 101 | 99, 100 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔:𝑌⟶𝑧) |
| 102 | 6, 94, 3, 95, 96, 97, 98, 101 | setcco 18128 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (𝑔 ∘ 𝐹)) |
| 103 | | simprrr 782 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)) |
| 104 | 6, 94, 2, 96, 97 | elsetchom 18126 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (ℎ ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ ℎ:𝑌⟶𝑧)) |
| 105 | 103, 104 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ℎ:𝑌⟶𝑧) |
| 106 | 6, 94, 3, 95, 96, 97, 98, 105 | setcco 18128 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ ∘ 𝐹)) |
| 107 | 102, 106 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) ↔ (𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹))) |
| 108 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋–onto→𝑌) |
| 109 | 101 | ffnd 6737 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 Fn 𝑌) |
| 110 | 105 | ffnd 6737 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ℎ Fn 𝑌) |
| 111 | | cocan2 7312 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑔 Fn 𝑌 ∧ ℎ Fn 𝑌) → ((𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹) ↔ 𝑔 = ℎ)) |
| 112 | 108, 109,
110, 111 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹) ↔ 𝑔 = ℎ)) |
| 113 | 112 | biimpd 229 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹) → 𝑔 = ℎ)) |
| 114 | 107, 113 | sylbid 240 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)) |
| 115 | 114 | anassrs 467 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝑧 ∈ 𝑈) ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)) |
| 116 | 115 | ralrimivva 3202 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝑧 ∈ 𝑈) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)) |
| 117 | 116 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ 𝑈 → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))) |
| 118 | 93, 117 | sylbird 260 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ (Base‘𝐶) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))) |
| 119 | 118 | ralrimiv 3145 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)) |
| 120 | 1, 2, 3, 4, 8, 11,
13 | isepi2 17785 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)))) |
| 121 | 120 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)))) |
| 122 | 91, 119, 121 | mpbir2and 713 |
. 2
⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝐹 ∈ (𝑋𝐸𝑌)) |
| 123 | 87, 122 | impbida 801 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋–onto→𝑌)) |