natfval

Description: Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

	Ref	Expression
Hypotheses	natfval.1	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	natfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	natfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	natfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	natfval.o	⊢ · = ( comp ‘ 𝐷 )
Assertion	natfval	⊢ 𝑁 = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		natfval.1	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2		natfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		natfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		natfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
5		natfval.o	⊢ · = ( comp ‘ 𝐷 )
6		oveq12	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( 𝑡 Func 𝑢 ) = ( 𝐶 Func 𝐷 ) )
7		simpl	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → 𝑡 = 𝐶 )
8	7	fveq2d	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( Base ‘ 𝑡 ) = ( Base ‘ 𝐶 ) )
9	8 2	eqtr4di	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( Base ‘ 𝑡 ) = 𝐵 )
10	9	ixpeq1d	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) )
11		simpr	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → 𝑢 = 𝐷 )
12	11	fveq2d	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( Hom ‘ 𝑢 ) = ( Hom ‘ 𝐷 ) )
13	12 4	eqtr4di	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( Hom ‘ 𝑢 ) = 𝐽 )
14	13	oveqd	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) = ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) )
15	14	ixpeq2dv	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) )
16	10 15	eqtrd	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) )
17	7	fveq2d	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( Hom ‘ 𝑡 ) = ( Hom ‘ 𝐶 ) )
18	17 3	eqtr4di	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( Hom ‘ 𝑡 ) = 𝐻 )
19	18	oveqd	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
20	11	fveq2d	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( comp ‘ 𝑢 ) = ( comp ‘ 𝐷 ) )
21	20 5	eqtr4di	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( comp ‘ 𝑢 ) = · )
22	21	oveqd	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) = ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) )
23	22	oveqd	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) )
24	21	oveqd	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) = ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) )
25	24	oveqd	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) )
26	23 25	eqeq12d	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
27	19 26	raleqbidv	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
28	9 27	raleqbidv	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
29	9 28	raleqbidv	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
30	16 29	rabeqbidv	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
31	30	csbeq2dv	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
32	31	csbeq2dv	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
33	6 6 32	mpoeq123dv	⊢ ( ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) → ( 𝑓 ∈ ( 𝑡 Func 𝑢 ) , 𝑔 ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )
34		df-nat	⊢ Nat = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ ( 𝑓 ∈ ( 𝑡 Func 𝑢 ) , 𝑔 ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )
35		ovex	⊢ ( 𝐶 Func 𝐷 ) ∈ V
36	35 35	mpoex	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) ∈ V
37	33 34 36	ovmpoa	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Nat 𝐷 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )
38	34	mpondm0	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Nat 𝐷 ) = ∅ )
39		funcrcl	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
40	39	con3i	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ¬ 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
41	40	eq0rdv	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Func 𝐷 ) = ∅ )
42	41	olcd	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( ( 𝐶 Func 𝐷 ) = ∅ ∨ ( 𝐶 Func 𝐷 ) = ∅ ) )
43		0mpo0	⊢ ( ( ( 𝐶 Func 𝐷 ) = ∅ ∨ ( 𝐶 Func 𝐷 ) = ∅ ) → ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) = ∅ )
44	42 43	syl	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) = ∅ )
45	38 44	eqtr4d	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Nat 𝐷 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )
46	37 45	pm2.61i	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
47	1 46	eqtri	⊢ 𝑁 = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )

Metamath Proof Explorer

Theorem natfval

Proof