Metamath Proof Explorer

Theorem wunnat

Description: A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses wunnat.1 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
wunnat.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
wunnat.3 ⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
Assertion wunnat ( 𝜑 → ( 𝐶 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 𝐷 ) ∈ 𝑈 )