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	syl5eq	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )