Step | Hyp | Ref
| Expression |
1 | | catcoppccl.3 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
2 | | eqid 2824 |
. . . . . 6
⊢
(Base‘𝑋) =
(Base‘𝑋) |
3 | | eqid 2824 |
. . . . . 6
⊢ (Hom
‘𝑋) = (Hom
‘𝑋) |
4 | | eqid 2824 |
. . . . . 6
⊢
(comp‘𝑋) =
(comp‘𝑋) |
5 | | catcoppccl.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝑋) |
6 | 2, 3, 4, 5 | oppcval 16724 |
. . . . 5
⊢ (𝑋 ∈ 𝐵 → 𝑂 = ((𝑋 sSet 〈(Hom ‘ndx), tpos (Hom
‘𝑋)〉) sSet
〈(comp‘ndx), (𝑥
∈ ((Base‘𝑋)
× (Base‘𝑋)),
𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)))〉)) |
7 | 1, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑂 = ((𝑋 sSet 〈(Hom ‘ndx), tpos (Hom
‘𝑋)〉) sSet
〈(comp‘ndx), (𝑥
∈ ((Base‘𝑋)
× (Base‘𝑋)),
𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)))〉)) |
8 | | catcoppccl.1 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ WUni) |
9 | | inss1 4056 |
. . . . . . 7
⊢ (𝑈 ∩ Cat) ⊆ 𝑈 |
10 | | catcoppccl.c |
. . . . . . . . 9
⊢ 𝐶 = (CatCat‘𝑈) |
11 | | catcoppccl.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐶) |
12 | 10, 11, 8 | catcbas 17098 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) |
13 | 1, 12 | eleqtrd 2907 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (𝑈 ∩ Cat)) |
14 | 9, 13 | sseldi 3824 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
15 | | df-hom 16328 |
. . . . . . . 8
⊢ Hom =
Slot ;14 |
16 | | catcoppccl.2 |
. . . . . . . . 9
⊢ (𝜑 → ω ∈ 𝑈) |
17 | 8, 16 | wunndx 16242 |
. . . . . . . 8
⊢ (𝜑 → ndx ∈ 𝑈) |
18 | 15, 8, 17 | wunstr 16245 |
. . . . . . 7
⊢ (𝜑 → (Hom ‘ndx) ∈
𝑈) |
19 | 15, 8, 14 | wunstr 16245 |
. . . . . . . 8
⊢ (𝜑 → (Hom ‘𝑋) ∈ 𝑈) |
20 | 8, 19 | wuntpos 9870 |
. . . . . . 7
⊢ (𝜑 → tpos (Hom ‘𝑋) ∈ 𝑈) |
21 | 8, 18, 20 | wunop 9858 |
. . . . . 6
⊢ (𝜑 → 〈(Hom ‘ndx),
tpos (Hom ‘𝑋)〉
∈ 𝑈) |
22 | 8, 14, 21 | wunsets 16262 |
. . . . 5
⊢ (𝜑 → (𝑋 sSet 〈(Hom ‘ndx), tpos (Hom
‘𝑋)〉) ∈
𝑈) |
23 | | df-cco 16329 |
. . . . . . 7
⊢ comp =
Slot ;15 |
24 | 23, 8, 17 | wunstr 16245 |
. . . . . 6
⊢ (𝜑 → (comp‘ndx) ∈
𝑈) |
25 | | df-base 16227 |
. . . . . . . . . 10
⊢ Base =
Slot 1 |
26 | 25, 8, 14 | wunstr 16245 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈) |
27 | 8, 26, 26 | wunxp 9860 |
. . . . . . . 8
⊢ (𝜑 → ((Base‘𝑋) × (Base‘𝑋)) ∈ 𝑈) |
28 | 8, 27, 26 | wunxp 9860 |
. . . . . . 7
⊢ (𝜑 → (((Base‘𝑋) × (Base‘𝑋)) × (Base‘𝑋)) ∈ 𝑈) |
29 | 23, 8, 14 | wunstr 16245 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (comp‘𝑋) ∈ 𝑈) |
30 | 8, 29 | wunrn 9865 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (comp‘𝑋) ∈ 𝑈) |
31 | 8, 30 | wununi 9842 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ ran (comp‘𝑋) ∈ 𝑈) |
32 | 8, 31 | wundm 9864 |
. . . . . . . . . . 11
⊢ (𝜑 → dom ∪ ran (comp‘𝑋) ∈ 𝑈) |
33 | 8, 32 | wuncnv 9866 |
. . . . . . . . . 10
⊢ (𝜑 → ◡dom ∪ ran
(comp‘𝑋) ∈ 𝑈) |
34 | 8 | wun0 9854 |
. . . . . . . . . . 11
⊢ (𝜑 → ∅ ∈ 𝑈) |
35 | 8, 34 | wunsn 9852 |
. . . . . . . . . 10
⊢ (𝜑 → {∅} ∈ 𝑈) |
36 | 8, 33, 35 | wunun 9846 |
. . . . . . . . 9
⊢ (𝜑 → (◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) ∈ 𝑈) |
37 | 8, 31 | wunrn 9865 |
. . . . . . . . 9
⊢ (𝜑 → ran ∪ ran (comp‘𝑋) ∈ 𝑈) |
38 | 8, 36, 37 | wunxp 9860 |
. . . . . . . 8
⊢ (𝜑 → ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) ∈ 𝑈) |
39 | 8, 38 | wunpw 9843 |
. . . . . . 7
⊢ (𝜑 → 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) ∈ 𝑈) |
40 | | tposssxp 7620 |
. . . . . . . . . . . 12
⊢ tpos
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ((◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) × ran (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) |
41 | | ovssunirn 6939 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑦,
(2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ∪ ran
(comp‘𝑋) |
42 | | dmss 5554 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑦,
(2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ∪ ran
(comp‘𝑋) → dom
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ dom ∪
ran (comp‘𝑋)) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ dom
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ dom ∪
ran (comp‘𝑋) |
44 | | cnvss 5526 |
. . . . . . . . . . . . . 14
⊢ (dom
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ dom ∪
ran (comp‘𝑋) →
◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ◡dom ∪ ran
(comp‘𝑋)) |
45 | | unss1 4008 |
. . . . . . . . . . . . . 14
⊢ (◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ◡dom ∪ ran
(comp‘𝑋) →
(◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) ⊆ (◡dom ∪ ran
(comp‘𝑋) ∪
{∅})) |
46 | 43, 44, 45 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) ⊆ (◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) |
47 | | rnss 5585 |
. . . . . . . . . . . . . 14
⊢
((〈𝑦,
(2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ∪ ran
(comp‘𝑋) → ran
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ran ∪
ran (comp‘𝑋)) |
48 | 41, 47 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ran
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ran ∪
ran (comp‘𝑋) |
49 | | xpss12 5356 |
. . . . . . . . . . . . 13
⊢ (((◡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‘𝑋))) |
50 | 46, 48, 49 | mp2an 685 |
. . . . . . . . . . . 12
⊢ ((◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) × ran (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) ⊆ ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) |
51 | 40, 50 | sstri 3835 |
. . . . . . . . . . 11
⊢ tpos
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) |
52 | | elpw2g 5048 |
. . . . . . . . . . . 12
⊢ (((◡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‘𝑋)))) |
53 | 38, 52 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) ↔ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)))) |
54 | 51, 53 | mpbiri 250 |
. . . . . . . . . 10
⊢ (𝜑 → tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋))) |
55 | 54 | ralrimivw 3175 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ (Base‘𝑋)tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋))) |
56 | 55 | ralrimivw 3175 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋))∀𝑦 ∈ (Base‘𝑋)tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋))) |
57 | | eqid 2824 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) = (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) |
58 | 57 | fmpt2 7499 |
. . . . . . . 8
⊢
(∀𝑥 ∈
((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‘𝑋))) |
59 | 56, 58 | sylib 210 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))):(((Base‘𝑋) × (Base‘𝑋)) × (Base‘𝑋))⟶𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋))) |
60 | 8, 28, 39, 59 | wunf 9863 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) ∈ 𝑈) |
61 | 8, 24, 60 | wunop 9858 |
. . . . 5
⊢ (𝜑 → 〈(comp‘ndx),
(𝑥 ∈
((Base‘𝑋) ×
(Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)))〉 ∈ 𝑈) |
62 | 8, 22, 61 | wunsets 16262 |
. . . 4
⊢ (𝜑 → ((𝑋 sSet 〈(Hom ‘ndx), tpos (Hom
‘𝑋)〉) sSet
〈(comp‘ndx), (𝑥
∈ ((Base‘𝑋)
× (Base‘𝑋)),
𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)))〉) ∈ 𝑈) |
63 | 7, 62 | eqeltrd 2905 |
. . 3
⊢ (𝜑 → 𝑂 ∈ 𝑈) |
64 | | inss2 4057 |
. . . . 5
⊢ (𝑈 ∩ Cat) ⊆
Cat |
65 | 64, 13 | sseldi 3824 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Cat) |
66 | 5 | oppccat 16733 |
. . . 4
⊢ (𝑋 ∈ Cat → 𝑂 ∈ Cat) |
67 | 65, 66 | syl 17 |
. . 3
⊢ (𝜑 → 𝑂 ∈ Cat) |
68 | 63, 67 | elind 4024 |
. 2
⊢ (𝜑 → 𝑂 ∈ (𝑈 ∩ Cat)) |
69 | 68, 12 | eleqtrrd 2908 |
1
⊢ (𝜑 → 𝑂 ∈ 𝐵) |