Metamath Proof Explorer


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