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) (Proof shortened by AV, 13-Oct-2024)

Ref Expression
Hypotheses catcoppccl.c ⊢ C = CatCat ⁡ U
catcoppccl.b ⊢ B = Base C
catcoppccl.o ⊢ O = oppCat ⁡ X
catcoppccl.1 ⊢ φ → U ∈ WUni
catcoppccl.2 ⊢ φ → ω ∈ U
catcoppccl.3 ⊢ φ → X ∈ B
Assertion catcoppccl ⊢ φ → O ∈ B

Proof

Step Hyp Ref Expression
1 catcoppccl.c ⊢ C = CatCat ⁡ U
2 catcoppccl.b ⊢ B = Base C
3 catcoppccl.o ⊢ O = oppCat ⁡ X
4 catcoppccl.1 ⊢ φ → U ∈ WUni
5 catcoppccl.2 ⊢ φ → ω ∈ U
6 catcoppccl.3 ⊢ φ → X ∈ B
7 eqid ⊢ Base X = Base X
8 eqid ⊢ Hom ⁡ X = Hom ⁡ X
9 eqid ⊢ comp ⁡ X = comp ⁡ X
10 7 8 9 3 oppcval ⊢ X ∈ B → O = X sSet Hom ⁡ ndx tpos Hom ⁡ X sSet comp ⁡ ndx x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x
11 6 10 syl ⊢ φ → O = X sSet Hom ⁡ ndx tpos Hom ⁡ X sSet comp ⁡ ndx x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x
12 1 2 4 6 catcbascl ⊢ φ → X ∈ U
13 homid ⊢ Hom = Slot Hom ⁡ ndx
14 4 5 wunndx ⊢ φ → ndx ∈ U
15 13 4 14 wunstr ⊢ φ → Hom ⁡ ndx ∈ U
16 1 2 4 6 catchomcl ⊢ φ → Hom ⁡ X ∈ U
17 4 16 wuntpos ⊢ φ → tpos Hom ⁡ X ∈ U
18 4 15 17 wunop ⊢ φ → Hom ⁡ ndx tpos Hom ⁡ X ∈ U
19 4 12 18 wunsets ⊢ φ → X sSet Hom ⁡ ndx tpos Hom ⁡ X ∈ U
20 ccoid ⊢ comp = Slot comp ⁡ ndx
21 20 4 14 wunstr ⊢ φ → comp ⁡ ndx ∈ U
22 1 2 4 6 catcbaselcl ⊢ φ → Base X ∈ U
23 4 22 22 wunxp ⊢ φ → Base X × Base X ∈ U
24 4 23 22 wunxp ⊢ φ → Base X × Base X × Base X ∈ U
25 1 2 4 6 catcccocl ⊢ φ → comp ⁡ X ∈ U
26 4 25 wunrn ⊢ φ → ran ⁡ comp ⁡ X ∈ U
27 4 26 wununi ⊢ φ → ⋃ ran ⁡ comp ⁡ X ∈ U
28 4 27 wundm ⊢ φ → dom ⁡ ⋃ ran ⁡ comp ⁡ X ∈ U
29 4 28 wuncnv ⊢ φ → dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∈ U
30 4 wun0 ⊢ φ → ∅ ∈ U
31 4 30 wunsn ⊢ φ → ∅ ∈ U
32 4 29 31 wunun ⊢ φ → dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ ∈ U
33 4 27 wunrn ⊢ φ → ran ⁡ ⋃ ran ⁡ comp ⁡ X ∈ U
34 4 32 33 wunxp ⊢ φ → dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X ∈ U
35 4 34 wunpw ⊢ φ → 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X ∈ U
36 tposssxp ⊢ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x -1 ∪ ∅ × ran ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x
37 ovssunirn ⊢ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ ⋃ ran ⁡ comp ⁡ X
38 dmss ⊢ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ ⋃ ran ⁡ comp ⁡ X → dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X
39 37 38 ax-mp ⊢ dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X
40 cnvss ⊢ dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X → dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x -1 ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1
41 unss1 ⊢ dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x -1 ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 → dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x -1 ∪ ∅ ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅
42 39 40 41 mp2b ⊢ dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x -1 ∪ ∅ ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅
43 37 rnssi ⊢ ran ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ ran ⁡ ⋃ ran ⁡ comp ⁡ X
44 xpss12 ⊢ dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x -1 ∪ ∅ ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ ∧ ran ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ ran ⁡ ⋃ ran ⁡ comp ⁡ X → dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x -1 ∪ ∅ × ran ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
45 42 43 44 mp2an ⊢ dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x -1 ∪ ∅ × ran ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
46 36 45 sstri ⊢ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
47 elpw2g ⊢ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X ∈ U → tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X ↔ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
48 34 47 syl ⊢ φ → tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X ↔ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
49 46 48 mpbiri ⊢ φ → tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
50 49 ralrimivw ⊢ φ → ∀ y ∈ Base X tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
51 50 ralrimivw ⊢ φ → ∀ x ∈ Base X × Base X ∀ y ∈ Base X tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
52 eqid ⊢ x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x = x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x
53 52 fmpo ⊢ ∀ x ∈ Base X × Base X ∀ y ∈ Base X tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X ↔ x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x : Base X × Base X × Base X ⟶ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
54 51 53 sylib ⊢ φ → x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x : Base X × Base X × Base X ⟶ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
55 4 24 35 54 wunf ⊢ φ → x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ U
56 4 21 55 wunop ⊢ φ → comp ⁡ ndx x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ U
57 4 19 56 wunsets ⊢ φ → X sSet Hom ⁡ ndx tpos Hom ⁡ X sSet comp ⁡ ndx x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ U
58 11 57 eqeltrd ⊢ φ → O ∈ U
59 1 2 4 catcbas ⊢ φ → B = U ∩ Cat
60 6 59 eleqtrd ⊢ φ → X ∈ U ∩ Cat
61 60 elin2d ⊢ φ → X ∈ Cat
62 3 oppccat ⊢ X ∈ Cat → O ∈ Cat
63 61 62 syl ⊢ φ → O ∈ Cat
64 58 63 elind ⊢ φ → O ∈ U ∩ Cat
65 64 59 eleqtrrd ⊢ φ → O ∈ B