catcoppcclOLD

Description: Obsolete proof of catcoppccl as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	catcoppccl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcoppccl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	catcoppccl.o	⊢ 𝑂 = ( oppCat ‘ 𝑋 )
	catcoppccl.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	catcoppccl.2	⊢ ( 𝜑 → ω ∈ 𝑈 )
	catcoppccl.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	catcoppcclOLD	⊢ ( 𝜑 → 𝑂 ∈ 𝐵 )

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	catcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
13	6 12	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Cat ) )
14	13	elin1d	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
15		df-hom	⊢ Hom = Slot ; 1 4
16	4 5	wunndx	⊢ ( 𝜑 → ndx ∈ 𝑈 )
17	15 4 16	wunstr	⊢ ( 𝜑 → ( Hom ‘ ndx ) ∈ 𝑈 )
18	15 4 14	wunstr	⊢ ( 𝜑 → ( Hom ‘ 𝑋 ) ∈ 𝑈 )
19	4 18	wuntpos	⊢ ( 𝜑 → tpos ( Hom ‘ 𝑋 ) ∈ 𝑈 )
20	4 17 19	wunop	⊢ ( 𝜑 → ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ∈ 𝑈 )
21	4 14 20	wunsets	⊢ ( 𝜑 → ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) ∈ 𝑈 )
22		df-cco	⊢ comp = Slot ; 1 5
23	22 4 16	wunstr	⊢ ( 𝜑 → ( comp ‘ ndx ) ∈ 𝑈 )
24		df-base	⊢ Base = Slot 1
25	24 4 14	wunstr	⊢ ( 𝜑 → ( Base ‘ 𝑋 ) ∈ 𝑈 )
26	4 25 25	wunxp	⊢ ( 𝜑 → ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ∈ 𝑈 )
27	4 26 25	wunxp	⊢ ( 𝜑 → ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) × ( Base ‘ 𝑋 ) ) ∈ 𝑈 )
28	22 4 14	wunstr	⊢ ( 𝜑 → ( comp ‘ 𝑋 ) ∈ 𝑈 )
29	4 28	wunrn	⊢ ( 𝜑 → ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
30	4 29	wununi	⊢ ( 𝜑 → ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
31	4 30	wundm	⊢ ( 𝜑 → dom ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
32	4 31	wuncnv	⊢ ( 𝜑 → ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
33	4	wun0	⊢ ( 𝜑 → ∅ ∈ 𝑈 )
34	4 33	wunsn	⊢ ( 𝜑 → { ∅ } ∈ 𝑈 )
35	4 32 34	wunun	⊢ ( 𝜑 → ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) ∈ 𝑈 )
36	4 30	wunrn	⊢ ( 𝜑 → ran ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
37	4 35 36	wunxp	⊢ ( 𝜑 → ( ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ∈ 𝑈 )
38	4 37	wunpw	⊢ ( 𝜑 → 𝒫 ( ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) ∈ 𝑈 )
39		tposssxp	⊢ tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ ( ( ^◡ dom ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ∪ { ∅ } ) × ran ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) )
40		ovssunirn	⊢ ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ ∪ ran ( comp ‘ 𝑋 )
41		dmss	⊢ ( ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ ∪ ran ( comp ‘ 𝑋 ) → dom ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ dom ∪ ran ( comp ‘ 𝑋 ) )
42	40 41	ax-mp	⊢ dom ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ dom ∪ ran ( comp ‘ 𝑋 )
43		cnvss	⊢ ( dom ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ dom ∪ ran ( comp ‘ 𝑋 ) → ^◡ dom ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ ^◡ dom ∪ ran ( comp ‘ 𝑋 ) )
44		unss1	⊢ ( ^◡ dom ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ ^◡ dom ∪ ran ( comp ‘ 𝑋 ) → ( ^◡ dom ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ∪ { ∅ } ) ⊆ ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) )
45	42 43 44	mp2b	⊢ ( ^◡ dom ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ∪ { ∅ } ) ⊆ ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } )
46	40	rnssi	⊢ ran ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ ran ∪ ran ( comp ‘ 𝑋 )
47		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 ‘ 𝑋 ) ) )
48	45 46 47	mp2an	⊢ ( ( ^◡ dom ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ∪ { ∅ } ) × ran ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ) ⊆ ( ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) )
49	39 48	sstri	⊢ tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ⊆ ( ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) )
50		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 ‘ 𝑋 ) ) ) )
51	37 50	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 ‘ 𝑋 ) ) ) )
52	49 51	mpbiri	⊢ ( 𝜑 → tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ∈ 𝒫 ( ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
53	52	ralrimivw	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ∈ 𝒫 ( ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
54	53	ralrimivw	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ∈ 𝒫 ( ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
55		eqid	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) )
56	55	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 ‘ 𝑋 ) ) )
57	54 56	sylib	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) × ( Base ‘ 𝑋 ) ) ⟶ 𝒫 ( ( ^◡ dom ∪ ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ∪ ran ( comp ‘ 𝑋 ) ) )
58	4 27 38 57	wunf	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ) ∈ 𝑈 )
59	4 23 58	wunop	⊢ ( 𝜑 → ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ) ⟩ ∈ 𝑈 )
60	4 21 59	wunsets	⊢ ( 𝜑 → ( ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑥 ) ) ) ⟩ ) ∈ 𝑈 )
61	11 60	eqeltrd	⊢ ( 𝜑 → 𝑂 ∈ 𝑈 )
62	13	elin2d	⊢ ( 𝜑 → 𝑋 ∈ Cat )
63	3	oppccat	⊢ ( 𝑋 ∈ Cat → 𝑂 ∈ Cat )
64	62 63	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
65	61 64	elind	⊢ ( 𝜑 → 𝑂 ∈ ( 𝑈 ∩ Cat ) )
66	65 12	eleqtrrd	⊢ ( 𝜑 → 𝑂 ∈ 𝐵 )

Metamath Proof Explorer

Theorem catcoppcclOLD

Proof