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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcoppccl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	catcoppccl.o	⊢ 𝑂 = ( oppCat ‘ 𝑋 )
	catcoppccl.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	catcoppccl.2	⊢ ( 𝜑 → ω ∈ 𝑈 )
	catcoppccl.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	catcoppccl	⊢ ( 𝜑 → 𝑂 ∈ 𝐵 )

Proof

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

Metamath Proof Explorer

Theorem catcoppccl

Proof