| Step | Hyp | Ref
| Expression |
| 1 | | catcoppccl.3 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑋) =
(Base‘𝑋) |
| 3 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝑋) = (Hom
‘𝑋) |
| 4 | | eqid 2737 |
. . . . . 6
⊢
(comp‘𝑋) =
(comp‘𝑋) |
| 5 | | catcoppccl.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝑋) |
| 6 | 2, 3, 4, 5 | oppcval 17756 |
. . . . 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 | | catcoppccl.c |
. . . . . . 7
⊢ 𝐶 = (CatCat‘𝑈) |
| 10 | | catcoppccl.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
| 11 | 9, 10, 8, 1 | catcbascl 18157 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
| 12 | | homid 17456 |
. . . . . . . 8
⊢ Hom =
Slot (Hom ‘ndx) |
| 13 | | catcoppccl.2 |
. . . . . . . . 9
⊢ (𝜑 → ω ∈ 𝑈) |
| 14 | 8, 13 | wunndx 17232 |
. . . . . . . 8
⊢ (𝜑 → ndx ∈ 𝑈) |
| 15 | 12, 8, 14 | wunstr 17225 |
. . . . . . 7
⊢ (𝜑 → (Hom ‘ndx) ∈
𝑈) |
| 16 | 9, 10, 8, 1 | catchomcl 18160 |
. . . . . . . 8
⊢ (𝜑 → (Hom ‘𝑋) ∈ 𝑈) |
| 17 | 8, 16 | wuntpos 10774 |
. . . . . . 7
⊢ (𝜑 → tpos (Hom ‘𝑋) ∈ 𝑈) |
| 18 | 8, 15, 17 | wunop 10762 |
. . . . . 6
⊢ (𝜑 → 〈(Hom ‘ndx),
tpos (Hom ‘𝑋)〉
∈ 𝑈) |
| 19 | 8, 11, 18 | wunsets 17214 |
. . . . 5
⊢ (𝜑 → (𝑋 sSet 〈(Hom ‘ndx), tpos (Hom
‘𝑋)〉) ∈
𝑈) |
| 20 | | ccoid 17458 |
. . . . . . 7
⊢ comp =
Slot (comp‘ndx) |
| 21 | 20, 8, 14 | wunstr 17225 |
. . . . . 6
⊢ (𝜑 → (comp‘ndx) ∈
𝑈) |
| 22 | 9, 10, 8, 1 | catcbaselcl 18159 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈) |
| 23 | 8, 22, 22 | wunxp 10764 |
. . . . . . . 8
⊢ (𝜑 → ((Base‘𝑋) × (Base‘𝑋)) ∈ 𝑈) |
| 24 | 8, 23, 22 | wunxp 10764 |
. . . . . . 7
⊢ (𝜑 → (((Base‘𝑋) × (Base‘𝑋)) × (Base‘𝑋)) ∈ 𝑈) |
| 25 | 9, 10, 8, 1 | catcccocl 18161 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (comp‘𝑋) ∈ 𝑈) |
| 26 | 8, 25 | wunrn 10769 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (comp‘𝑋) ∈ 𝑈) |
| 27 | 8, 26 | wununi 10746 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ ran (comp‘𝑋) ∈ 𝑈) |
| 28 | 8, 27 | wundm 10768 |
. . . . . . . . . . 11
⊢ (𝜑 → dom ∪ ran (comp‘𝑋) ∈ 𝑈) |
| 29 | 8, 28 | wuncnv 10770 |
. . . . . . . . . 10
⊢ (𝜑 → ◡dom ∪ ran
(comp‘𝑋) ∈ 𝑈) |
| 30 | 8 | wun0 10758 |
. . . . . . . . . . 11
⊢ (𝜑 → ∅ ∈ 𝑈) |
| 31 | 8, 30 | wunsn 10756 |
. . . . . . . . . 10
⊢ (𝜑 → {∅} ∈ 𝑈) |
| 32 | 8, 29, 31 | wunun 10750 |
. . . . . . . . 9
⊢ (𝜑 → (◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) ∈ 𝑈) |
| 33 | 8, 27 | wunrn 10769 |
. . . . . . . . 9
⊢ (𝜑 → ran ∪ ran (comp‘𝑋) ∈ 𝑈) |
| 34 | 8, 32, 33 | wunxp 10764 |
. . . . . . . 8
⊢ (𝜑 → ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) ∈ 𝑈) |
| 35 | 8, 34 | wunpw 10747 |
. . . . . . 7
⊢ (𝜑 → 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) ∈ 𝑈) |
| 36 | | tposssxp 8255 |
. . . . . . . . . . . 12
⊢ tpos
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ((◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) × ran (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) |
| 37 | | ovssunirn 7467 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑦,
(2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ∪ ran
(comp‘𝑋) |
| 38 | | dmss 5913 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑦,
(2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ∪ ran
(comp‘𝑋) → dom
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ dom ∪
ran (comp‘𝑋)) |
| 39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ dom
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ dom ∪
ran (comp‘𝑋) |
| 40 | | cnvss 5883 |
. . . . . . . . . . . . . 14
⊢ (dom
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ dom ∪
ran (comp‘𝑋) →
◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ◡dom ∪ ran
(comp‘𝑋)) |
| 41 | | unss1 4185 |
. . . . . . . . . . . . . 14
⊢ (◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ◡dom ∪ ran
(comp‘𝑋) →
(◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) ⊆ (◡dom ∪ ran
(comp‘𝑋) ∪
{∅})) |
| 42 | 39, 40, 41 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) ⊆ (◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) |
| 43 | 37 | rnssi 5951 |
. . . . . . . . . . . . 13
⊢ ran
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ran ∪
ran (comp‘𝑋) |
| 44 | | xpss12 5700 |
. . . . . . . . . . . . 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‘𝑋))) |
| 45 | 42, 43, 44 | mp2an 692 |
. . . . . . . . . . . 12
⊢ ((◡dom (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) × ran (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) ⊆ ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) |
| 46 | 36, 45 | sstri 3993 |
. . . . . . . . . . 11
⊢ tpos
(〈𝑦, (2nd
‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) |
| 47 | | elpw2g 5333 |
. . . . . . . . . . . 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‘𝑋)))) |
| 48 | 34, 47 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)) ↔ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ⊆ ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋)))) |
| 49 | 46, 48 | mpbiri 258 |
. . . . . . . . . 10
⊢ (𝜑 → tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋))) |
| 50 | 49 | ralrimivw 3150 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ (Base‘𝑋)tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋))) |
| 51 | 50 | ralrimivw 3150 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋))∀𝑦 ∈ (Base‘𝑋)tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋))) |
| 52 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) = (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) |
| 53 | 52 | fmpo 8093 |
. . . . . . . 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‘𝑋))) |
| 54 | 51, 53 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))):(((Base‘𝑋) × (Base‘𝑋)) × (Base‘𝑋))⟶𝒫 ((◡dom ∪ ran
(comp‘𝑋) ∪
{∅}) × ran ∪ ran (comp‘𝑋))) |
| 55 | 8, 24, 35, 54 | wunf 10767 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥))) ∈ 𝑈) |
| 56 | 8, 21, 55 | wunop 10762 |
. . . . 5
⊢ (𝜑 → 〈(comp‘ndx),
(𝑥 ∈
((Base‘𝑋) ×
(Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)))〉 ∈ 𝑈) |
| 57 | 8, 19, 56 | wunsets 17214 |
. . . 4
⊢ (𝜑 → ((𝑋 sSet 〈(Hom ‘ndx), tpos (Hom
‘𝑋)〉) sSet
〈(comp‘ndx), (𝑥
∈ ((Base‘𝑋)
× (Base‘𝑋)),
𝑦 ∈ (Base‘𝑋) ↦ tpos (〈𝑦, (2nd ‘𝑥)〉(comp‘𝑋)(1st ‘𝑥)))〉) ∈ 𝑈) |
| 58 | 7, 57 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → 𝑂 ∈ 𝑈) |
| 59 | 9, 10, 8 | catcbas 18146 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) |
| 60 | 1, 59 | eleqtrd 2843 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝑈 ∩ Cat)) |
| 61 | 60 | elin2d 4205 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Cat) |
| 62 | 5 | oppccat 17765 |
. . . 4
⊢ (𝑋 ∈ Cat → 𝑂 ∈ Cat) |
| 63 | 61, 62 | syl 17 |
. . 3
⊢ (𝜑 → 𝑂 ∈ Cat) |
| 64 | 58, 63 | elind 4200 |
. 2
⊢ (𝜑 → 𝑂 ∈ (𝑈 ∩ Cat)) |
| 65 | 64, 59 | eleqtrrd 2844 |
1
⊢ (𝜑 → 𝑂 ∈ 𝐵) |