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 eqid 
 |-  ( Base ` C ) = ( Base ` C )
4 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
5 eqid 
 |-  ( comp ` C ) = ( comp ` C )
6 3 4 5 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 ) ) ) >. ) )
7 6 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 ) ) ) >. ) ) )
8 baseid 
 |-  Base = Slot ( Base ` ndx )
9 1re 
 |-  1 e. RR
10 1nn 
 |-  1 e. NN
11 4nn0 
 |-  4 e. NN0
12 1nn0 
 |-  1 e. NN0
13 1lt10 
 |-  1 < ; 1 0
14 10 11 12 13 declti 
 |-  1 < ; 1 4
15 9 14 ltneii 
 |-  1 =/= ; 1 4
16 basendx 
 |-  ( Base ` ndx ) = 1
17 homndx 
 |-  ( Hom ` ndx ) = ; 1 4
18 16 17 neeq12i 
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) <-> 1 =/= ; 1 4 )
19 15 18 mpbir 
 |-  ( Base ` ndx ) =/= ( Hom ` ndx )
20 8 19 setsnid 
 |-  ( Base ` C ) = ( Base ` ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) )
21 5nn 
 |-  5 e. NN
22 4lt5 
 |-  4 < 5
23 12 11 21 22 declt 
 |-  ; 1 4 < ; 1 5
24 4nn 
 |-  4 e. NN
25 12 24 decnncl 
 |-  ; 1 4 e. NN
26 25 nnrei 
 |-  ; 1 4 e. RR
27 12 21 decnncl 
 |-  ; 1 5 e. NN
28 27 nnrei 
 |-  ; 1 5 e. RR
29 9 26 28 lttri 
 |-  ( ( 1 < ; 1 4 /\ ; 1 4 < ; 1 5 ) -> 1 < ; 1 5 )
30 14 23 29 mp2an 
 |-  1 < ; 1 5
31 9 30 ltneii 
 |-  1 =/= ; 1 5
32 ccondx 
 |-  ( comp ` ndx ) = ; 1 5
33 16 32 neeq12i 
 |-  ( ( Base ` ndx ) =/= ( comp ` ndx ) <-> 1 =/= ; 1 5 )
34 31 33 mpbir 
 |-  ( Base ` ndx ) =/= ( comp ` ndx )
35 8 34 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 ) ) ) >. ) )
36 20 35 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 ) ) ) >. ) )
37 7 36 syl6reqr 
 |-  ( 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 )