Metamath Proof Explorer

Theorem oppcbasOLD

Description: Obsolete version of oppcbas as of 18-Oct-2024. Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 oppcbas.1 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppcbas.2 ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 baseid ⊢ Base = Slot ( Base ‘ ndx )
4 1re ⊢ 1 ∈ ℝ
5 1nn ⊢ 1 ∈ ℕ
6 4nn0 ⊢ 4 ∈ ℕ0
7 1nn0 ⊢ 1 ∈ ℕ0
8 1lt10 ⊢ 1 < 1 0
9 5 6 7 8 declti ⊢ 1 < 1 4
10 4 9 ltneii ⊢ 1 ≠ 1 4
11 basendx ⊢ ( Base ‘ ndx ) = 1
12 homndx ⊢ ( Hom ‘ ndx ) = 1 4
13 11 12 neeq12i ⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ↔ 1 ≠ 1 4 )
14 10 13 mpbir ⊢ ( Base ‘ ndx ) ≠ ( Hom ‘ ndx )
15 3 14 setsnid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) )
16 5nn ⊢ 5 ∈ ℕ
17 4lt5 ⊢ 4 < 5
18 7 6 16 17 declt ⊢ 1 4 < 1 5
19 4nn ⊢ 4 ∈ ℕ
20 7 19 decnncl ⊢ 1 4 ∈ ℕ
21 20 nnrei ⊢ 1 4 ∈ ℝ
22 7 16 decnncl ⊢ 1 5 ∈ ℕ
23 22 nnrei ⊢ 1 5 ∈ ℝ
24 4 21 23 lttri ⊢ ( ( 1 < 1 4 ∧ 1 4 < 1 5 ) → 1 < 1 5 )
25 9 18 24 mp2an ⊢ 1 < 1 5
26 4 25 ltneii ⊢ 1 ≠ 1 5
27 ccondx ⊢ ( comp ‘ ndx ) = 1 5
28 11 27 neeq12i ⊢ ( ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ↔ 1 ≠ 1 5 )
29 26 28 mpbir ⊢ ( Base ‘ ndx ) ≠ ( comp ‘ ndx )
30 3 29 setsnid ⊢ ( Base ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) ) = ( Base ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
31 15 30 eqtri ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
32 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
33 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
34 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
35 32 33 34 1 oppcval ⊢ ( 𝐶 ∈ V → 𝑂 = ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
36 35 fveq2d ⊢ ( 𝐶 ∈ V → ( Base ‘ 𝑂 ) = ( Base ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) ) )
37 31 36 eqtr4id ⊢ ( 𝐶 ∈ V → ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 ) )
38 base0 ⊢ ∅ = ( Base ‘ ∅ )
39 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( Base ‘ 𝐶 ) = ∅ )
40 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( oppCat ‘ 𝐶 ) = ∅ )
41 1 40 eqtrid ⊢ ( ¬ 𝐶 ∈ V → 𝑂 = ∅ )
42 41 fveq2d ⊢ ( ¬ 𝐶 ∈ V → ( Base ‘ 𝑂 ) = ( Base ‘ ∅ ) )
43 38 39 42 3eqtr4a ⊢ ( ¬ 𝐶 ∈ V → ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 ) )
44 37 43 pm2.61i ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
45 2 44 eqtri ⊢ 𝐵 = ( Base ‘ 𝑂 )