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	$⊢ φ \to U \in WUni$
	catcoppccl.2	$⊢ φ \to ω \in U$
	catcoppccl.3	$⊢ φ \to X \in B$
Assertion	catcoppccl	$⊢ φ \to O \in 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	$⊢ φ \to U \in WUni$
5		catcoppccl.2	$⊢ φ \to ω \in U$
6		catcoppccl.3	$⊢ φ \to X \in 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 \in B \to O = (X sSet ⟨Hom (ndx), tpos Hom (X)⟩) sSet ⟨comp (ndx), (x \in ({Base}_{X} \times {Base}_{X}), y \in {Base}_{X} ⟼ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)))⟩$
11	6 10	syl	$⊢ φ \to O = (X sSet ⟨Hom (ndx), tpos Hom (X)⟩) sSet ⟨comp (ndx), (x \in ({Base}_{X} \times {Base}_{X}), y \in {Base}_{X} ⟼ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)))⟩$
12	1 2 4 6	catcbascl	$⊢ φ \to X \in U$
13		homid	$⊢ Hom = Slot Hom (ndx)$
14	4 5	wunndx	$⊢ φ \to ndx \in U$
15	13 4 14	wunstr	$⊢ φ \to Hom (ndx) \in U$
16	1 2 4 6	catchomcl	$⊢ φ \to Hom (X) \in U$
17	4 16	wuntpos	$⊢ φ \to tpos Hom (X) \in U$
18	4 15 17	wunop	$⊢ φ \to ⟨Hom (ndx), tpos Hom (X)⟩ \in U$
19	4 12 18	wunsets	$⊢ φ \to X sSet ⟨Hom (ndx), tpos Hom (X)⟩ \in U$
20		ccoid	$⊢ comp = Slot comp (ndx)$
21	20 4 14	wunstr	$⊢ φ \to comp (ndx) \in U$
22	1 2 4 6	catcbaselcl	$⊢ φ \to {Base}_{X} \in U$
23	4 22 22	wunxp	$⊢ φ \to {Base}_{X} \times {Base}_{X} \in U$
24	4 23 22	wunxp	$⊢ φ \to ({Base}_{X} \times {Base}_{X}) \times {Base}_{X} \in U$
25	1 2 4 6	catcccocl	$⊢ φ \to comp (X) \in U$
26	4 25	wunrn	$⊢ φ \to ran comp (X) \in U$
27	4 26	wununi	$⊢ φ \to ⋃ ran comp (X) \in U$
28	4 27	wundm	$⊢ φ \to dom ⋃ ran comp (X) \in U$
29	4 28	wuncnv	$⊢ φ \to {dom ⋃ ran comp (X)}^{-1} \in U$
30	4	wun0	$⊢ φ \to \emptyset \in U$
31	4 30	wunsn	$⊢ φ \to \{\emptyset\} \in U$
32	4 29 31	wunun	$⊢ φ \to {dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\} \in U$
33	4 27	wunrn	$⊢ φ \to ran ⋃ ran comp (X) \in U$
34	4 32 33	wunxp	$⊢ φ \to ({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X) \in U$
35	4 34	wunpw	$⊢ φ \to 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X)) \in U$
36		tposssxp	$⊢ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ({dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))}^{-1} \cup \{\emptyset\}) \times ran (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))$
37		ovssunirn	$⊢ ⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x) \subseteq ⋃ ran comp (X)$
38		dmss	$⊢ ⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x) \subseteq ⋃ ran comp (X) \to dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq dom ⋃ ran comp (X)$
39	37 38	ax-mp	$⊢ dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq dom ⋃ ran comp (X)$
40		cnvss	$⊢ dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq dom ⋃ ran comp (X) \to {dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))}^{-1} \subseteq {dom ⋃ ran comp (X)}^{-1}$
41		unss1	$⊢ {dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))}^{-1} \subseteq {dom ⋃ ran comp (X)}^{-1} \to {dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))}^{-1} \cup \{\emptyset\} \subseteq {dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}$
42	39 40 41	mp2b	$⊢ {dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))}^{-1} \cup \{\emptyset\} \subseteq {dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}$
43	37	rnssi	$⊢ ran (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ran ⋃ ran comp (X)$
44		xpss12	$⊢ ({dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))}^{-1} \cup \{\emptyset\} \subseteq {dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\} \land ran (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ran ⋃ ran comp (X)) \to ({dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))}^{-1} \cup \{\emptyset\}) \times ran (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X)$
45	42 43 44	mp2an	$⊢ ({dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))}^{-1} \cup \{\emptyset\}) \times ran (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X)$
46	36 45	sstri	$⊢ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X)$
47		elpw2g	$⊢ ({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X) \in U \to (tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \in 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X)) \leftrightarrow tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X))$
48	34 47	syl	$⊢ φ \to (tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \in 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X)) \leftrightarrow tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X))$
49	46 48	mpbiri	$⊢ φ \to tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \in 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X))$
50	49	ralrimivw	$⊢ φ \to \forall y \in {Base}_{X} tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \in 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X))$
51	50	ralrimivw	$⊢ φ \to \forall x \in ({Base}_{X} \times {Base}_{X}) \forall y \in {Base}_{X} tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \in 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X))$
52		eqid	$⊢ (x \in ({Base}_{X} \times {Base}_{X}), y \in {Base}_{X} ⟼ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))) = (x \in ({Base}_{X} \times {Base}_{X}), y \in {Base}_{X} ⟼ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)))$
53	52	fmpo	$⊢ \forall x \in ({Base}_{X} \times {Base}_{X}) \forall y \in {Base}_{X} tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \in 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X)) \leftrightarrow (x \in ({Base}_{X} \times {Base}_{X}), y \in {Base}_{X} ⟼ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))) : ({Base}_{X} \times {Base}_{X}) \times {Base}_{X} ⟶ 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X))$
54	51 53	sylib	$⊢ φ \to (x \in ({Base}_{X} \times {Base}_{X}), y \in {Base}_{X} ⟼ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))) : ({Base}_{X} \times {Base}_{X}) \times {Base}_{X} ⟶ 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X))$
55	4 24 35 54	wunf	$⊢ φ \to (x \in ({Base}_{X} \times {Base}_{X}), y \in {Base}_{X} ⟼ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))) \in U$
56	4 21 55	wunop	$⊢ φ \to ⟨comp (ndx), (x \in ({Base}_{X} \times {Base}_{X}), y \in {Base}_{X} ⟼ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)))⟩ \in U$
57	4 19 56	wunsets	$⊢ φ \to (X sSet ⟨Hom (ndx), tpos Hom (X)⟩) sSet ⟨comp (ndx), (x \in ({Base}_{X} \times {Base}_{X}), y \in {Base}_{X} ⟼ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)))⟩ \in U$
58	11 57	eqeltrd	$⊢ φ \to O \in U$
59	1 2 4	catcbas	$⊢ φ \to B = U \cap Cat$
60	6 59	eleqtrd	$⊢ φ \to X \in (U \cap Cat)$
61	60	elin2d	$⊢ φ \to X \in Cat$
62	3	oppccat	$⊢ X \in Cat \to O \in Cat$
63	61 62	syl	$⊢ φ \to O \in Cat$
64	58 63	elind	$⊢ φ \to O \in (U \cap Cat)$
65	64 59	eleqtrrd	$⊢ φ \to O \in B$

Metamath Proof Explorer

Theorem catcoppccl

Proof