Step |
Hyp |
Ref |
Expression |
1 |
|
rngcbasALTV.c |
⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 ) |
2 |
|
rngcbasALTV.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
3 |
|
rngcbasALTV.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑉 ) |
4 |
|
rngchomfvalALTV.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
5 |
1 2 3
|
rngcbasALTV |
⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) ) |
6 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) ) |
7 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RngHomo 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RngHomo ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RngHomo 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RngHomo ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) |
8 |
1 3 5 6 7
|
rngcvalALTV |
⊢ ( 𝜑 → 𝐶 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RngHomo 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RngHomo ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } ) |
9 |
8
|
fveq2d |
⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RngHomo 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RngHomo ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } ) ) |
10 |
4 9
|
syl5eq |
⊢ ( 𝜑 → 𝐻 = ( Hom ‘ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RngHomo 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RngHomo ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } ) ) |
11 |
2
|
fvexi |
⊢ 𝐵 ∈ V |
12 |
11 11
|
mpoex |
⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) ∈ V |
13 |
|
catstr |
⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RngHomo 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RngHomo ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } Struct 〈 1 , ; 1 5 〉 |
14 |
|
homid |
⊢ Hom = Slot ( Hom ‘ ndx ) |
15 |
|
snsstp2 |
⊢ { 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) 〉 } ⊆ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RngHomo 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RngHomo ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } |
16 |
13 14 15
|
strfv |
⊢ ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) ∈ V → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) = ( Hom ‘ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RngHomo 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RngHomo ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } ) ) |
17 |
12 16
|
mp1i |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) = ( Hom ‘ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RngHomo 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RngHomo ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } ) ) |
18 |
10 17
|
eqtr4d |
⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) ) |