Metamath Proof Explorer

Theorem catcoppccl

Description: The category of categories for a weak universe is closed under taking opposites. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses catcoppccl.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
catcoppccl.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
catcoppccl.o ⊢ 𝑂 = ( oppCat ‘ 𝑋 )
catcoppccl.1 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
catcoppccl.2 ⊢ ( 𝜑 → ω ∈ 𝑈 )
catcoppccl.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion catcoppccl ( 𝜑 → 𝑂 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 catcoppccl.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 catcoppccl.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 catcoppccl.o ⊢ 𝑂 = ( oppCat ‘ 𝑋 )
4 catcoppccl.1 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
5 catcoppccl.2 ⊢ ( 𝜑 → ω ∈ 𝑈 )
6 catcoppccl.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
8 eqid ⊢ ( Hom ‘ 𝑋 ) = ( Hom ‘ 𝑋 )
9 eqid ⊢ ( comp ‘ 𝑋 ) = ( comp ‘ 𝑋 )
10 7 8 9 3 oppcval ⊢ ( 𝑋 ∈ 𝐵 → 𝑂 = ( ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) ⟩ ) )
11 6 10 syl ⊢ ( 𝜑 → 𝑂 = ( ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) ⟩ ) )
12 1 2 4 catcbas ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
13 6 12 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Cat ) )
14 13 elin1d ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
15 df-hom ⊢ Hom = Slot 1 4
16 4 5 wunndx ⊢ ( 𝜑 → ndx ∈ 𝑈 )
17 15 4 16 wunstr ⊢ ( 𝜑 → ( Hom ‘ ndx ) ∈ 𝑈 )
18 15 4 14 wunstr ⊢ ( 𝜑 → ( Hom ‘ 𝑋 ) ∈ 𝑈 )
19 4 18 wuntpos ⊢ ( 𝜑 → tpos ( Hom ‘ 𝑋 ) ∈ 𝑈 )
20 4 17 19 wunop ⊢ ( 𝜑 → ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ∈ 𝑈 )
21 4 14 20 wunsets ⊢ ( 𝜑 → ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) ∈ 𝑈 )
22 df-cco ⊢ comp = Slot 1 5
23 22 4 16 wunstr ⊢ ( 𝜑 → ( comp ‘ ndx ) ∈ 𝑈 )
24 df-base ⊢ Base = Slot 1
25 24 4 14 wunstr ⊢ ( 𝜑 → ( Base ‘ 𝑋 ) ∈ 𝑈 )
26 4 25 25 wunxp ⊢ ( 𝜑 → ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ∈ 𝑈 )
27 4 26 25 wunxp ⊢ ( 𝜑 → ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) × ( Base ‘ 𝑋 ) ) ∈ 𝑈 )
28 22 4 14 wunstr ⊢ ( 𝜑 → ( comp ‘ 𝑋 ) ∈ 𝑈 )
29 4 28 wunrn ⊢ ( 𝜑 → ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
30 4 29 wununi ⊢ ( 𝜑 → ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
31 4 30 wundm ⊢ ( 𝜑 → dom ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
32 4 31 wuncnv ⊢ ( 𝜑 → ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
33 4 wun0 ⊢ ( 𝜑 → ∅ ∈ 𝑈 )
34 4 33 wunsn ⊢ ( 𝜑 → { ∅ } ∈ 𝑈 )
35 4 32 34 wunun ⊢ ( 𝜑 → ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) ∈ 𝑈 )
36 4 30 wunrn ⊢ ( 𝜑 → ran ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
37 4 35 36 wunxp ⊢ ( 𝜑 → ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ∈ 𝑈 )
38 4 37 wunpw ⊢ ( 𝜑 → 𝒫 ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ∈ 𝑈 )
39 tposssxp ⊢ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ( ( ◡ dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∪ { ∅ } ) × ran ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) )
40 ovssunirn ⊢ ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ∪ ran ( comp ‘ 𝑋 )
41 dmss ⊢ ( ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ∪ ran ( comp ‘ 𝑋 ) → dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ dom ∪ ran ( comp ‘ 𝑋 ) )
42 40 41 ax-mp ⊢ dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ dom ∪ ran ( comp ‘ 𝑋 )
43 cnvss ⊢ ( dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ dom ∪ ran ( comp ‘ 𝑋 ) → ◡ dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ◡ dom ∪ ran ( comp ‘ 𝑋 ) )
44 unss1 ⊢ ( ◡ dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ◡ dom ∪ ran ( comp ‘ 𝑋 ) → ( ◡ dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∪ { ∅ } ) ⊆ ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) )
45 42 43 44 mp2b ⊢ ( ◡ dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∪ { ∅ } ) ⊆ ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } )
46 40 rnssi ⊢ ran ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ran ∪ ran ( comp ‘ 𝑋 )
47 xpss12 ⊢ ( ( ( ◡ dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∪ { ∅ } ) ⊆ ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) ∧ ran ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ran ∪ ran ( comp ‘ 𝑋 ) ) → ( ( ◡ dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∪ { ∅ } ) × ran ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) ⊆ ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
48 45 46 47 mp2an ⊢ ( ( ◡ dom ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∪ { ∅ } ) × ran ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) ⊆ ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) )
49 39 48 sstri ⊢ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) )
50 elpw2g ⊢ ( ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ∈ 𝑈 → ( tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∈ 𝒫 ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ↔ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ) )
51 37 50 syl ⊢ ( 𝜑 → ( tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∈ 𝒫 ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ↔ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ⊆ ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ) )
52 49 51 mpbiri ⊢ ( 𝜑 → tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∈ 𝒫 ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
53 52 ralrimivw ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∈ 𝒫 ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
54 53 ralrimivw ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∈ 𝒫 ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
55 eqid ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) )
56 55 fmpo ⊢ ( ∀ 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ∈ 𝒫 ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ↔ ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) × ( Base ‘ 𝑋 ) ) ⟶ 𝒫 ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
57 54 56 sylib ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) × ( Base ‘ 𝑋 ) ) ⟶ 𝒫 ( ( ◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
58 4 27 38 57 wunf ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) ∈ 𝑈 )
59 4 23 58 wunop ⊢ ( 𝜑 → ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) ⟩ ∈ 𝑈 )
60 4 21 59 wunsets ⊢ ( 𝜑 → ( ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st ‘ 𝑥 ) ) ) ⟩ ) ∈ 𝑈 )
61 11 60 eqeltrd ⊢ ( 𝜑 → 𝑂 ∈ 𝑈 )
62 13 elin2d ⊢ ( 𝜑 → 𝑋 ∈ Cat )
63 3 oppccat ⊢ ( 𝑋 ∈ Cat → 𝑂 ∈ Cat )
64 62 63 syl ⊢ ( 𝜑 → 𝑂 ∈ Cat )
65 61 64 elind ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑈 ∩ Cat ) )
66 65 12 eleqtrrd ⊢ ( 𝜑 → 𝑂 ∈ 𝐵 )