Step |
Hyp |
Ref |
Expression |
1 |
|
ringcbasALTV.c |
⊢ 𝐶 = ( RingCatALTV ‘ 𝑈 ) |
2 |
|
ringcbasALTV.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
3 |
|
ringcbasALTV.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑉 ) |
4 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑈 ∩ Ring ) = ( 𝑈 ∩ Ring ) ) |
5 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑈 ∩ Ring ) , 𝑦 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑥 RingHom 𝑦 ) ) = ( 𝑥 ∈ ( 𝑈 ∩ Ring ) , 𝑦 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑥 RingHom 𝑦 ) ) ) |
6 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) , 𝑧 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) = ( 𝑣 ∈ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) , 𝑧 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) |
7 |
1 3 4 5 6
|
ringcvalALTV |
⊢ ( 𝜑 → 𝐶 = { 〈 ( Base ‘ ndx ) , ( 𝑈 ∩ Ring ) 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ ( 𝑈 ∩ Ring ) , 𝑦 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑥 RingHom 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) , 𝑧 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } ) |
8 |
|
catstr |
⊢ { 〈 ( Base ‘ ndx ) , ( 𝑈 ∩ Ring ) 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ ( 𝑈 ∩ Ring ) , 𝑦 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑥 RingHom 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) , 𝑧 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } Struct 〈 1 , ; 1 5 〉 |
9 |
|
baseid |
⊢ Base = Slot ( Base ‘ ndx ) |
10 |
|
snsstp1 |
⊢ { 〈 ( Base ‘ ndx ) , ( 𝑈 ∩ Ring ) 〉 } ⊆ { 〈 ( Base ‘ ndx ) , ( 𝑈 ∩ Ring ) 〉 , 〈 ( Hom ‘ ndx ) , ( 𝑥 ∈ ( 𝑈 ∩ Ring ) , 𝑦 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑥 RingHom 𝑦 ) ) 〉 , 〈 ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) , 𝑧 ∈ ( 𝑈 ∩ Ring ) ↦ ( 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑔 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑓 ∘ 𝑔 ) ) ) 〉 } |
11 |
|
inex1g |
⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Ring ) ∈ V ) |
12 |
3 11
|
syl |
⊢ ( 𝜑 → ( 𝑈 ∩ Ring ) ∈ V ) |
13 |
7 8 9 10 12 2
|
strfv3 |
⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) ) |