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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcxpccl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	catcxpccl.o	⊢ 𝑇 = ( 𝑋 ×_c 𝑌 )
	catcxpccl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	catcxpccl.1	⊢ ( 𝜑 → ω ∈ 𝑈 )
	catcxpccl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	catcxpccl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	catcxpccl	⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		catcxpccl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catcxpccl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		catcxpccl.o	⊢ 𝑇 = ( 𝑋 ×_c 𝑌 )
4		catcxpccl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
5		catcxpccl.1	⊢ ( 𝜑 → ω ∈ 𝑈 )
6		catcxpccl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		catcxpccl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		eqid	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
9		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
10		eqid	⊢ ( Hom ‘ 𝑋 ) = ( Hom ‘ 𝑋 )
11		eqid	⊢ ( Hom ‘ 𝑌 ) = ( Hom ‘ 𝑌 )
12		eqid	⊢ ( comp ‘ 𝑋 ) = ( comp ‘ 𝑋 )
13		eqid	⊢ ( comp ‘ 𝑌 ) = ( comp ‘ 𝑌 )
14		eqidd	⊢ ( 𝜑 → ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) = ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) )
15	3 8 9	xpcbas	⊢ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) = ( Base ‘ 𝑇 )
16		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
17	3 15 10 11 16	xpchomfval	⊢ ( Hom ‘ 𝑇 ) = ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) )
18	17	a1i	⊢ ( 𝜑 → ( Hom ‘ 𝑇 ) = ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ) )
19		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) )
20	3 8 9 10 11 12 13 6 7 14 18 19	xpcval	⊢ ( 𝜑 → 𝑇 = { ⟨ ( Base ‘ ndx ) , ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( Hom ‘ 𝑇 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } )
21		baseid	⊢ Base = Slot ( Base ‘ ndx )
22	4 5	wunndx	⊢ ( 𝜑 → ndx ∈ 𝑈 )
23	21 4 22	wunstr	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )
24	1 2 4 6	catcbaselcl	⊢ ( 𝜑 → ( Base ‘ 𝑋 ) ∈ 𝑈 )
25	1 2 4 7	catcbaselcl	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) ∈ 𝑈 )
26	4 24 25	wunxp	⊢ ( 𝜑 → ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ∈ 𝑈 )
27	4 23 26	wunop	⊢ ( 𝜑 → ⟨ ( Base ‘ ndx ) , ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ⟩ ∈ 𝑈 )
28		homid	⊢ Hom = Slot ( Hom ‘ ndx )
29	28 4 22	wunstr	⊢ ( 𝜑 → ( Hom ‘ ndx ) ∈ 𝑈 )
30	4 26 26	wunxp	⊢ ( 𝜑 → ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ∈ 𝑈 )
31	1 2 4 6	catchomcl	⊢ ( 𝜑 → ( Hom ‘ 𝑋 ) ∈ 𝑈 )
32	4 31	wunrn	⊢ ( 𝜑 → ran ( Hom ‘ 𝑋 ) ∈ 𝑈 )
33	4 32	wununi	⊢ ( 𝜑 → ∪ ran ( Hom ‘ 𝑋 ) ∈ 𝑈 )
34	1 2 4 7	catchomcl	⊢ ( 𝜑 → ( Hom ‘ 𝑌 ) ∈ 𝑈 )
35	4 34	wunrn	⊢ ( 𝜑 → ran ( Hom ‘ 𝑌 ) ∈ 𝑈 )
36	4 35	wununi	⊢ ( 𝜑 → ∪ ran ( Hom ‘ 𝑌 ) ∈ 𝑈 )
37	4 33 36	wunxp	⊢ ( 𝜑 → ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) ∈ 𝑈 )
38	4 37	wunpw	⊢ ( 𝜑 → 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) ∈ 𝑈 )
39		ovssunirn	⊢ ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) ⊆ ∪ ran ( Hom ‘ 𝑋 )
40		ovssunirn	⊢ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ⊆ ∪ ran ( Hom ‘ 𝑌 )
41		xpss12	⊢ ( ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) ⊆ ∪ ran ( Hom ‘ 𝑋 ) ∧ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ⊆ ∪ ran ( Hom ‘ 𝑌 ) ) → ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ⊆ ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) )
42	39 40 41	mp2an	⊢ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ⊆ ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) )
43		ovex	⊢ ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) ∈ V
44		ovex	⊢ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ∈ V
45	43 44	xpex	⊢ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ∈ V
46	45	elpw	⊢ ( ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) ↔ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ⊆ ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) )
47	42 46	mpbir	⊢ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) )
48	47	rgen2w	⊢ ∀ 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) )
49		eqid	⊢ ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) )
50	49	fmpo	⊢ ( ∀ 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) ↔ ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) )
51	48 50	mpbi	⊢ ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) )
52	51	a1i	⊢ ( 𝜑 → ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) )
53	4 30 38 52	wunf	⊢ ( 𝜑 → ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ) ∈ 𝑈 )
54	17 53	eqeltrid	⊢ ( 𝜑 → ( Hom ‘ 𝑇 ) ∈ 𝑈 )
55	4 29 54	wunop	⊢ ( 𝜑 → ⟨ ( Hom ‘ ndx ) , ( Hom ‘ 𝑇 ) ⟩ ∈ 𝑈 )
56		ccoid	⊢ comp = Slot ( comp ‘ ndx )
57	56 4 22	wunstr	⊢ ( 𝜑 → ( comp ‘ ndx ) ∈ 𝑈 )
58	4 30 26	wunxp	⊢ ( 𝜑 → ( ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ∈ 𝑈 )
59	1 2 4 6	catcccocl	⊢ ( 𝜑 → ( comp ‘ 𝑋 ) ∈ 𝑈 )
60	4 59	wunrn	⊢ ( 𝜑 → ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
61	4 60	wununi	⊢ ( 𝜑 → ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
62	4 61	wunrn	⊢ ( 𝜑 → ran ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
63	4 62	wununi	⊢ ( 𝜑 → ∪ ran ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
64	4 63	wunpw	⊢ ( 𝜑 → 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
65	1 2 4 7	catcccocl	⊢ ( 𝜑 → ( comp ‘ 𝑌 ) ∈ 𝑈 )
66	4 65	wunrn	⊢ ( 𝜑 → ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
67	4 66	wununi	⊢ ( 𝜑 → ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
68	4 67	wunrn	⊢ ( 𝜑 → ran ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
69	4 68	wununi	⊢ ( 𝜑 → ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
70	4 69	wunpw	⊢ ( 𝜑 → 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
71	4 64 70	wunxp	⊢ ( 𝜑 → ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ∈ 𝑈 )
72	4 54	wunrn	⊢ ( 𝜑 → ran ( Hom ‘ 𝑇 ) ∈ 𝑈 )
73	4 72	wununi	⊢ ( 𝜑 → ∪ ran ( Hom ‘ 𝑇 ) ∈ 𝑈 )
74	4 73 73	wunxp	⊢ ( 𝜑 → ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ∈ 𝑈 )
75	4 71 74	wunpm	⊢ ( 𝜑 → ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↑_pm ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ) ∈ 𝑈 )
76		fvex	⊢ ( comp ‘ 𝑋 ) ∈ V
77	76	rnex	⊢ ran ( comp ‘ 𝑋 ) ∈ V
78	77	uniex	⊢ ∪ ran ( comp ‘ 𝑋 ) ∈ V
79	78	rnex	⊢ ran ∪ ran ( comp ‘ 𝑋 ) ∈ V
80	79	uniex	⊢ ∪ ran ∪ ran ( comp ‘ 𝑋 ) ∈ V
81	80	pwex	⊢ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) ∈ V
82		fvex	⊢ ( comp ‘ 𝑌 ) ∈ V
83	82	rnex	⊢ ran ( comp ‘ 𝑌 ) ∈ V
84	83	uniex	⊢ ∪ ran ( comp ‘ 𝑌 ) ∈ V
85	84	rnex	⊢ ran ∪ ran ( comp ‘ 𝑌 ) ∈ V
86	85	uniex	⊢ ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ V
87	86	pwex	⊢ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ V
88	81 87	xpex	⊢ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ∈ V
89		fvex	⊢ ( Hom ‘ 𝑇 ) ∈ V
90	89	rnex	⊢ ran ( Hom ‘ 𝑇 ) ∈ V
91	90	uniex	⊢ ∪ ran ( Hom ‘ 𝑇 ) ∈ V
92	91 91	xpex	⊢ ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ∈ V
93		ovssunirn	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ⊆ ∪ ran ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) )
94		ovssunirn	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ⊆ ∪ ran ( comp ‘ 𝑋 )
95		rnss	⊢ ( ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ⊆ ∪ ran ( comp ‘ 𝑋 ) → ran ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ⊆ ran ∪ ran ( comp ‘ 𝑋 ) )
96		uniss	⊢ ( ran ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ⊆ ran ∪ ran ( comp ‘ 𝑋 ) → ∪ ran ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑋 ) )
97	94 95 96	mp2b	⊢ ∪ ran ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑋 )
98	93 97	sstri	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑋 )
99		ovex	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ∈ V
100	99	elpw	⊢ ( ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) ↔ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑋 ) )
101	98 100	mpbir	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 )
102		ovssunirn	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⊆ ∪ ran ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) )
103		ovssunirn	⊢ ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ⊆ ∪ ran ( comp ‘ 𝑌 )
104		rnss	⊢ ( ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ⊆ ∪ ran ( comp ‘ 𝑌 ) → ran ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ⊆ ran ∪ ran ( comp ‘ 𝑌 ) )
105		uniss	⊢ ( ran ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ⊆ ran ∪ ran ( comp ‘ 𝑌 ) → ∪ ran ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 ) )
106	103 104 105	mp2b	⊢ ∪ ran ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 )
107	102 106	sstri	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 )
108		ovex	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ∈ V
109	108	elpw	⊢ ( ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↔ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 ) )
110	107 109	mpbir	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 )
111		opelxpi	⊢ ( ( ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) ∧ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) → ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) )
112	101 110 111	mp2an	⊢ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) )
113	112	rgen2w	⊢ ∀ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ∀ 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) )
114		eqid	⊢ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
115	114	fmpo	⊢ ( ∀ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ∀ 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↔ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) : ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⟶ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) )
116	113 115	mpbi	⊢ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) : ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⟶ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) )
117		ovssunirn	⊢ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ⊆ ∪ ran ( Hom ‘ 𝑇 )
118		fvssunirn	⊢ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⊆ ∪ ran ( Hom ‘ 𝑇 )
119		xpss12	⊢ ( ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ⊆ ∪ ran ( Hom ‘ 𝑇 ) ∧ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⊆ ∪ ran ( Hom ‘ 𝑇 ) ) → ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⊆ ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) )
120	117 118 119	mp2an	⊢ ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⊆ ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) )
121		elpm2r	⊢ ( ( ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ∈ V ∧ ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ∈ V ) ∧ ( ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) : ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⟶ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ∧ ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⊆ ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ) ) → ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↑_pm ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ) )
122	88 92 116 120 121	mp4an	⊢ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↑_pm ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) )
123	122	rgen2w	⊢ ∀ 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↑_pm ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) )
124		eqid	⊢ ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
125	124	fmpo	⊢ ( ∀ 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↑_pm ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ) ↔ ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) : ( ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↑_pm ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ) )
126	123 125	mpbi	⊢ ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) : ( ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↑_pm ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) )
127	126	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) : ( ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↑_pm ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ) )
128	4 58 75 127	wunf	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ∈ 𝑈 )
129	4 57 128	wunop	⊢ ( 𝜑 → ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ ∈ 𝑈 )
130	4 27 55 129	wuntp	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( Hom ‘ 𝑇 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } ∈ 𝑈 )
131	20 130	eqeltrd	⊢ ( 𝜑 → 𝑇 ∈ 𝑈 )
132	1 2 4	catcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
133	6 132	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Cat ) )
134	133	elin2d	⊢ ( 𝜑 → 𝑋 ∈ Cat )
135	7 132	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑈 ∩ Cat ) )
136	135	elin2d	⊢ ( 𝜑 → 𝑌 ∈ Cat )
137	3 134 136	xpccat	⊢ ( 𝜑 → 𝑇 ∈ Cat )
138	131 137	elind	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑈 ∩ Cat ) )
139	138 132	eleqtrrd	⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )

Metamath Proof Explorer

Theorem catcxpccl

Proof