lanfval

Description: Value of the function generating the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025)

	Ref	Expression
Hypotheses	lanfval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	lanfval.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
	lanfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	lanfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	lanfval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
Assertion	lanfval	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lanfval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2		lanfval.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
3		lanfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
4		lanfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
5		lanfval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
6		df-lan	⊢ Lan = ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( ⟨ 𝑑 , 𝑒 ⟩ −∘_F 𝑓 ) ( ( 𝑑 FuncCat 𝑒 ) UP ( 𝑐 FuncCat 𝑒 ) ) 𝑥 ) ) )
7	6	a1i	⊢ ( 𝜑 → Lan = ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( ⟨ 𝑑 , 𝑒 ⟩ −∘_F 𝑓 ) ( ( 𝑑 FuncCat 𝑒 ) UP ( 𝑐 FuncCat 𝑒 ) ) 𝑥 ) ) ) )
8		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ( 1^st ‘ 𝑝 ) ∈ V )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ )
10	9	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ( 1^st ‘ 𝑝 ) = ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
11		op1stg	⊢ ( ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
12	3 4 11	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
13	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
14	10 13	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ( 1^st ‘ 𝑝 ) = 𝐶 )
15		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑝 ) ∈ V )
16		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ )
17	16	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑝 ) = ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
18		op2ndg	⊢ ( ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
19	3 4 18	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
20	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
21	17 20	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑝 ) = 𝐷 )
22		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 )
23		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
24	22 23	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑐 Func 𝑑 ) = ( 𝐶 Func 𝐷 ) )
25		simpllr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) )
26	25	simprd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑒 = 𝐸 )
27	22 26	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑐 Func 𝑒 ) = ( 𝐶 Func 𝐸 ) )
28	23 26	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑑 FuncCat 𝑒 ) = ( 𝐷 FuncCat 𝐸 ) )
29	28 1	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑑 FuncCat 𝑒 ) = 𝑅 )
30	22 26	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑐 FuncCat 𝑒 ) = ( 𝐶 FuncCat 𝐸 ) )
31	30 2	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑐 FuncCat 𝑒 ) = 𝑆 )
32	29 31	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑑 FuncCat 𝑒 ) UP ( 𝑐 FuncCat 𝑒 ) ) = ( 𝑅 UP 𝑆 ) )
33	23 26	opeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ⟨ 𝑑 , 𝑒 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ )
34	33	oveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ⟨ 𝑑 , 𝑒 ⟩ −∘_F 𝑓 ) = ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) )
35		eqidd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑥 = 𝑥 )
36	32 34 35	oveq123d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( ⟨ 𝑑 , 𝑒 ⟩ −∘_F 𝑓 ) ( ( 𝑑 FuncCat 𝑒 ) UP ( 𝑐 FuncCat 𝑒 ) ) 𝑥 ) = ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) )
37	24 27 36	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( ⟨ 𝑑 , 𝑒 ⟩ −∘_F 𝑓 ) ( ( 𝑑 FuncCat 𝑒 ) UP ( 𝑐 FuncCat 𝑒 ) ) 𝑥 ) ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) ) )
38	15 21 37	csbied2	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ⦋ ( 2^nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( ⟨ 𝑑 , 𝑒 ⟩ −∘_F 𝑓 ) ( ( 𝑑 FuncCat 𝑒 ) UP ( 𝑐 FuncCat 𝑒 ) ) 𝑥 ) ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) ) )
39	8 14 38	csbied2	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ⦋ ( 1^st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( ⟨ 𝑑 , 𝑒 ⟩ −∘_F 𝑓 ) ( ( 𝑑 FuncCat 𝑒 ) UP ( 𝑐 FuncCat 𝑒 ) ) 𝑥 ) ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) ) )
40	3	elexd	⊢ ( 𝜑 → 𝐶 ∈ V )
41	4	elexd	⊢ ( 𝜑 → 𝐷 ∈ V )
42	40 41	opelxpd	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( V × V ) )
43	5	elexd	⊢ ( 𝜑 → 𝐸 ∈ V )
44		ovex	⊢ ( 𝐶 Func 𝐷 ) ∈ V
45		ovex	⊢ ( 𝐶 Func 𝐸 ) ∈ V
46	44 45	mpoex	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) ) ∈ V
47	46	a1i	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) ) ∈ V )
48	7 39 42 43 47	ovmpod	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) ) )

Metamath Proof Explorer

Theorem lanfval

Proof