Step |
Hyp |
Ref |
Expression |
1 |
|
isepi.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
2 |
|
isepi.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
3 |
|
isepi.o |
⊢ · = ( comp ‘ 𝐶 ) |
4 |
|
isepi.e |
⊢ 𝐸 = ( Epi ‘ 𝐶 ) |
5 |
|
isepi.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
6 |
|
isepi.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
7 |
|
isepi.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
8 |
|
eqid |
⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 ) |
9 |
8 1
|
oppcbas |
⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) ) |
10 |
|
eqid |
⊢ ( Hom ‘ ( oppCat ‘ 𝐶 ) ) = ( Hom ‘ ( oppCat ‘ 𝐶 ) ) |
11 |
|
eqid |
⊢ ( comp ‘ ( oppCat ‘ 𝐶 ) ) = ( comp ‘ ( oppCat ‘ 𝐶 ) ) |
12 |
|
eqid |
⊢ ( Mono ‘ ( oppCat ‘ 𝐶 ) ) = ( Mono ‘ ( oppCat ‘ 𝐶 ) ) |
13 |
8
|
oppccat |
⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat ) |
14 |
5 13
|
syl |
⊢ ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat ) |
15 |
9 10 11 12 14 7 6
|
ismon |
⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ↔ ( 𝐹 ∈ ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( 〈 𝑧 , 𝑌 〉 ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) ) ) ) |
16 |
8 5 12 4
|
oppcmon |
⊢ ( 𝜑 → ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐸 𝑌 ) ) |
17 |
16
|
eleq2d |
⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ↔ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) ) |
18 |
2 8
|
oppchom |
⊢ ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐻 𝑌 ) |
19 |
18
|
a1i |
⊢ ( 𝜑 → ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐻 𝑌 ) ) |
20 |
19
|
eleq2d |
⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ↔ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ) |
21 |
2 8
|
oppchom |
⊢ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) = ( 𝑌 𝐻 𝑧 ) |
22 |
21
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) = ( 𝑌 𝐻 𝑧 ) ) |
23 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 ) |
24 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 ) |
25 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 ) |
26 |
1 3 8 23 24 25
|
oppcco |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ( 〈 𝑧 , 𝑌 〉 ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) = ( 𝑔 ( 〈 𝑋 , 𝑌 〉 · 𝑧 ) 𝐹 ) ) |
27 |
22 26
|
mpteq12dv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( 〈 𝑧 , 𝑌 〉 ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( 〈 𝑋 , 𝑌 〉 · 𝑧 ) 𝐹 ) ) ) |
28 |
27
|
cnveqd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ◡ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( 〈 𝑧 , 𝑌 〉 ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) = ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( 〈 𝑋 , 𝑌 〉 · 𝑧 ) 𝐹 ) ) ) |
29 |
28
|
funeqd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( Fun ◡ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( 〈 𝑧 , 𝑌 〉 ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) ↔ Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( 〈 𝑋 , 𝑌 〉 · 𝑧 ) 𝐹 ) ) ) ) |
30 |
29
|
ralbidva |
⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( 〈 𝑧 , 𝑌 〉 ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) ↔ ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( 〈 𝑋 , 𝑌 〉 · 𝑧 ) 𝐹 ) ) ) ) |
31 |
20 30
|
anbi12d |
⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( 〈 𝑧 , 𝑌 〉 ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( 〈 𝑋 , 𝑌 〉 · 𝑧 ) 𝐹 ) ) ) ) ) |
32 |
15 17 31
|
3bitr3d |
⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( 〈 𝑋 , 𝑌 〉 · 𝑧 ) 𝐹 ) ) ) ) ) |