Metamath Proof Explorer

Theorem oppcbas

Description: Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses oppcbas.1 
|- O = ( oppCat ` C )
oppcbas.2 
|- B = ( Base ` C )
Assertion oppcbas 
|- B = ( Base ` O )

Proof

Step Hyp Ref Expression
1 oppcbas.1 
 |-  O = ( oppCat ` C )
2 oppcbas.2 
 |-  B = ( Base ` C )
3 baseid 
 |-  Base = Slot ( Base ` ndx )
4 1re 
 |-  1 e. RR
5 1nn 
 |-  1 e. NN
6 4nn0 
 |-  4 e. NN0
7 1nn0 
 |-  1 e. NN0
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 ` C ) = ( Base ` ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) )
16 5nn 
 |-  5 e. NN
17 4lt5 
 |-  4 < 5
18 7 6 16 17 declt 
 |-  ; 1 4 < ; 1 5
19 4nn 
 |-  4 e. NN
20 7 19 decnncl 
 |-  ; 1 4 e. NN
21 20 nnrei 
 |-  ; 1 4 e. RR
22 7 16 decnncl 
 |-  ; 1 5 e. NN
23 22 nnrei 
 |-  ; 1 5 e. RR
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 ` ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) ) = ( Base ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) )
31 15 30 eqtri 
 |-  ( Base ` C ) = ( Base ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) )
32 eqid 
 |-  ( Base ` C ) = ( Base ` C )
33 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
34 eqid 
 |-  ( comp ` C ) = ( comp ` C )
35 32 33 34 1 oppcval 
 |-  ( C e. _V -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) )
36 35 fveq2d 
 |-  ( C e. _V -> ( Base ` O ) = ( Base ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) ) )
37 31 36 eqtr4id 
 |-  ( C e. _V -> ( Base ` C ) = ( Base ` O ) )
38 base0 
 |-  (/) = ( Base ` (/) )
39 fvprc 
 |-  ( -. C e. _V -> ( Base ` C ) = (/) )
40 fvprc 
 |-  ( -. C e. _V -> ( oppCat ` C ) = (/) )
41 1 40 syl5eq 
 |-  ( -. C e. _V -> O = (/) )
42 41 fveq2d 
 |-  ( -. C e. _V -> ( Base ` O ) = ( Base ` (/) ) )
43 38 39 42 3eqtr4a 
 |-  ( -. C e. _V -> ( Base ` C ) = ( Base ` O ) )
44 37 43 pm2.61i 
 |-  ( Base ` C ) = ( Base ` O )
45 2 44 eqtri 
 |-  B = ( Base ` O )