Metamath Proof Explorer

Theorem lanup

Description: The universal property of the left Kan extension; expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses lanup.s ⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
lanup.m ⊢ 𝑀 = ( 𝐷 Nat 𝐸 )
lanup.n ⊢ 𝑁 = ( 𝐶 Nat 𝐸 )
lanup.x ⊢ ∙ = ( comp ‘ 𝑆 )
lanup.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
lanup.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐷 Func 𝐸 ) )
lanup.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝑁 ( 𝐿 ∘func 𝐹 ) ) )
Assertion lanup ( 𝜑 → ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 ↔ ∀ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ∃! 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) 𝑎 = ( ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ( ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ ( 𝑙 ∘func 𝐹 ) ) 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 lanup.s ⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
2 lanup.m ⊢ 𝑀 = ( 𝐷 Nat 𝐸 )
3 lanup.n ⊢ 𝑁 = ( 𝐶 Nat 𝐸 )
4 lanup.x ⊢ ∙ = ( comp ‘ 𝑆 )
5 lanup.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
6 lanup.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐷 Func 𝐸 ) )
7 lanup.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝑁 ( 𝐿 ∘func 𝐹 ) ) )
8 eqid ⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
9 8 fucbas ⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
10 1 fucbas ⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ 𝑆 )
11 8 2 fuchom ⊢ 𝑀 = ( Hom ‘ ( 𝐷 FuncCat 𝐸 ) )
12 1 3 fuchom ⊢ 𝑁 = ( Hom ‘ 𝑆 )
13 3 natrcl ⊢ ( 𝐴 ∈ ( 𝑋 𝑁 ( 𝐿 ∘func 𝐹 ) ) → ( 𝑋 ∈ ( 𝐶 Func 𝐸 ) ∧ ( 𝐿 ∘func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) ) )
14 7 13 syl ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐶 Func 𝐸 ) ∧ ( 𝐿 ∘func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) ) )
15 14 simpld ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
16 15 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝑋 ) ( 𝐶 Func 𝐸 ) ( 2nd ‘ 𝑋 ) )
17 16 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
18 8 17 1 5 prcoffunca ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( ( 𝐷 FuncCat 𝐸 ) Func 𝑆 ) )
19 18 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ( ( 𝐷 FuncCat 𝐸 ) Func 𝑆 ) ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
20 eqidd ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
21 6 20 prcof1 ⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) = ( 𝐿 ∘func 𝐹 ) )
22 21 oveq2d ⊢ ( 𝜑 → ( 𝑋 𝑁 ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ) = ( 𝑋 𝑁 ( 𝐿 ∘func 𝐹 ) ) )
23 7 22 eleqtrrd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝑁 ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ) )
24 9 10 11 12 4 15 19 6 23 isup ⊢ ( 𝜑 → ( 𝐿 ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( ( 𝐷 FuncCat 𝐸 ) UP 𝑆 ) 𝑋 ) 𝐴 ↔ ∀ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑎 ∈ ( 𝑋 𝑁 ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) ∃! 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) 𝑎 = ( ( ( 𝐿 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝑙 ) ‘ 𝑏 ) ( ⟨ 𝑋 , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) 𝐴 ) ) )
25 eqidd ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) )
26 8 1 5 15 25 lanval ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP 𝑆 ) 𝑋 ) )
27 26 breqd ⊢ ( 𝜑 → ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 ↔ 𝐿 ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP 𝑆 ) 𝑋 ) 𝐴 ) )
28 18 up1st2ndb ⊢ ( 𝜑 → ( 𝐿 ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP 𝑆 ) 𝑋 ) 𝐴 ↔ 𝐿 ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( ( 𝐷 FuncCat 𝐸 ) UP 𝑆 ) 𝑋 ) 𝐴 ) )
29 27 28 bitrd ⊢ ( 𝜑 → ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 ↔ 𝐿 ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( ( 𝐷 FuncCat 𝐸 ) UP 𝑆 ) 𝑋 ) 𝐴 ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → 𝑙 ∈ ( 𝐷 Func 𝐸 ) )
31 eqidd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
32 30 31 prcof1 ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) = ( 𝑙 ∘func 𝐹 ) )
33 32 eqcomd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( 𝑙 ∘func 𝐹 ) = ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) )
34 33 oveq2d ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) = ( 𝑋 𝑁 ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) )
35 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) = ( 𝐿 ∘func 𝐹 ) )
36 35 opeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → ⟨ 𝑋 , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ = ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ )
37 32 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) = ( 𝑙 ∘func 𝐹 ) )
38 36 37 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → ( ⟨ 𝑋 , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) = ( ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ ( 𝑙 ∘func 𝐹 ) ) )
39 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) )
40 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
41 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
42 2 39 40 41 prcof21a ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → ( ( 𝐿 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝑙 ) ‘ 𝑏 ) = ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) )
43 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → 𝐴 = 𝐴 )
44 38 42 43 oveq123d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → ( ( ( 𝐿 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝑙 ) ‘ 𝑏 ) ( ⟨ 𝑋 , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) 𝐴 ) = ( ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ( ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ ( 𝑙 ∘func 𝐹 ) ) 𝐴 ) )
45 44 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → ( ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ( ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ ( 𝑙 ∘func 𝐹 ) ) 𝐴 ) = ( ( ( 𝐿 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝑙 ) ‘ 𝑏 ) ( ⟨ 𝑋 , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) 𝐴 ) )
46 45 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) ∧ 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) ) → ( 𝑎 = ( ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ( ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ ( 𝑙 ∘func 𝐹 ) ) 𝐴 ) ↔ 𝑎 = ( ( ( 𝐿 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝑙 ) ‘ 𝑏 ) ( ⟨ 𝑋 , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) 𝐴 ) ) )
47 46 reubidva ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ) → ( ∃! 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) 𝑎 = ( ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ( ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ ( 𝑙 ∘func 𝐹 ) ) 𝐴 ) ↔ ∃! 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) 𝑎 = ( ( ( 𝐿 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝑙 ) ‘ 𝑏 ) ( ⟨ 𝑋 , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) 𝐴 ) ) )
48 34 47 raleqbidva ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( ∀ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ∃! 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) 𝑎 = ( ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ( ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ ( 𝑙 ∘func 𝐹 ) ) 𝐴 ) ↔ ∀ 𝑎 ∈ ( 𝑋 𝑁 ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) ∃! 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) 𝑎 = ( ( ( 𝐿 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝑙 ) ‘ 𝑏 ) ( ⟨ 𝑋 , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) 𝐴 ) ) )
49 48 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ∃! 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) 𝑎 = ( ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ( ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ ( 𝑙 ∘func 𝐹 ) ) 𝐴 ) ↔ ∀ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑎 ∈ ( 𝑋 𝑁 ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) ∃! 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) 𝑎 = ( ( ( 𝐿 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝑙 ) ‘ 𝑏 ) ( ⟨ 𝑋 , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) ) 𝐴 ) ) )
50 24 29 49 3bitr4d ⊢ ( 𝜑 → ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 ↔ ∀ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑎 ∈ ( 𝑋 𝑁 ( 𝑙 ∘func 𝐹 ) ) ∃! 𝑏 ∈ ( 𝐿 𝑀 𝑙 ) 𝑎 = ( ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ( ⟨ 𝑋 , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ ( 𝑙 ∘func 𝐹 ) ) 𝐴 ) ) )