Theorem catcoppcclOLD 18185

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

Hypotheses

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

Assertion

Ref	Expression
catcoppcclOLD	⊢ (𝜑 → 𝑂 ∈ 𝐵)

Proof of Theorem catcoppcclOLD

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		catcoppccl.3	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
2		eqid 2740	. . . . . 6 ⊢ (Base‘𝑋) = (Base‘𝑋)
3		eqid 2740	. . . . . 6 ⊢ (Hom ‘𝑋) = (Hom ‘𝑋)
4		eqid 2740	. . . . . 6 ⊢ (comp‘𝑋) = (comp‘𝑋)
5		catcoppccl.o	. . . . . 6 ⊢ 𝑂 = (oppCat‘𝑋)
6	2, 3, 4, 5	oppcval 17771	. . . . 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	. . . . . . . . 9 ⊢ 𝐶 = (CatCat‘𝑈)
10		catcoppccl.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐶)
11	9, 10, 8	catcbas 18168	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
12	1, 11	eleqtrd 2846	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝑈 ∩ Cat))
13	12	elin1d 4227	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
14		df-hom 17335	. . . . . . . 8 ⊢ Hom = Slot ;14
15		catcoppccl.2	. . . . . . . . 9 ⊢ (𝜑 → ω ∈ 𝑈)
16	8, 15	wunndx 17242	. . . . . . . 8 ⊢ (𝜑 → ndx ∈ 𝑈)
17	14, 8, 16	wunstr 17235	. . . . . . 7 ⊢ (𝜑 → (Hom ‘ndx) ∈ 𝑈)
18	14, 8, 13	wunstr 17235	. . . . . . . 8 ⊢ (𝜑 → (Hom ‘𝑋) ∈ 𝑈)
19	8, 18	wuntpos 10803	. . . . . . 7 ⊢ (𝜑 → tpos (Hom ‘𝑋) ∈ 𝑈)
20	8, 17, 19	wunop 10791	. . . . . 6 ⊢ (𝜑 → ⟨(Hom ‘ndx), tpos (Hom ‘𝑋)⟩ ∈ 𝑈)
21	8, 13, 20	wunsets 17224	. . . . 5 ⊢ (𝜑 → (𝑋 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑋)⟩) ∈ 𝑈)
22		df-cco 17336	. . . . . . 7 ⊢ comp = Slot ;15
23	22, 8, 16	wunstr 17235	. . . . . 6 ⊢ (𝜑 → (comp‘ndx) ∈ 𝑈)
24		df-base 17259	. . . . . . . . . 10 ⊢ Base = Slot 1
25	24, 8, 13	wunstr 17235	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈)
26	8, 25, 25	wunxp 10793	. . . . . . . 8 ⊢ (𝜑 → ((Base‘𝑋) × (Base‘𝑋)) ∈ 𝑈)
27	8, 26, 25	wunxp 10793	. . . . . . 7 ⊢ (𝜑 → (((Base‘𝑋) × (Base‘𝑋)) × (Base‘𝑋)) ∈ 𝑈)
28	22, 8, 13	wunstr 17235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (comp‘𝑋) ∈ 𝑈)
29	8, 28	wunrn 10798	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (comp‘𝑋) ∈ 𝑈)
30	8, 29	wununi 10775	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ ran (comp‘𝑋) ∈ 𝑈)
31	8, 30	wundm 10797	. . . . . . . . . . 11 ⊢ (𝜑 → dom ∪ ran (comp‘𝑋) ∈ 𝑈)
32	8, 31	wuncnv 10799	. . . . . . . . . 10 ⊢ (𝜑 → ◡dom ∪ ran (comp‘𝑋) ∈ 𝑈)
33	8	wun0 10787	. . . . . . . . . . 11 ⊢ (𝜑 → ∅ ∈ 𝑈)
34	8, 33	wunsn 10785	. . . . . . . . . 10 ⊢ (𝜑 → {∅} ∈ 𝑈)
35	8, 32, 34	wunun 10779	. . . . . . . . 9 ⊢ (𝜑 → (◡dom ∪ ran (comp‘𝑋) ∪ {∅}) ∈ 𝑈)
36	8, 30	wunrn 10798	. . . . . . . . 9 ⊢ (𝜑 → ran ∪ ran (comp‘𝑋) ∈ 𝑈)
37	8, 35, 36	wunxp 10793	. . . . . . . 8 ⊢ (𝜑 → ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋)) ∈ 𝑈)
38	8, 37	wunpw 10776	. . . . . . 7 ⊢ (𝜑 → 𝒫 ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋)) ∈ 𝑈)
39		tposssxp 8271	. . . . . . . . . . . 12 ⊢ tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ ((◡dom (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) × ran (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)))
40		ovssunirn 7484	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ ∪ ran (comp‘𝑋)
41		dmss 5927	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ ∪ ran (comp‘𝑋) → dom (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ dom ∪ ran (comp‘𝑋))
42	40, 41	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ dom (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ dom ∪ ran (comp‘𝑋)
43		cnvss 5897	. . . . . . . . . . . . . 14 ⊢ (dom (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ dom ∪ ran (comp‘𝑋) → ◡dom (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ ◡dom ∪ ran (comp‘𝑋))
44		unss1 4208	. . . . . . . . . . . . . 14 ⊢ (◡dom (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ ◡dom ∪ ran (comp‘𝑋) → (◡dom (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) ⊆ (◡dom ∪ ran (comp‘𝑋) ∪ {∅}))
45	42, 43, 44	mp2b 10	. . . . . . . . . . . . 13 ⊢ (◡dom (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) ⊆ (◡dom ∪ ran (comp‘𝑋) ∪ {∅})
46	40	rnssi 5965	. . . . . . . . . . . . 13 ⊢ ran (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ ran ∪ ran (comp‘𝑋)
47		xpss12 5715	. . . . . . . . . . . . 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‘𝑋)))
48	45, 46, 47	mp2an 691	. . . . . . . . . . . 12 ⊢ ((◡dom (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ∪ {∅}) × ran (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥))) ⊆ ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋))
49	39, 48	sstri 4018	. . . . . . . . . . 11 ⊢ tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋))
50		elpw2g 5351	. . . . . . . . . . . 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‘𝑋))))
51	37, 50	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋)) ↔ tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ⊆ ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋))))
52	49, 51	mpbiri 258	. . . . . . . . . 10 ⊢ (𝜑 → tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋)))
53	52	ralrimivw 3156	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦 ∈ (Base‘𝑋)tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋)))
54	53	ralrimivw 3156	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋))∀𝑦 ∈ (Base‘𝑋)tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)) ∈ 𝒫 ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋)))
55		eqid 2740	. . . . . . . . 9 ⊢ (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥))) = (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)))
56	55	fmpo 8109	. . . . . . . 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‘𝑋)))
57	54, 56	sylib 218	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥))):(((Base‘𝑋) × (Base‘𝑋)) × (Base‘𝑋))⟶𝒫 ((◡dom ∪ ran (comp‘𝑋) ∪ {∅}) × ran ∪ ran (comp‘𝑋)))
58	8, 27, 38, 57	wunf 10796	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥))) ∈ 𝑈)
59	8, 23, 58	wunop 10791	. . . . 5 ⊢ (𝜑 → ⟨(comp‘ndx), (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)))⟩ ∈ 𝑈)
60	8, 21, 59	wunsets 17224	. . . 4 ⊢ (𝜑 → ((𝑋 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑋)⟩) sSet ⟨(comp‘ndx), (𝑥 ∈ ((Base‘𝑋) × (Base‘𝑋)), 𝑦 ∈ (Base‘𝑋) ↦ tpos (⟨𝑦, (2nd ‘𝑥)⟩(comp‘𝑋)(1st ‘𝑥)))⟩) ∈ 𝑈)
61	7, 60	eqeltrd 2844	. . 3 ⊢ (𝜑 → 𝑂 ∈ 𝑈)
62	12	elin2d 4228	. . . 4 ⊢ (𝜑 → 𝑋 ∈ Cat)
63	5	oppccat 17782	. . . 4 ⊢ (𝑋 ∈ Cat → 𝑂 ∈ Cat)
64	62, 63	syl 17	. . 3 ⊢ (𝜑 → 𝑂 ∈ Cat)
65	61, 64	elind 4223	. 2 ⊢ (𝜑 → 𝑂 ∈ (𝑈 ∩ Cat))
66	65, 11	eleqtrrd 2847	1 ⊢ (𝜑 → 𝑂 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ∀wral 3067   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  𝒫 cpw 4622  {csn 4648  ⟨cop 4654  ∪ cuni 4931   × cxp 5698  ^◡ccnv 5699  dom cdm 5700  ran crn 5701  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450  ωcom 7903  1^st c1st 8028  2^nd c2nd 8029  tpos ctpos 8266  WUnicwun 10769  1c1 11185  4c4 12350  5c5 12351  ;cdc 12758   sSet csts 17210  ndxcnx 17240  Basecbs 17258  Hom chom 17322  compcco 17323  Catccat 17722  oppCatcoppc 17769  CatCatccatc 18165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-tpos 8267  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-oadd 8526  df-omul 8527  df-er 8763  df-ec 8765  df-qs 8769  df-map 8886  df-pm 8887  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-wun 10771  df-ni 10941  df-pli 10942  df-mi 10943  df-lti 10944  df-plpq 10977  df-mpq 10978  df-ltpq 10979  df-enq 10980  df-nq 10981  df-erq 10982  df-plq 10983  df-mq 10984  df-1nq 10985  df-rq 10986  df-ltnq 10987  df-np 11050  df-plp 11052  df-ltp 11054  df-enr 11124  df-nr 11125  df-c 11190  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-z 12640  df-dec 12759  df-uz 12904  df-fz 13568  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-hom 17335  df-cco 17336  df-cat 17726  df-cid 17727  df-oppc 17770  df-catc 18166

This theorem is referenced by: (None)