catcxpcclOLD

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

	Ref	Expression
Hypotheses	catcxpccl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcxpccl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	catcxpccl.o	⊢ 𝑇 = ( 𝑋 ×_c 𝑌 )
	catcxpccl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	catcxpccl.1	⊢ ( 𝜑 → ω ∈ 𝑈 )
	catcxpccl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	catcxpccl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	catcxpcclOLD	⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )

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		df-base	⊢ Base = Slot 1
22	4 5	wunndx	⊢ ( 𝜑 → ndx ∈ 𝑈 )
23	21 4 22	wunstr	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )
24	1 2 4	catcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
25	6 24	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Cat ) )
26	25	elin1d	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
27	21 4 26	wunstr	⊢ ( 𝜑 → ( Base ‘ 𝑋 ) ∈ 𝑈 )
28	7 24	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑈 ∩ Cat ) )
29	28	elin1d	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
30	21 4 29	wunstr	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) ∈ 𝑈 )
31	4 27 30	wunxp	⊢ ( 𝜑 → ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ∈ 𝑈 )
32	4 23 31	wunop	⊢ ( 𝜑 → ⟨ ( Base ‘ ndx ) , ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ⟩ ∈ 𝑈 )
33		df-hom	⊢ Hom = Slot ; 1 4
34	33 4 22	wunstr	⊢ ( 𝜑 → ( Hom ‘ ndx ) ∈ 𝑈 )
35	4 31 31	wunxp	⊢ ( 𝜑 → ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ∈ 𝑈 )
36	33 4 26	wunstr	⊢ ( 𝜑 → ( Hom ‘ 𝑋 ) ∈ 𝑈 )
37	4 36	wunrn	⊢ ( 𝜑 → ran ( Hom ‘ 𝑋 ) ∈ 𝑈 )
38	4 37	wununi	⊢ ( 𝜑 → ∪ ran ( Hom ‘ 𝑋 ) ∈ 𝑈 )
39	33 4 29	wunstr	⊢ ( 𝜑 → ( Hom ‘ 𝑌 ) ∈ 𝑈 )
40	4 39	wunrn	⊢ ( 𝜑 → ran ( Hom ‘ 𝑌 ) ∈ 𝑈 )
41	4 40	wununi	⊢ ( 𝜑 → ∪ ran ( Hom ‘ 𝑌 ) ∈ 𝑈 )
42	4 38 41	wunxp	⊢ ( 𝜑 → ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) ∈ 𝑈 )
43	4 42	wunpw	⊢ ( 𝜑 → 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) ∈ 𝑈 )
44		ovssunirn	⊢ ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) ⊆ ∪ ran ( Hom ‘ 𝑋 )
45		ovssunirn	⊢ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ⊆ ∪ ran ( Hom ‘ 𝑌 )
46		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 ‘ 𝑌 ) ) )
47	44 45 46	mp2an	⊢ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ⊆ ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) )
48		ovex	⊢ ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) ∈ V
49		ovex	⊢ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ∈ V
50	48 49	xpex	⊢ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ∈ V
51	50	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 ‘ 𝑌 ) ) )
52	47 51	mpbir	⊢ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) )
53	52	rgen2w	⊢ ∀ 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) )
54		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 ‘ 𝑣 ) ) ) )
55	54	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 ‘ 𝑌 ) ) )
56	53 55	mpbi	⊢ ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) )
57	56	a1i	⊢ ( 𝜑 → ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ 𝒫 ( ∪ ran ( Hom ‘ 𝑋 ) × ∪ ran ( Hom ‘ 𝑌 ) ) )
58	4 35 43 57	wunf	⊢ ( 𝜑 → ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 2^nd ‘ 𝑣 ) ) ) ) ∈ 𝑈 )
59	17 58	eqeltrid	⊢ ( 𝜑 → ( Hom ‘ 𝑇 ) ∈ 𝑈 )
60	4 34 59	wunop	⊢ ( 𝜑 → ⟨ ( Hom ‘ ndx ) , ( Hom ‘ 𝑇 ) ⟩ ∈ 𝑈 )
61		df-cco	⊢ comp = Slot ; 1 5
62	61 4 22	wunstr	⊢ ( 𝜑 → ( comp ‘ ndx ) ∈ 𝑈 )
63	4 35 31	wunxp	⊢ ( 𝜑 → ( ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ∈ 𝑈 )
64	61 4 26	wunstr	⊢ ( 𝜑 → ( comp ‘ 𝑋 ) ∈ 𝑈 )
65	4 64	wunrn	⊢ ( 𝜑 → ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
66	4 65	wununi	⊢ ( 𝜑 → ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
67	4 66	wunrn	⊢ ( 𝜑 → ran ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
68	4 67	wununi	⊢ ( 𝜑 → ∪ ran ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
69	4 68	wunpw	⊢ ( 𝜑 → 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
70	61 4 29	wunstr	⊢ ( 𝜑 → ( comp ‘ 𝑌 ) ∈ 𝑈 )
71	4 70	wunrn	⊢ ( 𝜑 → ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
72	4 71	wununi	⊢ ( 𝜑 → ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
73	4 72	wunrn	⊢ ( 𝜑 → ran ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
74	4 73	wununi	⊢ ( 𝜑 → ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
75	4 74	wunpw	⊢ ( 𝜑 → 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
76	4 69 75	wunxp	⊢ ( 𝜑 → ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ∈ 𝑈 )
77	4 59	wunrn	⊢ ( 𝜑 → ran ( Hom ‘ 𝑇 ) ∈ 𝑈 )
78	4 77	wununi	⊢ ( 𝜑 → ∪ ran ( Hom ‘ 𝑇 ) ∈ 𝑈 )
79	4 78 78	wunxp	⊢ ( 𝜑 → ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ∈ 𝑈 )
80	4 76 79	wunpm	⊢ ( 𝜑 → ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ↑_pm ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ) ∈ 𝑈 )
81		fvex	⊢ ( comp ‘ 𝑋 ) ∈ V
82	81	rnex	⊢ ran ( comp ‘ 𝑋 ) ∈ V
83	82	uniex	⊢ ∪ ran ( comp ‘ 𝑋 ) ∈ V
84	83	rnex	⊢ ran ∪ ran ( comp ‘ 𝑋 ) ∈ V
85	84	uniex	⊢ ∪ ran ∪ ran ( comp ‘ 𝑋 ) ∈ V
86	85	pwex	⊢ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) ∈ V
87		fvex	⊢ ( comp ‘ 𝑌 ) ∈ V
88	87	rnex	⊢ ran ( comp ‘ 𝑌 ) ∈ V
89	88	uniex	⊢ ∪ ran ( comp ‘ 𝑌 ) ∈ V
90	89	rnex	⊢ ran ∪ ran ( comp ‘ 𝑌 ) ∈ V
91	90	uniex	⊢ ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ V
92	91	pwex	⊢ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ V
93	86 92	xpex	⊢ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 ) × 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ) ∈ V
94		fvex	⊢ ( Hom ‘ 𝑇 ) ∈ V
95	94	rnex	⊢ ran ( Hom ‘ 𝑇 ) ∈ V
96	95	uniex	⊢ ∪ ran ( Hom ‘ 𝑇 ) ∈ V
97	96 96	xpex	⊢ ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) ∈ V
98		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 ‘ 𝑦 ) )
99		ovssunirn	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ⊆ ∪ ran ( comp ‘ 𝑋 )
100		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 ‘ 𝑋 ) )
101		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 ‘ 𝑋 ) )
102	99 100 101	mp2b	⊢ ∪ ran ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑋 )
103	98 102	sstri	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑋 )
104		ovex	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ∈ V
105	104	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 ‘ 𝑋 ) )
106	103 105	mpbir	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑋 )
107		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 ‘ 𝑦 ) )
108		ovssunirn	⊢ ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ⊆ ∪ ran ( comp ‘ 𝑌 )
109		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 ‘ 𝑌 ) )
110		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 ‘ 𝑌 ) )
111	108 109 110	mp2b	⊢ ∪ ran ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 )
112	107 111	sstri	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 )
113		ovex	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ∈ V
114	113	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 ‘ 𝑌 ) )
115	112 114	mpbir	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 )
116		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 ‘ 𝑌 ) ) )
117	106 115 116	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 ‘ 𝑌 ) )
118	117	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 ‘ 𝑌 ) )
119		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 ‘ 𝑓 ) ) ⟩ )
120	119	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 ‘ 𝑌 ) ) )
121	118 120	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 ‘ 𝑌 ) )
122		ovssunirn	⊢ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ⊆ ∪ ran ( Hom ‘ 𝑇 )
123		fvssunirn	⊢ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⊆ ∪ ran ( Hom ‘ 𝑇 )
124		xpss12	⊢ ( ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ⊆ ∪ ran ( Hom ‘ 𝑇 ) ∧ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⊆ ∪ ran ( Hom ‘ 𝑇 ) ) → ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⊆ ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) ) )
125	122 123 124	mp2an	⊢ ( ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⊆ ( ∪ ran ( Hom ‘ 𝑇 ) × ∪ ran ( Hom ‘ 𝑇 ) )
126		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 ‘ 𝑇 ) ) ) )
127	93 97 121 125 126	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 ‘ 𝑇 ) ) )
128	127	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 ‘ 𝑇 ) ) )
129		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 ‘ 𝑓 ) ) ⟩ ) )
130	129	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 ‘ 𝑇 ) ) ) )
131	128 130	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 ‘ 𝑇 ) ) )
132	131	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 ‘ 𝑇 ) ) ) )
133	4 63 80 132	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 ‘ 𝑓 ) ) ⟩ ) ) ∈ 𝑈 )
134	4 62 133	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 ‘ 𝑓 ) ) ⟩ ) ) ⟩ ∈ 𝑈 )
135	4 32 60 134	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 ‘ 𝑓 ) ) ⟩ ) ) ⟩ } ∈ 𝑈 )
136	20 135	eqeltrd	⊢ ( 𝜑 → 𝑇 ∈ 𝑈 )
137	25	elin2d	⊢ ( 𝜑 → 𝑋 ∈ Cat )
138	28	elin2d	⊢ ( 𝜑 → 𝑌 ∈ Cat )
139	3 137 138	xpccat	⊢ ( 𝜑 → 𝑇 ∈ Cat )
140	136 139	elind	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑈 ∩ Cat ) )
141	140 24	eleqtrrd	⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )

Metamath Proof Explorer

Theorem catcxpcclOLD

Proof