This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem catcval

Description: Value of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catcval.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
catcval.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
catcval.b ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
catcval.h ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) )
catcval.o ⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) )
Assertion catcval ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )

Proof

Step Hyp Ref Expression
1 catcval.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 catcval.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 catcval.b ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
4 catcval.h ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) )
5 catcval.o ⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) )
6 df-catc ⊢ CatCat = ( 𝑢 ∈ V ↦ ⦋ ( 𝑢 ∩ Cat ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } )
7 vex ⊢ 𝑢 ∈ V
8 7 inex1 ⊢ ( 𝑢 ∩ Cat ) ∈ V
9 8 a1i ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑢 ∩ Cat ) ∈ V )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → 𝑢 = 𝑈 )
11 10 ineq1d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑢 ∩ Cat ) = ( 𝑈 ∩ Cat ) )
12 3 adantr ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → 𝐵 = ( 𝑈 ∩ Cat ) )
13 11 12 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑢 ∩ Cat ) = 𝐵 )
14 simpr ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
15 14 opeq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
16 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 Func 𝑦 ) = ( 𝑥 Func 𝑦 ) )
17 14 14 16 mpoeq123dv ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) )
18 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) )
19 17 18 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) = 𝐻 )
20 19 opeq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
21 14 sqxpeqd ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) )
22 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) = ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) )
23 21 14 22 mpoeq123dv ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) )
24 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → · = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) )
25 23 24 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) = · )
26 25 opeq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , · ⟩ )
27 15 20 26 tpeq123d ⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
28 9 13 27 csbied2 ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ⦋ ( 𝑢 ∩ Cat ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
29 2 elexd ⊢ ( 𝜑 → 𝑈 ∈ V )
30 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V
31 30 a1i ⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V )
32 6 28 29 31 fvmptd2 ⊢ ( 𝜑 → ( CatCat ‘ 𝑈 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
33 1 32 eqtrid ⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )