Step |
Hyp |
Ref |
Expression |
1 |
|
yon11.y |
⊢ 𝑌 = ( Yon ‘ 𝐶 ) |
2 |
|
yon11.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
3 |
|
yon11.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
4 |
|
yon11.p |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
5 |
|
yon1cl.o |
⊢ 𝑂 = ( oppCat ‘ 𝐶 ) |
6 |
|
yon1cl.s |
⊢ 𝑆 = ( SetCat ‘ 𝑈 ) |
7 |
|
yon1cl.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑉 ) |
8 |
|
yon1cl.h |
⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 ) |
9 |
|
eqid |
⊢ ( 𝑂 FuncCat 𝑆 ) = ( 𝑂 FuncCat 𝑆 ) |
10 |
9
|
fucbas |
⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ ( 𝑂 FuncCat 𝑆 ) ) |
11 |
|
relfunc |
⊢ Rel ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) |
12 |
1 3 5 6 9 7 8
|
yoncl |
⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ) |
13 |
|
1st2ndbr |
⊢ ( ( Rel ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ∧ 𝑌 ∈ ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ) → ( 1st ‘ 𝑌 ) ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ( 2nd ‘ 𝑌 ) ) |
14 |
11 12 13
|
sylancr |
⊢ ( 𝜑 → ( 1st ‘ 𝑌 ) ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ( 2nd ‘ 𝑌 ) ) |
15 |
2 10 14
|
funcf1 |
⊢ ( 𝜑 → ( 1st ‘ 𝑌 ) : 𝐵 ⟶ ( 𝑂 Func 𝑆 ) ) |
16 |
15 4
|
ffvelrnd |
⊢ ( 𝜑 → ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) ) |