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 ⊢ 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 catcbas ⊢ φ → B = U ∩ Cat
13 6 12 eleqtrd ⊢ φ → X ∈ U ∩ Cat
14 13 elin1d ⊢ φ → X ∈ U
15 df-hom ⊢ Hom = Slot 14
16 4 5 wunndx ⊢ φ → ndx ∈ U
17 15 4 16 wunstr ⊢ φ → Hom ⁡ ndx ∈ U
18 15 4 14 wunstr ⊢ φ → Hom ⁡ X ∈ U
19 4 18 wuntpos ⊢ φ → tpos Hom ⁡ X ∈ U
20 4 17 19 wunop ⊢ φ → Hom ⁡ ndx tpos Hom ⁡ X ∈ U
21 4 14 20 wunsets ⊢ φ → X sSet Hom ⁡ ndx tpos Hom ⁡ X ∈ U
22 df-cco ⊢ comp = Slot 15
23 22 4 16 wunstr ⊢ φ → comp ⁡ ndx ∈ U
24 df-base ⊢ Base = Slot 1
25 24 4 14 wunstr ⊢ φ → Base X ∈ U
26 4 25 25 wunxp ⊢ φ → Base X × Base X ∈ U
27 4 26 25 wunxp ⊢ φ → Base X × Base X × Base X ∈ U
28 22 4 14 wunstr ⊢ φ → comp ⁡ X ∈ U
29 4 28 wunrn ⊢ φ → ran ⁡ comp ⁡ X ∈ U
30 4 29 wununi ⊢ φ → ⋃ ran ⁡ comp ⁡ X ∈ U
31 4 30 wundm ⊢ φ → dom ⁡ ⋃ ran ⁡ comp ⁡ X ∈ U
32 4 31 wuncnv ⊢ φ → dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∈ U
33 4 wun0 ⊢ φ → ∅ ∈ U
34 4 33 wunsn ⊢ φ → ∅ ∈ U
35 4 32 34 wunun ⊢ φ → dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ ∈ U
36 4 30 wunrn ⊢ φ → ran ⁡ ⋃ ran ⁡ comp ⁡ X ∈ U
37 4 35 36 wunxp ⊢ φ → dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X ∈ U
38 4 37 wunpw ⊢ φ → 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X ∈ U
39 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
40 ovssunirn ⊢ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ ⋃ ran ⁡ comp ⁡ X
41 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
42 40 41 ax-mp ⊢ dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X
43 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
44 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 ∪ ∅
45 42 43 44 mp2b ⊢ dom ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x -1 ∪ ∅ ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅
46 40 rnssi ⊢ ran ⁡ y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ ran ⁡ ⋃ ran ⁡ comp ⁡ X
47 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
48 45 46 47 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
49 39 48 sstri ⊢ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ⊆ dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
50 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
51 37 50 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
52 49 51 mpbiri ⊢ φ → tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
53 52 ralrimivw ⊢ φ → ∀ y ∈ Base X tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ 𝒫 dom ⁡ ⋃ ran ⁡ comp ⁡ X -1 ∪ ∅ × ran ⁡ ⋃ ran ⁡ comp ⁡ X
54 53 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
55 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
56 55 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
57 54 56 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
58 4 27 38 57 wunf ⊢ φ → x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ U
59 4 23 58 wunop ⊢ φ → comp ⁡ ndx x ∈ Base X × Base X , y ∈ Base X ⟼ tpos y 2 nd ⁡ x comp ⁡ X 1 st ⁡ x ∈ U
60 4 21 59 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
61 11 60 eqeltrd ⊢ φ → O ∈ U
62 13 elin2d ⊢ φ → X ∈ Cat
63 3 oppccat ⊢ X ∈ Cat → O ∈ Cat
64 62 63 syl ⊢ φ → O ∈ Cat
65 61 64 elind ⊢ φ → O ∈ U ∩ Cat
66 65 12 eleqtrrd ⊢ φ → O ∈ B