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	$⊢ 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	catcoppcclOLD	$⊢ φ \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	catcbas	$⊢ φ \to B = U \cap Cat$
13	6 12	eleqtrd	$⊢ φ \to X \in (U \cap Cat)$
14	13	elin1d	$⊢ φ \to X \in U$
15		df-hom	$⊢ Hom = Slot 14$
16	4 5	wunndx	$⊢ φ \to ndx \in U$
17	15 4 16	wunstr	$⊢ φ \to Hom (ndx) \in U$
18	15 4 14	wunstr	$⊢ φ \to Hom (X) \in U$
19	4 18	wuntpos	$⊢ φ \to tpos Hom (X) \in U$
20	4 17 19	wunop	$⊢ φ \to ⟨Hom (ndx), tpos Hom (X)⟩ \in U$
21	4 14 20	wunsets	$⊢ φ \to X sSet ⟨Hom (ndx), tpos Hom (X)⟩ \in U$
22		df-cco	$⊢ comp = Slot 15$
23	22 4 16	wunstr	$⊢ φ \to comp (ndx) \in U$
24		df-base	$⊢ Base = Slot 1$
25	24 4 14	wunstr	$⊢ φ \to {Base}_{X} \in U$
26	4 25 25	wunxp	$⊢ φ \to {Base}_{X} \times {Base}_{X} \in U$
27	4 26 25	wunxp	$⊢ φ \to ({Base}_{X} \times {Base}_{X}) \times {Base}_{X} \in U$
28	22 4 14	wunstr	$⊢ φ \to comp (X) \in U$
29	4 28	wunrn	$⊢ φ \to ran comp (X) \in U$
30	4 29	wununi	$⊢ φ \to ⋃ ran comp (X) \in U$
31	4 30	wundm	$⊢ φ \to dom ⋃ ran comp (X) \in U$
32	4 31	wuncnv	$⊢ φ \to {dom ⋃ ran comp (X)}^{-1} \in U$
33	4	wun0	$⊢ φ \to \emptyset \in U$
34	4 33	wunsn	$⊢ φ \to \{\emptyset\} \in U$
35	4 32 34	wunun	$⊢ φ \to {dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\} \in U$
36	4 30	wunrn	$⊢ φ \to ran ⋃ ran comp (X) \in U$
37	4 35 36	wunxp	$⊢ φ \to ({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X) \in U$
38	4 37	wunpw	$⊢ φ \to 𝒫 (({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X)) \in U$
39		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))$
40		ovssunirn	$⊢ ⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x) \subseteq ⋃ ran comp (X)$
41		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)$
42	40 41	ax-mp	$⊢ dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq dom ⋃ ran comp (X)$
43		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}$
44		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\}$
45	42 43 44	mp2b	$⊢ {dom (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x))}^{-1} \cup \{\emptyset\} \subseteq {dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}$
46	40	rnssi	$⊢ ran (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ran ⋃ ran comp (X)$
47		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)$
48	45 46 47	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)$
49	39 48	sstri	$⊢ tpos (⟨y, 2^{nd} (x)⟩ comp (X) 1^{st} (x)) \subseteq ({dom ⋃ ran comp (X)}^{-1} \cup \{\emptyset\}) \times ran ⋃ ran comp (X)$
50		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))$
51	37 50	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))$
52	49 51	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))$
53	52	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))$
54	53	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))$
55		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)))$
56	55	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))$
57	54 56	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))$
58	4 27 38 57	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$
59	4 23 58	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$
60	4 21 59	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$
61	11 60	eqeltrd	$⊢ φ \to O \in U$
62	13	elin2d	$⊢ φ \to X \in Cat$
63	3	oppccat	$⊢ X \in Cat \to O \in Cat$
64	62 63	syl	$⊢ φ \to O \in Cat$
65	61 64	elind	$⊢ φ \to O \in (U \cap Cat)$
66	65 12	eleqtrrd	$⊢ φ \to O \in B$

Metamath Proof Explorer

Theorem catcoppcclOLD

Proof