Theorem oppchomfval

Description: Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	oppchom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	oppchom.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
Assertion	oppchomfval	⊢ tpos 𝐻 = ( Hom ‘ 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		oppchom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
2		oppchom.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
3		homid	⊢ Hom = Slot ( Hom ‘ ndx )
4		1nn0	⊢ 1 ∈ ℕ0
5		4nn	⊢ 4 ∈ ℕ
6	4 5	decnncl	⊢ ; 1 4 ∈ ℕ
7	6	nnrei	⊢ ; 1 4 ∈ ℝ
8		4nn0	⊢ 4 ∈ ℕ0
9		5nn	⊢ 5 ∈ ℕ
10		4lt5	⊢ 4 < 5
11	4 8 9 10	declt	⊢ ; 1 4 < ; 1 5
12	7 11	ltneii	⊢ ; 1 4 ≠ ; 1 5
13		homndx	⊢ ( Hom ‘ ndx ) = ; 1 4
14		ccondx	⊢ ( comp ‘ ndx ) = ; 1 5
15	13 14	neeq12i	⊢ ( ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) ↔ ; 1 4 ≠ ; 1 5 )
16	12 15	mpbir	⊢ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx )
17	3 16	setsnid	⊢ ( Hom ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) ) = ( Hom ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
18	1	fvexi	⊢ 𝐻 ∈ V
19	18	tposex	⊢ tpos 𝐻 ∈ V
20	3	setsid	⊢ ( ( 𝐶 ∈ V ∧ tpos 𝐻 ∈ V ) → tpos 𝐻 = ( Hom ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) ) )
21	19 20	mpan2	⊢ ( 𝐶 ∈ V → tpos 𝐻 = ( Hom ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) ) )
22		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
23		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
24	22 1 23 2	oppcval	⊢ ( 𝐶 ∈ V → 𝑂 = ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
25	24	fveq2d	⊢ ( 𝐶 ∈ V → ( Hom ‘ 𝑂 ) = ( Hom ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) ) )
26	17 21 25	3eqtr4a	⊢ ( 𝐶 ∈ V → tpos 𝐻 = ( Hom ‘ 𝑂 ) )
27		tpos0	⊢ tpos ∅ = ∅
28		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( Hom ‘ 𝐶 ) = ∅ )
29	1 28	syl5eq	⊢ ( ¬ 𝐶 ∈ V → 𝐻 = ∅ )
30	29	tposeqd	⊢ ( ¬ 𝐶 ∈ V → tpos 𝐻 = tpos ∅ )
31		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( oppCat ‘ 𝐶 ) = ∅ )
32	2 31	syl5eq	⊢ ( ¬ 𝐶 ∈ V → 𝑂 = ∅ )
33	32	fveq2d	⊢ ( ¬ 𝐶 ∈ V → ( Hom ‘ 𝑂 ) = ( Hom ‘ ∅ ) )
34		df-hom	⊢ Hom = Slot ; 1 4
35	34	str0	⊢ ∅ = ( Hom ‘ ∅ )
36	33 35	eqtr4di	⊢ ( ¬ 𝐶 ∈ V → ( Hom ‘ 𝑂 ) = ∅ )
37	27 30 36	3eqtr4a	⊢ ( ¬ 𝐶 ∈ V → tpos 𝐻 = ( Hom ‘ 𝑂 ) )
38	26 37	pm2.61i	⊢ tpos 𝐻 = ( Hom ‘ 𝑂 )