Step |
Hyp |
Ref |
Expression |
1 |
|
sectepi.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
2 |
|
sectepi.e |
⊢ 𝐸 = ( Epi ‘ 𝐶 ) |
3 |
|
sectepi.s |
⊢ 𝑆 = ( Sect ‘ 𝐶 ) |
4 |
|
sectepi.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
5 |
|
sectepi.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
6 |
|
sectepi.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
7 |
|
episect.n |
⊢ 𝑁 = ( Inv ‘ 𝐶 ) |
8 |
|
episect.1 |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) |
9 |
|
episect.2 |
⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ) |
10 |
|
eqid |
⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 ) |
11 |
|
eqid |
⊢ ( Inv ‘ ( oppCat ‘ 𝐶 ) ) = ( Inv ‘ ( oppCat ‘ 𝐶 ) ) |
12 |
1 10 4 6 5 7 11
|
oppcinv |
⊢ ( 𝜑 → ( 𝑌 ( Inv ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝑁 𝑌 ) ) |
13 |
10 1
|
oppcbas |
⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) ) |
14 |
|
eqid |
⊢ ( Mono ‘ ( oppCat ‘ 𝐶 ) ) = ( Mono ‘ ( oppCat ‘ 𝐶 ) ) |
15 |
|
eqid |
⊢ ( Sect ‘ ( oppCat ‘ 𝐶 ) ) = ( Sect ‘ ( oppCat ‘ 𝐶 ) ) |
16 |
10
|
oppccat |
⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat ) |
17 |
4 16
|
syl |
⊢ ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat ) |
18 |
10 4 14 2
|
oppcmon |
⊢ ( 𝜑 → ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐸 𝑌 ) ) |
19 |
8 18
|
eleqtrrd |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ) |
20 |
1 10 4 5 6 3 15
|
oppcsect |
⊢ ( 𝜑 → ( 𝐺 ( 𝑋 ( Sect ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) 𝐹 ↔ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ) ) |
21 |
9 20
|
mpbird |
⊢ ( 𝜑 → 𝐺 ( 𝑋 ( Sect ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) 𝐹 ) |
22 |
13 14 15 17 6 5 11 19 21
|
monsect |
⊢ ( 𝜑 → 𝐹 ( 𝑌 ( Inv ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝐺 ) |
23 |
12 22
|
breqdi |
⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ) |