Metamath Proof Explorer

Theorem estrcval

Description: Value of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020)

Ref Expression
Hypotheses estrcval.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
estrcval.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
estrcval.h ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
estrcval.o ⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
Assertion estrcval ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )

Proof

Step Hyp Ref Expression
1 estrcval.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 estrcval.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 estrcval.h ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
4 estrcval.o ⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
5 df-estrc ⊢ ExtStrCat = ( 𝑢 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → 𝑢 = 𝑈 )
7 6 opeq2d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ )
8 eqidd ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) = ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) )
9 6 6 8 mpoeq123dv ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → 𝐻 = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
11 9 10 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = 𝐻 )
12 11 opeq2d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
13 6 sqxpeqd ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑢 × 𝑢 ) = ( 𝑈 × 𝑈 ) )
14 eqidd ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
15 13 6 14 mpoeq123dv ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
16 4 adantr ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
17 15 16 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) = · )
18 17 opeq2d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , · ⟩ )
19 7 12 18 tpeq123d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → { ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
20 2 elexd ⊢ ( 𝜑 → 𝑈 ∈ V )
21 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V
22 21 a1i ⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V )
23 5 19 20 22 fvmptd2 ⊢ ( 𝜑 → ( ExtStrCat ‘ 𝑈 ) = { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
24 1 23 eqtrid ⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )