catcxpccl

Description: The category of categories for a weak universe is closed under the product category operation. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	catcxpccl.c	$⊢ C = CatCat (U)$
	catcxpccl.b	$⊢ B = {Base}_{C}$
	catcxpccl.o	$⊢ T = X \times_{c} Y$
	catcxpccl.u	$⊢ φ \to U \in WUni$
	catcxpccl.1	$⊢ φ \to ω \in U$
	catcxpccl.x	$⊢ φ \to X \in B$
	catcxpccl.y	$⊢ φ \to Y \in B$
Assertion	catcxpccl	$⊢ φ \to T \in B$

Proof

Step	Hyp	Ref	Expression
1		catcxpccl.c	$⊢ C = CatCat (U)$
2		catcxpccl.b	$⊢ B = {Base}_{C}$
3		catcxpccl.o	$⊢ T = X \times_{c} Y$
4		catcxpccl.u	$⊢ φ \to U \in WUni$
5		catcxpccl.1	$⊢ φ \to ω \in U$
6		catcxpccl.x	$⊢ φ \to X \in B$
7		catcxpccl.y	$⊢ φ \to Y \in B$
8		eqid	$⊢ {Base}_{X} = {Base}_{X}$
9		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
10		eqid	$⊢ Hom (X) = Hom (X)$
11		eqid	$⊢ Hom (Y) = Hom (Y)$
12		eqid	$⊢ comp (X) = comp (X)$
13		eqid	$⊢ comp (Y) = comp (Y)$
14		eqidd	$⊢ φ \to {Base}_{X} \times {Base}_{Y} = {Base}_{X} \times {Base}_{Y}$
15	3 8 9	xpcbas	$⊢ {Base}_{X} \times {Base}_{Y} = {Base}_{T}$
16		eqid	$⊢ Hom (T) = Hom (T)$
17	3 15 10 11 16	xpchomfval	$⊢ Hom (T) = (u \in ({Base}_{X} \times {Base}_{Y}), v \in ({Base}_{X} \times {Base}_{Y}) ⟼ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)))$
18	17	a1i	$⊢ φ \to Hom (T) = (u \in ({Base}_{X} \times {Base}_{Y}), v \in ({Base}_{X} \times {Base}_{Y}) ⟼ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)))$
19		eqidd	$⊢ φ \to (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩)) = (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩))$
20	3 8 9 10 11 12 13 6 7 14 18 19	xpcval	$⊢ φ \to T = \{⟨{Base}_{ndx}, {Base}_{X} \times {Base}_{Y}⟩, ⟨Hom (ndx), Hom (T)⟩, ⟨comp (ndx), (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\}$
21		df-base	$⊢ Base = Slot 1$
22	4 5	wunndx	$⊢ φ \to ndx \in U$
23	21 4 22	wunstr	$⊢ φ \to {Base}_{ndx} \in U$
24	1 2 4	catcbas	$⊢ φ \to B = U \cap Cat$
25	6 24	eleqtrd	$⊢ φ \to X \in (U \cap Cat)$
26	25	elin1d	$⊢ φ \to X \in U$
27	21 4 26	wunstr	$⊢ φ \to {Base}_{X} \in U$
28	7 24	eleqtrd	$⊢ φ \to Y \in (U \cap Cat)$
29	28	elin1d	$⊢ φ \to Y \in U$
30	21 4 29	wunstr	$⊢ φ \to {Base}_{Y} \in U$
31	4 27 30	wunxp	$⊢ φ \to {Base}_{X} \times {Base}_{Y} \in U$
32	4 23 31	wunop	$⊢ φ \to ⟨{Base}_{ndx}, {Base}_{X} \times {Base}_{Y}⟩ \in U$
33		df-hom	$⊢ Hom = Slot 14$
34	33 4 22	wunstr	$⊢ φ \to Hom (ndx) \in U$
35	4 31 31	wunxp	$⊢ φ \to ({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y}) \in U$
36	33 4 26	wunstr	$⊢ φ \to Hom (X) \in U$
37	4 36	wunrn	$⊢ φ \to ran Hom (X) \in U$
38	4 37	wununi	$⊢ φ \to ⋃ ran Hom (X) \in U$
39	33 4 29	wunstr	$⊢ φ \to Hom (Y) \in U$
40	4 39	wunrn	$⊢ φ \to ran Hom (Y) \in U$
41	4 40	wununi	$⊢ φ \to ⋃ ran Hom (Y) \in U$
42	4 38 41	wunxp	$⊢ φ \to ⋃ ran Hom (X) \times ⋃ ran Hom (Y) \in U$
43	4 42	wunpw	$⊢ φ \to 𝒫 (⋃ ran Hom (X) \times ⋃ ran Hom (Y)) \in U$
44		ovssunirn	$⊢ 1^{st} (u) Hom (X) 1^{st} (v) \subseteq ⋃ ran Hom (X)$
45		ovssunirn	$⊢ 2^{nd} (u) Hom (Y) 2^{nd} (v) \subseteq ⋃ ran Hom (Y)$
46		xpss12	$⊢ (1^{st} (u) Hom (X) 1^{st} (v) \subseteq ⋃ ran Hom (X) \land 2^{nd} (u) Hom (Y) 2^{nd} (v) \subseteq ⋃ ran Hom (Y)) \to (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)) \subseteq ⋃ ran Hom (X) \times ⋃ ran Hom (Y)$
47	44 45 46	mp2an	$⊢ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)) \subseteq ⋃ ran Hom (X) \times ⋃ ran Hom (Y)$
48		ovex	$⊢ 1^{st} (u) Hom (X) 1^{st} (v) \in V$
49		ovex	$⊢ 2^{nd} (u) Hom (Y) 2^{nd} (v) \in V$
50	48 49	xpex	$⊢ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)) \in V$
51	50	elpw	$⊢ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)) \in 𝒫 (⋃ ran Hom (X) \times ⋃ ran Hom (Y)) \leftrightarrow (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)) \subseteq ⋃ ran Hom (X) \times ⋃ ran Hom (Y)$
52	47 51	mpbir	$⊢ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)) \in 𝒫 (⋃ ran Hom (X) \times ⋃ ran Hom (Y))$
53	52	rgen2w	$⊢ \forall u \in ({Base}_{X} \times {Base}_{Y}) \forall v \in ({Base}_{X} \times {Base}_{Y}) (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)) \in 𝒫 (⋃ ran Hom (X) \times ⋃ ran Hom (Y))$
54		eqid	$⊢ (u \in ({Base}_{X} \times {Base}_{Y}), v \in ({Base}_{X} \times {Base}_{Y}) ⟼ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v))) = (u \in ({Base}_{X} \times {Base}_{Y}), v \in ({Base}_{X} \times {Base}_{Y}) ⟼ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)))$
55	54	fmpo	$⊢ \forall u \in ({Base}_{X} \times {Base}_{Y}) \forall v \in ({Base}_{X} \times {Base}_{Y}) (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)) \in 𝒫 (⋃ ran Hom (X) \times ⋃ ran Hom (Y)) \leftrightarrow (u \in ({Base}_{X} \times {Base}_{Y}), v \in ({Base}_{X} \times {Base}_{Y}) ⟼ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v))) : ({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y}) ⟶ 𝒫 (⋃ ran Hom (X) \times ⋃ ran Hom (Y))$
56	53 55	mpbi	$⊢ (u \in ({Base}_{X} \times {Base}_{Y}), v \in ({Base}_{X} \times {Base}_{Y}) ⟼ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v))) : ({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y}) ⟶ 𝒫 (⋃ ran Hom (X) \times ⋃ ran Hom (Y))$
57	56	a1i	$⊢ φ \to (u \in ({Base}_{X} \times {Base}_{Y}), v \in ({Base}_{X} \times {Base}_{Y}) ⟼ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v))) : ({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y}) ⟶ 𝒫 (⋃ ran Hom (X) \times ⋃ ran Hom (Y))$
58	4 35 43 57	wunf	$⊢ φ \to (u \in ({Base}_{X} \times {Base}_{Y}), v \in ({Base}_{X} \times {Base}_{Y}) ⟼ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v))) \in U$
59	17 58	eqeltrid	$⊢ φ \to Hom (T) \in U$
60	4 34 59	wunop	$⊢ φ \to ⟨Hom (ndx), Hom (T)⟩ \in U$
61		df-cco	$⊢ comp = Slot 15$
62	61 4 22	wunstr	$⊢ φ \to comp (ndx) \in U$
63	4 35 31	wunxp	$⊢ φ \to (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})) \times ({Base}_{X} \times {Base}_{Y}) \in U$
64	61 4 26	wunstr	$⊢ φ \to comp (X) \in U$
65	4 64	wunrn	$⊢ φ \to ran comp (X) \in U$
66	4 65	wununi	$⊢ φ \to ⋃ ran comp (X) \in U$
67	4 66	wunrn	$⊢ φ \to ran ⋃ ran comp (X) \in U$
68	4 67	wununi	$⊢ φ \to ⋃ ran ⋃ ran comp (X) \in U$
69	4 68	wunpw	$⊢ φ \to 𝒫 ⋃ ran ⋃ ran comp (X) \in U$
70	61 4 29	wunstr	$⊢ φ \to comp (Y) \in U$
71	4 70	wunrn	$⊢ φ \to ran comp (Y) \in U$
72	4 71	wununi	$⊢ φ \to ⋃ ran comp (Y) \in U$
73	4 72	wunrn	$⊢ φ \to ran ⋃ ran comp (Y) \in U$
74	4 73	wununi	$⊢ φ \to ⋃ ran ⋃ ran comp (Y) \in U$
75	4 74	wunpw	$⊢ φ \to 𝒫 ⋃ ran ⋃ ran comp (Y) \in U$
76	4 69 75	wunxp	$⊢ φ \to 𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y) \in U$
77	4 59	wunrn	$⊢ φ \to ran Hom (T) \in U$
78	4 77	wununi	$⊢ φ \to ⋃ ran Hom (T) \in U$
79	4 78 78	wunxp	$⊢ φ \to ⋃ ran Hom (T) \times ⋃ ran Hom (T) \in U$
80	4 76 79	wunpm	$⊢ φ \to (𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) ↑_{𝑝𝑚} (⋃ ran Hom (T) \times ⋃ ran Hom (T)) \in U$
81		fvex	$⊢ comp (X) \in V$
82	81	rnex	$⊢ ran comp (X) \in V$
83	82	uniex	$⊢ ⋃ ran comp (X) \in V$
84	83	rnex	$⊢ ran ⋃ ran comp (X) \in V$
85	84	uniex	$⊢ ⋃ ran ⋃ ran comp (X) \in V$
86	85	pwex	$⊢ 𝒫 ⋃ ran ⋃ ran comp (X) \in V$
87		fvex	$⊢ comp (Y) \in V$
88	87	rnex	$⊢ ran comp (Y) \in V$
89	88	uniex	$⊢ ⋃ ran comp (Y) \in V$
90	89	rnex	$⊢ ran ⋃ ran comp (Y) \in V$
91	90	uniex	$⊢ ⋃ ran ⋃ ran comp (Y) \in V$
92	91	pwex	$⊢ 𝒫 ⋃ ran ⋃ ran comp (Y) \in V$
93	86 92	xpex	$⊢ 𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y) \in V$
94		fvex	$⊢ Hom (T) \in V$
95	94	rnex	$⊢ ran Hom (T) \in V$
96	95	uniex	$⊢ ⋃ ran Hom (T) \in V$
97	96 96	xpex	$⊢ ⋃ ran Hom (T) \times ⋃ ran Hom (T) \in V$
98		ovssunirn	$⊢ 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f) \subseteq ⋃ ran (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y))$
99		ovssunirn	$⊢ ⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y) \subseteq ⋃ ran comp (X)$
100		rnss	$⊢ ⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y) \subseteq ⋃ ran comp (X) \to ran (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) \subseteq ran ⋃ ran comp (X)$
101		uniss	$⊢ ran (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) \subseteq ran ⋃ ran comp (X) \to ⋃ ran (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) \subseteq ⋃ ran ⋃ ran comp (X)$
102	99 100 101	mp2b	$⊢ ⋃ ran (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) \subseteq ⋃ ran ⋃ ran comp (X)$
103	98 102	sstri	$⊢ 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f) \subseteq ⋃ ran ⋃ ran comp (X)$
104		ovex	$⊢ 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f) \in V$
105	104	elpw	$⊢ 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f) \in 𝒫 ⋃ ran ⋃ ran comp (X) \leftrightarrow 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f) \subseteq ⋃ ran ⋃ ran comp (X)$
106	103 105	mpbir	$⊢ 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f) \in 𝒫 ⋃ ran ⋃ ran comp (X)$
107		ovssunirn	$⊢ 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f) \subseteq ⋃ ran (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y))$
108		ovssunirn	$⊢ ⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y) \subseteq ⋃ ran comp (Y)$
109		rnss	$⊢ ⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y) \subseteq ⋃ ran comp (Y) \to ran (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) \subseteq ran ⋃ ran comp (Y)$
110		uniss	$⊢ ran (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) \subseteq ran ⋃ ran comp (Y) \to ⋃ ran (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) \subseteq ⋃ ran ⋃ ran comp (Y)$
111	108 109 110	mp2b	$⊢ ⋃ ran (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) \subseteq ⋃ ran ⋃ ran comp (Y)$
112	107 111	sstri	$⊢ 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f) \subseteq ⋃ ran ⋃ ran comp (Y)$
113		ovex	$⊢ 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f) \in V$
114	113	elpw	$⊢ 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f) \in 𝒫 ⋃ ran ⋃ ran comp (Y) \leftrightarrow 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f) \subseteq ⋃ ran ⋃ ran comp (Y)$
115	112 114	mpbir	$⊢ 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f) \in 𝒫 ⋃ ran ⋃ ran comp (Y)$
116		opelxpi	$⊢ (1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f) \in 𝒫 ⋃ ran ⋃ ran comp (X) \land 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f) \in 𝒫 ⋃ ran ⋃ ran comp (Y)) \to ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩ \in (𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y))$
117	106 115 116	mp2an	$⊢ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩ \in (𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y))$
118	117	rgen2w	$⊢ \forall g \in (2^{nd} (x) Hom (T) y) \forall f \in Hom (T) (x) ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩ \in (𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y))$
119		eqid	$⊢ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩) = (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩)$
120	119	fmpo	$⊢ \forall g \in (2^{nd} (x) Hom (T) y) \forall f \in Hom (T) (x) ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩ \in (𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) \leftrightarrow (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩) : (2^{nd} (x) Hom (T) y) \times Hom (T) (x) ⟶ 𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)$
121	118 120	mpbi	$⊢ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩) : (2^{nd} (x) Hom (T) y) \times Hom (T) (x) ⟶ 𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)$
122		ovssunirn	$⊢ 2^{nd} (x) Hom (T) y \subseteq ⋃ ran Hom (T)$
123		fvssunirn	$⊢ Hom (T) (x) \subseteq ⋃ ran Hom (T)$
124		xpss12	$⊢ (2^{nd} (x) Hom (T) y \subseteq ⋃ ran Hom (T) \land Hom (T) (x) \subseteq ⋃ ran Hom (T)) \to (2^{nd} (x) Hom (T) y) \times Hom (T) (x) \subseteq ⋃ ran Hom (T) \times ⋃ ran Hom (T)$
125	122 123 124	mp2an	$⊢ (2^{nd} (x) Hom (T) y) \times Hom (T) (x) \subseteq ⋃ ran Hom (T) \times ⋃ ran Hom (T)$
126		elpm2r	$⊢ ((𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y) \in V \land ⋃ ran Hom (T) \times ⋃ ran Hom (T) \in V) \land ((g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩) : (2^{nd} (x) Hom (T) y) \times Hom (T) (x) ⟶ 𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y) \land (2^{nd} (x) Hom (T) y) \times Hom (T) (x) \subseteq ⋃ ran Hom (T) \times ⋃ ran Hom (T))) \to (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩) \in ((𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) ↑_{𝑝𝑚} (⋃ ran Hom (T) \times ⋃ ran Hom (T)))$
127	93 97 121 125 126	mp4an	$⊢ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩) \in ((𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) ↑_{𝑝𝑚} (⋃ ran Hom (T) \times ⋃ ran Hom (T)))$
128	127	rgen2w	$⊢ \forall x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})) \forall y \in ({Base}_{X} \times {Base}_{Y}) (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩) \in ((𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) ↑_{𝑝𝑚} (⋃ ran Hom (T) \times ⋃ ran Hom (T)))$
129		eqid	$⊢ (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩)) = (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩))$
130	129	fmpo	$⊢ \forall x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})) \forall y \in ({Base}_{X} \times {Base}_{Y}) (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩) \in ((𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) ↑_{𝑝𝑚} (⋃ ran Hom (T) \times ⋃ ran Hom (T))) \leftrightarrow (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩)) : (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})) \times ({Base}_{X} \times {Base}_{Y}) ⟶ (𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) ↑_{𝑝𝑚} (⋃ ran Hom (T) \times ⋃ ran Hom (T))$
131	128 130	mpbi	$⊢ (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩)) : (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})) \times ({Base}_{X} \times {Base}_{Y}) ⟶ (𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) ↑_{𝑝𝑚} (⋃ ran Hom (T) \times ⋃ ran Hom (T))$
132	131	a1i	$⊢ φ \to (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩)) : (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})) \times ({Base}_{X} \times {Base}_{Y}) ⟶ (𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) ↑_{𝑝𝑚} (⋃ ran Hom (T) \times ⋃ ran Hom (T))$
133	4 63 80 132	wunf	$⊢ φ \to (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩)) \in U$
134	4 62 133	wunop	$⊢ φ \to ⟨comp (ndx), (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩))⟩ \in U$
135	4 32 60 134	wuntp	$⊢ φ \to \{⟨{Base}_{ndx}, {Base}_{X} \times {Base}_{Y}⟩, ⟨Hom (ndx), Hom (T)⟩, ⟨comp (ndx), (x \in (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})), y \in ({Base}_{X} \times {Base}_{Y}) ⟼ (g \in (2^{nd} (x) Hom (T) y), f \in Hom (T) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\} \in U$
136	20 135	eqeltrd	$⊢ φ \to T \in U$
137	25	elin2d	$⊢ φ \to X \in Cat$
138	28	elin2d	$⊢ φ \to Y \in Cat$
139	3 137 138	xpccat	$⊢ φ \to T \in Cat$
140	136 139	elind	$⊢ φ \to T \in (U \cap Cat)$
141	140 24	eleqtrrd	$⊢ φ \to T \in B$

Metamath Proof Explorer

Theorem catcxpccl

Proof