catcxpccl

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

	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		baseid	$⊢ Base = Slot {Base}_{ndx}$
22	4 5	wunndx	$⊢ φ \to ndx \in U$
23	21 4 22	wunstr	$⊢ φ \to {Base}_{ndx} \in U$
24	1 2 4 6	catcbaselcl	$⊢ φ \to {Base}_{X} \in U$
25	1 2 4 7	catcbaselcl	$⊢ φ \to {Base}_{Y} \in U$
26	4 24 25	wunxp	$⊢ φ \to {Base}_{X} \times {Base}_{Y} \in U$
27	4 23 26	wunop	$⊢ φ \to ⟨{Base}_{ndx}, {Base}_{X} \times {Base}_{Y}⟩ \in U$
28		homid	$⊢ Hom = Slot Hom (ndx)$
29	28 4 22	wunstr	$⊢ φ \to Hom (ndx) \in U$
30	4 26 26	wunxp	$⊢ φ \to ({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y}) \in U$
31	1 2 4 6	catchomcl	$⊢ φ \to Hom (X) \in U$
32	4 31	wunrn	$⊢ φ \to ran Hom (X) \in U$
33	4 32	wununi	$⊢ φ \to ⋃ ran Hom (X) \in U$
34	1 2 4 7	catchomcl	$⊢ φ \to Hom (Y) \in U$
35	4 34	wunrn	$⊢ φ \to ran Hom (Y) \in U$
36	4 35	wununi	$⊢ φ \to ⋃ ran Hom (Y) \in U$
37	4 33 36	wunxp	$⊢ φ \to ⋃ ran Hom (X) \times ⋃ ran Hom (Y) \in U$
38	4 37	wunpw	$⊢ φ \to 𝒫 (⋃ ran Hom (X) \times ⋃ ran Hom (Y)) \in U$
39		ovssunirn	$⊢ 1^{st} (u) Hom (X) 1^{st} (v) \subseteq ⋃ ran Hom (X)$
40		ovssunirn	$⊢ 2^{nd} (u) Hom (Y) 2^{nd} (v) \subseteq ⋃ ran Hom (Y)$
41		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)$
42	39 40 41	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)$
43		ovex	$⊢ 1^{st} (u) Hom (X) 1^{st} (v) \in V$
44		ovex	$⊢ 2^{nd} (u) Hom (Y) 2^{nd} (v) \in V$
45	43 44	xpex	$⊢ (1^{st} (u) Hom (X) 1^{st} (v)) \times (2^{nd} (u) Hom (Y) 2^{nd} (v)) \in V$
46	45	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)$
47	42 46	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))$
48	47	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))$
49		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)))$
50	49	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))$
51	48 50	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))$
52	51	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))$
53	4 30 38 52	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$
54	17 53	eqeltrid	$⊢ φ \to Hom (T) \in U$
55	4 29 54	wunop	$⊢ φ \to ⟨Hom (ndx), Hom (T)⟩ \in U$
56		ccoid	$⊢ comp = Slot comp (ndx)$
57	56 4 22	wunstr	$⊢ φ \to comp (ndx) \in U$
58	4 30 26	wunxp	$⊢ φ \to (({Base}_{X} \times {Base}_{Y}) \times ({Base}_{X} \times {Base}_{Y})) \times ({Base}_{X} \times {Base}_{Y}) \in U$
59	1 2 4 6	catcccocl	$⊢ φ \to comp (X) \in U$
60	4 59	wunrn	$⊢ φ \to ran comp (X) \in U$
61	4 60	wununi	$⊢ φ \to ⋃ ran comp (X) \in U$
62	4 61	wunrn	$⊢ φ \to ran ⋃ ran comp (X) \in U$
63	4 62	wununi	$⊢ φ \to ⋃ ran ⋃ ran comp (X) \in U$
64	4 63	wunpw	$⊢ φ \to 𝒫 ⋃ ran ⋃ ran comp (X) \in U$
65	1 2 4 7	catcccocl	$⊢ φ \to comp (Y) \in U$
66	4 65	wunrn	$⊢ φ \to ran comp (Y) \in U$
67	4 66	wununi	$⊢ φ \to ⋃ ran comp (Y) \in U$
68	4 67	wunrn	$⊢ φ \to ran ⋃ ran comp (Y) \in U$
69	4 68	wununi	$⊢ φ \to ⋃ ran ⋃ ran comp (Y) \in U$
70	4 69	wunpw	$⊢ φ \to 𝒫 ⋃ ran ⋃ ran comp (Y) \in U$
71	4 64 70	wunxp	$⊢ φ \to 𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y) \in U$
72	4 54	wunrn	$⊢ φ \to ran Hom (T) \in U$
73	4 72	wununi	$⊢ φ \to ⋃ ran Hom (T) \in U$
74	4 73 73	wunxp	$⊢ φ \to ⋃ ran Hom (T) \times ⋃ ran Hom (T) \in U$
75	4 71 74	wunpm	$⊢ φ \to (𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y)) ↑_{𝑝𝑚} (⋃ ran Hom (T) \times ⋃ ran Hom (T)) \in U$
76		fvex	$⊢ comp (X) \in V$
77	76	rnex	$⊢ ran comp (X) \in V$
78	77	uniex	$⊢ ⋃ ran comp (X) \in V$
79	78	rnex	$⊢ ran ⋃ ran comp (X) \in V$
80	79	uniex	$⊢ ⋃ ran ⋃ ran comp (X) \in V$
81	80	pwex	$⊢ 𝒫 ⋃ ran ⋃ ran comp (X) \in V$
82		fvex	$⊢ comp (Y) \in V$
83	82	rnex	$⊢ ran comp (Y) \in V$
84	83	uniex	$⊢ ⋃ ran comp (Y) \in V$
85	84	rnex	$⊢ ran ⋃ ran comp (Y) \in V$
86	85	uniex	$⊢ ⋃ ran ⋃ ran comp (Y) \in V$
87	86	pwex	$⊢ 𝒫 ⋃ ran ⋃ ran comp (Y) \in V$
88	81 87	xpex	$⊢ 𝒫 ⋃ ran ⋃ ran comp (X) \times 𝒫 ⋃ ran ⋃ ran comp (Y) \in V$
89		fvex	$⊢ Hom (T) \in V$
90	89	rnex	$⊢ ran Hom (T) \in V$
91	90	uniex	$⊢ ⋃ ran Hom (T) \in V$
92	91 91	xpex	$⊢ ⋃ ran Hom (T) \times ⋃ ran Hom (T) \in V$
93		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))$
94		ovssunirn	$⊢ ⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y) \subseteq ⋃ ran comp (X)$
95		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)$
96		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)$
97	94 95 96	mp2b	$⊢ ⋃ ran (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) \subseteq ⋃ ran ⋃ ran comp (X)$
98	93 97	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)$
99		ovex	$⊢ 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (X) 1^{st} (y)) 1^{st} (f) \in V$
100	99	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)$
101	98 100	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)$
102		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))$
103		ovssunirn	$⊢ ⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y) \subseteq ⋃ ran comp (Y)$
104		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)$
105		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)$
106	103 104 105	mp2b	$⊢ ⋃ ran (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) \subseteq ⋃ ran ⋃ ran comp (Y)$
107	102 106	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)$
108		ovex	$⊢ 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (Y) 2^{nd} (y)) 2^{nd} (f) \in V$
109	108	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)$
110	107 109	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)$
111		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))$
112	101 110 111	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))$
113	112	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))$
114		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)⟩)$
115	114	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)$
116	113 115	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)$
117		ovssunirn	$⊢ 2^{nd} (x) Hom (T) y \subseteq ⋃ ran Hom (T)$
118		fvssunirn	$⊢ Hom (T) (x) \subseteq ⋃ ran Hom (T)$
119		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)$
120	117 118 119	mp2an	$⊢ (2^{nd} (x) Hom (T) y) \times Hom (T) (x) \subseteq ⋃ ran Hom (T) \times ⋃ ran Hom (T)$
121		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)))$
122	88 92 116 120 121	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)))$
123	122	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)))$
124		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)⟩))$
125	124	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))$
126	123 125	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))$
127	126	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))$
128	4 58 75 127	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$
129	4 57 128	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$
130	4 27 55 129	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$
131	20 130	eqeltrd	$⊢ φ \to T \in U$
132	1 2 4	catcbas	$⊢ φ \to B = U \cap Cat$
133	6 132	eleqtrd	$⊢ φ \to X \in (U \cap Cat)$
134	133	elin2d	$⊢ φ \to X \in Cat$
135	7 132	eleqtrd	$⊢ φ \to Y \in (U \cap Cat)$
136	135	elin2d	$⊢ φ \to Y \in Cat$
137	3 134 136	xpccat	$⊢ φ \to T \in Cat$
138	131 137	elind	$⊢ φ \to T \in (U \cap Cat)$
139	138 132	eleqtrrd	$⊢ φ \to T \in B$

Metamath Proof Explorer

Theorem catcxpccl

Proof