wunnat

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

	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		homid	⊢ Hom = Slot ( Hom ‘ ndx )
7	6 1 3	wunstr	⊢ ( 𝜑 → ( Hom ‘ 𝐷 ) ∈ 𝑈 )
8	1 7	wunrn	⊢ ( 𝜑 → ran ( Hom ‘ 𝐷 ) ∈ 𝑈 )
9	1 8	wununi	⊢ ( 𝜑 → ∪ ran ( Hom ‘ 𝐷 ) ∈ 𝑈 )
10		baseid	⊢ Base = Slot ( Base ‘ ndx )
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	⊢ ( 1^st ‘ 𝑓 ) ∈ V
15		fvex	⊢ ( 1^st ‘ 𝑔 ) ∈ V
16		ovex	⊢ ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) ∈ V
17		ssrab2	⊢ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( 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 ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ⊆ ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) )
29	16 28	elpwi2	⊢ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) )
30	29	sbcth	⊢ ( ( 1^st ‘ 𝑔 ) ∈ V → [ ( 1^st ‘ 𝑔 ) / 𝑠 ] { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) )
31		sbcel1g	⊢ ( ( 1^st ‘ 𝑔 ) ∈ V → ( [ ( 1^st ‘ 𝑔 ) / 𝑠 ] { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) ↔ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) ) )
32	30 31	mpbid	⊢ ( ( 1^st ‘ 𝑔 ) ∈ V → ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) )
33	15 32	ax-mp	⊢ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) )
34	33	sbcth	⊢ ( ( 1^st ‘ 𝑓 ) ∈ V → [ ( 1^st ‘ 𝑓 ) / 𝑟 ] ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) )
35		sbcel1g	⊢ ( ( 1^st ‘ 𝑓 ) ∈ V → ( [ ( 1^st ‘ 𝑓 ) / 𝑟 ] ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) ↔ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) ) )
36	34 35	mpbid	⊢ ( ( 1^st ‘ 𝑓 ) ∈ V → ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) )
37	14 36	ax-mp	⊢ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ 𝒫 ( ∪ ran ( Hom ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) )
38	37	rgen2w	⊢ ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( 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 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
45	44	fmpo	⊢ ( ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( 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 𝐷 ) ∈ 𝑈 )

Metamath Proof Explorer

Theorem wunnat

Proof