Step |
Hyp |
Ref |
Expression |
1 |
|
setcbas.c |
⊢ 𝐶 = ( SetCat ‘ 𝑈 ) |
2 |
|
setcbas.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑉 ) |
3 |
|
setchomfval.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
4 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) ) |
5 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ) |
6 |
1 2 4 5
|
setcval |
⊢ ( 𝜑 → 𝐶 = { 〈 ( Base ‘ ndx ) , 𝑈 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) 〉 } ) |
7 |
|
catstr |
⊢ { 〈 ( Base ‘ ndx ) , 𝑈 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) 〉 } Struct 〈 1 , ; 1 5 〉 |
8 |
|
homid |
⊢ Hom = Slot ( Hom ‘ ndx ) |
9 |
|
snsstp2 |
⊢ { 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) 〉 } ⊆ { 〈 ( Base ‘ ndx ) , 𝑈 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) 〉 } |
10 |
|
mpoexga |
⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) ∈ V ) |
11 |
2 2 10
|
syl2anc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) ∈ V ) |
12 |
6 7 8 9 11 3
|
strfv3 |
⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) ) |