Metamath Proof Explorer


Theorem wunnatOLD

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

Ref Expression
Hypotheses wunnat.1 ( 𝜑𝑈 ∈ WUni )
wunnat.2 ( 𝜑𝐶𝑈 )
wunnat.3 ( 𝜑𝐷𝑈 )
Assertion wunnatOLD ( 𝜑 → ( 𝐶 Nat 𝐷 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 wunnat.1 ( 𝜑𝑈 ∈ WUni )
2 wunnat.2 ( 𝜑𝐶𝑈 )
3 wunnat.3 ( 𝜑𝐷𝑈 )
4 1 2 3 wunfunc ( 𝜑 → ( 𝐶 Func 𝐷 ) ∈ 𝑈 )
5 1 4 4 wunxp ( 𝜑 → ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) ∈ 𝑈 )
6 df-hom Hom = Slot 1 4
7 6 1 3 wunstr ( 𝜑 → ( Hom ‘ 𝐷 ) ∈ 𝑈 )
8 1 7 wunrn ( 𝜑 → ran ( Hom ‘ 𝐷 ) ∈ 𝑈 )
9 1 8 wununi ( 𝜑 ran ( Hom ‘ 𝐷 ) ∈ 𝑈 )
10 df-base Base = Slot 1
11 10 1 2 wunstr ( 𝜑 → ( Base ‘ 𝐶 ) ∈ 𝑈 )
12 1 9 11 wunmap ( 𝜑 → ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) ∈ 𝑈 )
13 1 12 wunpw ( 𝜑 → 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) ∈ 𝑈 )
14 fvex ( 1st𝑓 ) ∈ V
15 fvex ( 1st𝑔 ) ∈ V
16 ovex ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) ∈ V
17 ssrab2 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ⊆ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) )
18 ovssunirn ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ⊆ ran ( Hom ‘ 𝐷 )
19 18 rgenw 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ⊆ ran ( Hom ‘ 𝐷 )
20 ss2ixp ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ⊆ ran ( Hom ‘ 𝐷 ) → X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ⊆ X 𝑥 ∈ ( Base ‘ 𝐶 ) ran ( Hom ‘ 𝐷 ) )
21 19 20 ax-mp X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ⊆ X 𝑥 ∈ ( Base ‘ 𝐶 ) ran ( Hom ‘ 𝐷 )
22 fvex ( Base ‘ 𝐶 ) ∈ V
23 fvex ( Hom ‘ 𝐷 ) ∈ V
24 23 rnex ran ( Hom ‘ 𝐷 ) ∈ V
25 24 uniex ran ( Hom ‘ 𝐷 ) ∈ V
26 22 25 ixpconst X 𝑥 ∈ ( Base ‘ 𝐶 ) ran ( Hom ‘ 𝐷 ) = ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) )
27 21 26 sseqtri X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ⊆ ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) )
28 17 27 sstri { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ⊆ ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) )
29 16 28 elpwi2 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) )
30 29 sbcth ( ( 1st𝑔 ) ∈ V → [ ( 1st𝑔 ) / 𝑠 ] { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) )
31 sbcel1g ( ( 1st𝑔 ) ∈ V → ( [ ( 1st𝑔 ) / 𝑠 ] { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) ↔ ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) ) )
32 30 31 mpbid ( ( 1st𝑔 ) ∈ V → ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) )
33 15 32 ax-mp ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) )
34 33 sbcth ( ( 1st𝑓 ) ∈ V → [ ( 1st𝑓 ) / 𝑟 ] ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) )
35 sbcel1g ( ( 1st𝑓 ) ∈ V → ( [ ( 1st𝑓 ) / 𝑟 ] ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) ↔ ( 1st𝑓 ) / 𝑟 ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) ) )
36 34 35 mpbid ( ( 1st𝑓 ) ∈ V → ( 1st𝑓 ) / 𝑟 ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) )
37 14 36 ax-mp ( 1st𝑓 ) / 𝑟 ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) )
38 37 rgen2w 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ( 1st𝑓 ) / 𝑟 ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) )
39 eqid ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
40 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
41 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
42 eqid ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
43 eqid ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
44 39 40 41 42 43 natfval ( 𝐶 Nat 𝐷 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1st𝑓 ) / 𝑟 ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } )
45 44 fmpo ( ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ( 1st𝑓 ) / 𝑟 ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) ↔ ( 𝐶 Nat 𝐷 ) : ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) ⟶ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) )
46 38 45 mpbi ( 𝐶 Nat 𝐷 ) : ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) ⟶ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) )
47 46 a1i ( 𝜑 → ( 𝐶 Nat 𝐷 ) : ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) ⟶ 𝒫 ( ran ( Hom ‘ 𝐷 ) ↑m ( Base ‘ 𝐶 ) ) )
48 1 5 13 47 wunf ( 𝜑 → ( 𝐶 Nat 𝐷 ) ∈ 𝑈 )