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

Metamath Proof Explorer

Theorem 2ndfval

Description: Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses 1stfval.t ⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
1stfval.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
1stfval.h ⊢ 𝐻 = ( Hom ‘ 𝑇 )
1stfval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
1stfval.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
2ndfval.p ⊢ 𝑄 = ( 𝐶 2ndF 𝐷 )
Assertion 2ndfval ( 𝜑 → 𝑄 = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )

Proof

Step Hyp Ref Expression
1 1stfval.t ⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2 1stfval.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
3 1stfval.h ⊢ 𝐻 = ( Hom ‘ 𝑇 )
4 1stfval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 1stfval.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
6 2ndfval.p ⊢ 𝑄 = ( 𝐶 2ndF 𝐷 )
7 fvex ⊢ ( Base ‘ 𝑐 ) ∈ V
8 fvex ⊢ ( Base ‘ 𝑑 ) ∈ V
9 7 8 xpex ⊢ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∈ V
10 9 a1i ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∈ V )
11 simpl ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 )
12 11 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
13 simpr ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
14 13 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑑 ) = ( Base ‘ 𝐷 ) )
15 12 14 xpeq12d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
16 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
17 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18 1 16 17 xpcbas ⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑇 )
19 18 2 eqtr4i ⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = 𝐵
20 15 19 eqtrdi ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) = 𝐵 )
21 simpr ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
22 21 reseq2d ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 2nd ↾ 𝑏 ) = ( 2nd ↾ 𝐵 ) )
23 simpll ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑐 = 𝐶 )
24 simplr ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑑 = 𝐷 )
25 23 24 oveq12d ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑐 ×c 𝑑 ) = ( 𝐶 ×c 𝐷 ) )
26 25 1 eqtr4di ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑐 ×c 𝑑 ) = 𝑇 )
27 26 fveq2d ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) = ( Hom ‘ 𝑇 ) )
28 27 3 eqtr4di ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) = 𝐻 )
29 28 oveqd ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
30 29 reseq2d ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) = ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) )
31 21 21 30 mpoeq123dv ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) )
32 22 31 opeq12d ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) ) ⟩ = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
33 10 20 32 csbied2 ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ⦋ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) / 𝑏 ⦌ ⟨ ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) ) ⟩ = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
34 df-2ndf ⊢ 2ndF = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ⦋ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) / 𝑏 ⦌ ⟨ ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) ) ⟩ )
35 opex ⊢ ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ ∈ V
36 33 34 35 ovmpoa ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 2ndF 𝐷 ) = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
37 4 5 36 syl2anc ⊢ ( 𝜑 → ( 𝐶 2ndF 𝐷 ) = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
38 6 37 eqtrid ⊢ ( 𝜑 → 𝑄 = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )