Theorem setcval

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

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

Proof

Step	Hyp	Ref	Expression
1		setcval.c	⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2		setcval.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		setcval.h	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) )
4		setcval.o	⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
5		df-setc	⊢ SetCat = ( 𝑢 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → 𝑢 = 𝑈 )
7	6	opeq2d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ )
8		eqidd	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑦 ↑m 𝑥 ) = ( 𝑦 ↑m 𝑥 ) )
9	6 6 8	mpoeq123dv	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) )
10	3	adantr	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → 𝐻 = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑦 ↑m 𝑥 ) ) )
11	9 10	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) ) = 𝐻 )
12	11	opeq2d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) ) ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
13	6	sqxpeqd	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑢 × 𝑢 ) = ( 𝑈 × 𝑈 ) )
14		eqidd	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
15	13 6 14	mpoeq123dv	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
16	4	adantr	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
17	15 16	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) = · )
18	17	opeq2d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , · ⟩ )
19	7 12 18	tpeq123d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → { ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 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	⊢ ( 𝜑 → ( SetCat ‘ 𝑈 ) = { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
24	1 23	syl5eq	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )