Metamath Proof Explorer


Theorem 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 ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) )
18 17 a1i ( 𝜑 → ( Hom ‘ 𝑇 ) = ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ) )
19 eqidd ( 𝜑 → ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) )
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 ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } )
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 ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) ⊆ ran ( Hom ‘ 𝑋 )
40 ovssunirn ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ⊆ ran ( Hom ‘ 𝑌 )
41 xpss12 ( ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) ⊆ ran ( Hom ‘ 𝑋 ) ∧ ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ⊆ ran ( Hom ‘ 𝑌 ) ) → ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ⊆ ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) ) )
42 39 40 41 mp2an ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ⊆ ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) )
43 ovex ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) ∈ V
44 ovex ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ∈ V
45 43 44 xpex ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ∈ V
46 45 elpw ( ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ∈ 𝒫 ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) ) ↔ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ⊆ ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) ) )
47 42 46 mpbir ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ∈ 𝒫 ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) )
48 47 rgen2w 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ∈ 𝒫 ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) )
49 eqid ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) )
50 49 fmpo ( ∀ 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ∈ 𝒫 ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) ) ↔ ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ 𝒫 ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) ) )
51 48 50 mpbi ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ 𝒫 ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) )
52 51 a1i ( 𝜑 → ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ⟶ 𝒫 ( ran ( Hom ‘ 𝑋 ) × ran ( Hom ‘ 𝑌 ) ) )
53 4 30 38 52 wunf ( 𝜑 → ( 𝑢 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑋 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑌 ) ( 2nd𝑣 ) ) ) ) ∈ 𝑈 )
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 ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) ⊆ ran ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) )
94 ovssunirn ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ⊆ ran ( comp ‘ 𝑋 )
95 rnss ( ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ⊆ ran ( comp ‘ 𝑋 ) → ran ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ⊆ ran ran ( comp ‘ 𝑋 ) )
96 uniss ( ran ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ⊆ ran ran ( comp ‘ 𝑋 ) → ran ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ⊆ ran ran ( comp ‘ 𝑋 ) )
97 94 95 96 mp2b ran ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ⊆ ran ran ( comp ‘ 𝑋 )
98 93 97 sstri ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) ⊆ ran ran ( comp ‘ 𝑋 )
99 ovex ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) ∈ V
100 99 elpw ( ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) ∈ 𝒫 ran ran ( comp ‘ 𝑋 ) ↔ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) ⊆ ran ran ( comp ‘ 𝑋 ) )
101 98 100 mpbir ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) ∈ 𝒫 ran ran ( comp ‘ 𝑋 )
102 ovssunirn ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⊆ ran ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) )
103 ovssunirn ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ⊆ ran ( comp ‘ 𝑌 )
104 rnss ( ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ⊆ ran ( comp ‘ 𝑌 ) → ran ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ⊆ ran ran ( comp ‘ 𝑌 ) )
105 uniss ( ran ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ⊆ ran ran ( comp ‘ 𝑌 ) → ran ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ⊆ ran ran ( comp ‘ 𝑌 ) )
106 103 104 105 mp2b ran ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ⊆ ran ran ( comp ‘ 𝑌 )
107 102 106 sstri ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⊆ ran ran ( comp ‘ 𝑌 )
108 ovex ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ∈ V
109 108 elpw ( ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ∈ 𝒫 ran ran ( comp ‘ 𝑌 ) ↔ ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⊆ ran ran ( comp ‘ 𝑌 ) )
110 107 109 mpbir ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ∈ 𝒫 ran ran ( comp ‘ 𝑌 )
111 opelxpi ( ( ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) ∈ 𝒫 ran ran ( comp ‘ 𝑋 ) ∧ ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ∈ 𝒫 ran ran ( comp ‘ 𝑌 ) ) → ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ∈ ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) ) )
112 101 110 111 mp2an ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ∈ ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) )
113 112 rgen2w 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ∀ 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ∈ ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) )
114 eqid ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) = ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ )
115 114 fmpo ( ∀ 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ∀ 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ∈ ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) ) ↔ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) : ( ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⟶ ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) ) )
116 113 115 mpbi ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) : ( ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⟶ ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) )
117 ovssunirn ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ⊆ ran ( Hom ‘ 𝑇 )
118 fvssunirn ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⊆ ran ( Hom ‘ 𝑇 )
119 xpss12 ( ( ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) ⊆ ran ( Hom ‘ 𝑇 ) ∧ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ⊆ ran ( Hom ‘ 𝑇 ) ) → ( ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⊆ ( ran ( Hom ‘ 𝑇 ) × ran ( Hom ‘ 𝑇 ) ) )
120 117 118 119 mp2an ( ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⊆ ( ran ( Hom ‘ 𝑇 ) × ran ( Hom ‘ 𝑇 ) )
121 elpm2r ( ( ( ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) ) ∈ V ∧ ( ran ( Hom ‘ 𝑇 ) × ran ( Hom ‘ 𝑇 ) ) ∈ V ) ∧ ( ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) : ( ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⟶ ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) ) ∧ ( ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) × ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ) ⊆ ( ran ( Hom ‘ 𝑇 ) × ran ( Hom ‘ 𝑇 ) ) ) ) → ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) ) ↑pm ( ran ( Hom ‘ 𝑇 ) × ran ( Hom ‘ 𝑇 ) ) ) )
122 88 92 116 120 121 mp4an ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) ) ↑pm ( ran ( Hom ‘ 𝑇 ) × ran ( Hom ‘ 𝑇 ) ) )
123 122 rgen2w 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) ) ↑pm ( ran ( Hom ‘ 𝑇 ) × ran ( Hom ‘ 𝑇 ) ) )
124 eqid ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) )
125 124 fmpo ( ∀ 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑋 ) × 𝒫 ran ran ( comp ‘ 𝑌 ) ) ↑pm ( ran ( Hom ‘ 𝑇 ) × ran ( Hom ‘ 𝑇 ) ) ) ↔ ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) : ( ( ( ( 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 ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) : ( ( ( ( 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 ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) : ( ( ( ( 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 ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ∈ 𝑈 )
129 4 57 128 wunop ( 𝜑 → ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ ∈ 𝑈 )
130 4 27 55 129 wuntp ( 𝜑 → { ⟨ ( Base ‘ ndx ) , ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( Hom ‘ 𝑇 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) × ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( Hom ‘ 𝑇 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑇 ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑌 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } ∈ 𝑈 )
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 ( 𝜑𝑇𝐵 )