Metamath Proof Explorer


Theorem catcfucclOLD

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

Ref Expression
Hypotheses catcfuccl.c 𝐶 = ( CatCat ‘ 𝑈 )
catcfuccl.b 𝐵 = ( Base ‘ 𝐶 )
catcfuccl.o 𝑄 = ( 𝑋 FuncCat 𝑌 )
catcfuccl.u ( 𝜑𝑈 ∈ WUni )
catcfuccl.1 ( 𝜑 → ω ∈ 𝑈 )
catcfuccl.x ( 𝜑𝑋𝐵 )
catcfuccl.y ( 𝜑𝑌𝐵 )
Assertion catcfucclOLD ( 𝜑𝑄𝐵 )

Proof

Step Hyp Ref Expression
1 catcfuccl.c 𝐶 = ( CatCat ‘ 𝑈 )
2 catcfuccl.b 𝐵 = ( Base ‘ 𝐶 )
3 catcfuccl.o 𝑄 = ( 𝑋 FuncCat 𝑌 )
4 catcfuccl.u ( 𝜑𝑈 ∈ WUni )
5 catcfuccl.1 ( 𝜑 → ω ∈ 𝑈 )
6 catcfuccl.x ( 𝜑𝑋𝐵 )
7 catcfuccl.y ( 𝜑𝑌𝐵 )
8 eqid ( 𝑋 Func 𝑌 ) = ( 𝑋 Func 𝑌 )
9 eqid ( 𝑋 Nat 𝑌 ) = ( 𝑋 Nat 𝑌 )
10 eqid ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
11 eqid ( comp ‘ 𝑌 ) = ( comp ‘ 𝑌 )
12 1 2 4 catcbas ( 𝜑𝐵 = ( 𝑈 ∩ Cat ) )
13 6 12 eleqtrd ( 𝜑𝑋 ∈ ( 𝑈 ∩ Cat ) )
14 13 elin2d ( 𝜑𝑋 ∈ Cat )
15 7 12 eleqtrd ( 𝜑𝑌 ∈ ( 𝑈 ∩ Cat ) )
16 15 elin2d ( 𝜑𝑌 ∈ Cat )
17 eqidd ( 𝜑 → ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) = ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) )
18 3 8 9 10 11 14 16 17 fucval ( 𝜑𝑄 = { ⟨ ( Base ‘ ndx ) , ( 𝑋 Func 𝑌 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑋 Nat 𝑌 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) ⟩ } )
19 df-base Base = Slot 1
20 4 5 wunndx ( 𝜑 → ndx ∈ 𝑈 )
21 19 4 20 wunstr ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )
22 13 elin1d ( 𝜑𝑋𝑈 )
23 15 elin1d ( 𝜑𝑌𝑈 )
24 4 22 23 wunfunc ( 𝜑 → ( 𝑋 Func 𝑌 ) ∈ 𝑈 )
25 4 21 24 wunop ( 𝜑 → ⟨ ( Base ‘ ndx ) , ( 𝑋 Func 𝑌 ) ⟩ ∈ 𝑈 )
26 df-hom Hom = Slot 1 4
27 26 4 20 wunstr ( 𝜑 → ( Hom ‘ ndx ) ∈ 𝑈 )
28 4 22 23 wunnat ( 𝜑 → ( 𝑋 Nat 𝑌 ) ∈ 𝑈 )
29 4 27 28 wunop ( 𝜑 → ⟨ ( Hom ‘ ndx ) , ( 𝑋 Nat 𝑌 ) ⟩ ∈ 𝑈 )
30 df-cco comp = Slot 1 5
31 30 4 20 wunstr ( 𝜑 → ( comp ‘ ndx ) ∈ 𝑈 )
32 4 24 24 wunxp ( 𝜑 → ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) ∈ 𝑈 )
33 4 32 24 wunxp ( 𝜑 → ( ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) × ( 𝑋 Func 𝑌 ) ) ∈ 𝑈 )
34 30 4 23 wunstr ( 𝜑 → ( comp ‘ 𝑌 ) ∈ 𝑈 )
35 4 34 wunrn ( 𝜑 → ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
36 4 35 wununi ( 𝜑 ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
37 4 36 wunrn ( 𝜑 → ran ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
38 4 37 wununi ( 𝜑 ran ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
39 4 38 wunpw ( 𝜑 → 𝒫 ran ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
40 19 4 22 wunstr ( 𝜑 → ( Base ‘ 𝑋 ) ∈ 𝑈 )
41 4 39 40 wunmap ( 𝜑 → ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∈ 𝑈 )
42 4 28 wunrn ( 𝜑 → ran ( 𝑋 Nat 𝑌 ) ∈ 𝑈 )
43 4 42 wununi ( 𝜑 ran ( 𝑋 Nat 𝑌 ) ∈ 𝑈 )
44 4 43 43 wunxp ( 𝜑 → ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ∈ 𝑈 )
45 4 41 44 wunpm ( 𝜑 → ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) ∈ 𝑈 )
46 fvex ( 1st𝑣 ) ∈ V
47 fvex ( 2nd𝑣 ) ∈ V
48 ovex ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∈ V
49 ovex ( 𝑋 Nat 𝑌 ) ∈ V
50 49 rnex ran ( 𝑋 Nat 𝑌 ) ∈ V
51 50 uniex ran ( 𝑋 Nat 𝑌 ) ∈ V
52 51 51 xpex ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ∈ V
53 eqid ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) )
54 ovssunirn ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ⊆ ran ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) )
55 ovssunirn ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ⊆ ran ( comp ‘ 𝑌 )
56 rnss ( ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ⊆ ran ( comp ‘ 𝑌 ) → ran ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ⊆ ran ran ( comp ‘ 𝑌 ) )
57 uniss ( ran ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ⊆ ran ran ( comp ‘ 𝑌 ) → ran ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ⊆ ran ran ( comp ‘ 𝑌 ) )
58 55 56 57 mp2b ran ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ⊆ ran ran ( comp ‘ 𝑌 )
59 54 58 sstri ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ⊆ ran ran ( comp ‘ 𝑌 )
60 ovex ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ∈ V
61 60 elpw ( ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ∈ 𝒫 ran ran ( comp ‘ 𝑌 ) ↔ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ⊆ ran ran ( comp ‘ 𝑌 ) )
62 59 61 mpbir ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ∈ 𝒫 ran ran ( comp ‘ 𝑌 )
63 62 a1i ( 𝑥 ∈ ( Base ‘ 𝑋 ) → ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ∈ 𝒫 ran ran ( comp ‘ 𝑌 ) )
64 53 63 fmpti ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) : ( Base ‘ 𝑋 ) ⟶ 𝒫 ran ran ( comp ‘ 𝑌 )
65 fvex ( comp ‘ 𝑌 ) ∈ V
66 65 rnex ran ( comp ‘ 𝑌 ) ∈ V
67 66 uniex ran ( comp ‘ 𝑌 ) ∈ V
68 67 rnex ran ran ( comp ‘ 𝑌 ) ∈ V
69 68 uniex ran ran ( comp ‘ 𝑌 ) ∈ V
70 69 pwex 𝒫 ran ran ( comp ‘ 𝑌 ) ∈ V
71 fvex ( Base ‘ 𝑋 ) ∈ V
72 70 71 elmap ( ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ∈ ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) : ( Base ‘ 𝑋 ) ⟶ 𝒫 ran ran ( comp ‘ 𝑌 ) )
73 64 72 mpbir ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ∈ ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) )
74 73 rgen2w 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) ∀ 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ∈ ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) )
75 eqid ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) )
76 75 fmpo ( ∀ 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) ∀ 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ∈ ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↔ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) : ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⟶ ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
77 74 76 mpbi ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) : ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⟶ ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) )
78 ovssunirn ( 𝑔 ( 𝑋 Nat 𝑌 ) ) ⊆ ran ( 𝑋 Nat 𝑌 )
79 ovssunirn ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ⊆ ran ( 𝑋 Nat 𝑌 )
80 xpss12 ( ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ) ⊆ ran ( 𝑋 Nat 𝑌 ) ∧ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ⊆ ran ( 𝑋 Nat 𝑌 ) ) → ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⊆ ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) )
81 78 79 80 mp2an ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⊆ ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) )
82 elpm2r ( ( ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∈ V ∧ ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ∈ V ) ∧ ( ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) : ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⟶ ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⊆ ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) ) → ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) )
83 48 52 77 81 82 mp4an ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) )
84 83 sbcth ( ( 2nd𝑣 ) ∈ V → [ ( 2nd𝑣 ) / 𝑔 ] ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) )
85 sbcel1g ( ( 2nd𝑣 ) ∈ V → ( [ ( 2nd𝑣 ) / 𝑔 ] ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) ↔ ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) ) )
86 84 85 mpbid ( ( 2nd𝑣 ) ∈ V → ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) )
87 47 86 ax-mp ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) )
88 87 sbcth ( ( 1st𝑣 ) ∈ V → [ ( 1st𝑣 ) / 𝑓 ] ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) )
89 sbcel1g ( ( 1st𝑣 ) ∈ V → ( [ ( 1st𝑣 ) / 𝑓 ] ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) ↔ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) ) )
90 88 89 mpbid ( ( 1st𝑣 ) ∈ V → ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) )
91 46 90 ax-mp ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) )
92 91 rgen2w 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) ∀ ∈ ( 𝑋 Func 𝑌 ) ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) )
93 eqid ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) = ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) )
94 93 fmpo ( ∀ 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) ∀ ∈ ( 𝑋 Func 𝑌 ) ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) ↔ ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) : ( ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) × ( 𝑋 Func 𝑌 ) ) ⟶ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) )
95 92 94 mpbi ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) : ( ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) × ( 𝑋 Func 𝑌 ) ) ⟶ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) )
96 95 a1i ( 𝜑 → ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) : ( ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) × ( 𝑋 Func 𝑌 ) ) ⟶ ( ( 𝒫 ran ran ( comp ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↑pm ( ran ( 𝑋 Nat 𝑌 ) × ran ( 𝑋 Nat 𝑌 ) ) ) )
97 4 33 45 96 wunf ( 𝜑 → ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) ∈ 𝑈 )
98 4 31 97 wunop ( 𝜑 → ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) ⟩ ∈ 𝑈 )
99 4 25 29 98 wuntp ( 𝜑 → { ⟨ ( Base ‘ ndx ) , ( 𝑋 Func 𝑌 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑋 Nat 𝑌 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ∈ ( 𝑋 Func 𝑌 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) ⟩ } ∈ 𝑈 )
100 18 99 eqeltrd ( 𝜑𝑄𝑈 )
101 3 14 16 fuccat ( 𝜑𝑄 ∈ Cat )
102 100 101 elind ( 𝜑𝑄 ∈ ( 𝑈 ∩ Cat ) )
103 102 12 eleqtrrd ( 𝜑𝑄𝐵 )