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

Metamath Proof Explorer

Theorem oppcbas

Description: Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017) (Proof shortened by AV, 18-Oct-2024)

Ref Expression
Hypotheses oppcbas.1 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppcbas.2 ⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion oppcbas 𝐵 = ( Base ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppcbas.1 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppcbas.2 ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 baseid ⊢ Base = Slot ( Base ‘ ndx )
4 slotsbhcdif ⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )
5 4 simp1i ⊢ ( Base ‘ ndx ) ≠ ( Hom ‘ ndx )
6 3 5 setsnid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) )
7 4 simp2i ⊢ ( Base ‘ ndx ) ≠ ( comp ‘ ndx )
8 3 7 setsnid ⊢ ( Base ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) ) = ( Base ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
9 6 8 eqtri ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
10 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
11 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
12 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
13 10 11 12 1 oppcval ⊢ ( 𝐶 ∈ V → 𝑂 = ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
14 13 fveq2d ⊢ ( 𝐶 ∈ V → ( Base ‘ 𝑂 ) = ( Base ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) ) )
15 9 14 eqtr4id ⊢ ( 𝐶 ∈ V → ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 ) )
16 base0 ⊢ ∅ = ( Base ‘ ∅ )
17 16 eqcomi ⊢ ( Base ‘ ∅ ) = ∅
18 17 1 fveqprc ⊢ ( ¬ 𝐶 ∈ V → ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 ) )
19 15 18 pm2.61i ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
20 2 19 eqtri ⊢ 𝐵 = ( Base ‘ 𝑂 )