Theorem oppcbas

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

	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		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	syl5eq	⊢ ( ¬ 𝐶 ∈ 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 ‘ 𝑂 )