Metamath Proof Explorer

Theorem ranup

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

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

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 ranup.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 simprd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
16 15 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝑋 ) ( 𝐶 Func 𝐸 ) ( 2nd ‘ 𝑋 ) )
17 16 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
18 opex ⊢ ⟨ 𝐷 , 𝐸 ⟩ ∈ V
19 18 a1i ⊢ ( 𝜑 → ⟨ 𝐷 , 𝐸 ⟩ ∈ V )
20 5 19 prcofelvv ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( V × V ) )
21 1st2nd2 ⊢ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( V × V ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )
22 20 21 syl ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )
23 8 17 1 5 22 prcoffunca2 ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ( ( 𝐷 FuncCat 𝐸 ) Func 𝑆 ) ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
24 eqidd ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
25 6 24 prcof1 ⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) = ( 𝐿 ∘func 𝐹 ) )
26 25 oveq1d ⊢ ( 𝜑 → ( ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) 𝑁 𝑋 ) = ( ( 𝐿 ∘func 𝐹 ) 𝑁 𝑋 ) )
27 7 26 eleqtrrd ⊢ ( 𝜑 → 𝐴 ∈ ( ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) 𝑁 𝑋 ) )
28 eqid ⊢ ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
29 eqid ⊢ ( oppCat ‘ 𝑆 ) = ( oppCat ‘ 𝑆 )
30 9 10 11 12 4 15 23 6 27 28 29 oppcup ⊢ ( 𝜑 → ( 𝐿 ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) ) UP ( oppCat ‘ 𝑆 ) ) 𝑋 ) 𝐴 ↔ ∀ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑎 ∈ ( ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) 𝑁 𝑋 ) ∃! 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) 𝑎 = ( 𝐴 ( ⟨ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ 𝑋 ) ( ( 𝑙 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝐿 ) ‘ 𝑏 ) ) ) )
31 1 fveq2i ⊢ ( oppCat ‘ 𝑆 ) = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
32 28 31 22 5 ranval2 ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) = ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) ) UP ( oppCat ‘ 𝑆 ) ) 𝑋 ) )
33 32 breqd ⊢ ( 𝜑 → ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) 𝐴 ↔ 𝐿 ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) ) UP ( oppCat ‘ 𝑆 ) ) 𝑋 ) 𝐴 ) )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → 𝑙 ∈ ( 𝐷 Func 𝐸 ) )
35 eqidd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
36 34 35 prcof1 ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) = ( 𝑙 ∘func 𝐹 ) )
37 36 eqcomd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( 𝑙 ∘func 𝐹 ) = ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) )
38 37 oveq1d ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) = ( ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) 𝑁 𝑋 ) )
39 36 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) = ( 𝑙 ∘func 𝐹 ) )
40 25 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) = ( 𝐿 ∘func 𝐹 ) )
41 39 40 opeq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → ⟨ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ = ⟨ ( 𝑙 ∘func 𝐹 ) , ( 𝐿 ∘func 𝐹 ) ⟩ )
42 41 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → ( ⟨ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ 𝑋 ) = ( ⟨ ( 𝑙 ∘func 𝐹 ) , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ 𝑋 ) )
43 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → 𝐴 = 𝐴 )
44 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) )
45 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
46 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
47 2 44 45 46 prcof21a ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → ( ( 𝑙 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝐿 ) ‘ 𝑏 ) = ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) )
48 42 43 47 oveq123d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → ( 𝐴 ( ⟨ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ 𝑋 ) ( ( 𝑙 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝐿 ) ‘ 𝑏 ) ) = ( 𝐴 ( ⟨ ( 𝑙 ∘func 𝐹 ) , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ 𝑋 ) ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ) )
49 48 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → ( 𝐴 ( ⟨ ( 𝑙 ∘func 𝐹 ) , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ 𝑋 ) ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ) = ( 𝐴 ( ⟨ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ 𝑋 ) ( ( 𝑙 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝐿 ) ‘ 𝑏 ) ) )
50 49 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) ) → ( 𝑎 = ( 𝐴 ( ⟨ ( 𝑙 ∘func 𝐹 ) , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ 𝑋 ) ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ) ↔ 𝑎 = ( 𝐴 ( ⟨ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ 𝑋 ) ( ( 𝑙 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝐿 ) ‘ 𝑏 ) ) ) )
51 50 reubidva ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) ∧ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ) → ( ∃! 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) 𝑎 = ( 𝐴 ( ⟨ ( 𝑙 ∘func 𝐹 ) , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ 𝑋 ) ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ) ↔ ∃! 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) 𝑎 = ( 𝐴 ( ⟨ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ 𝑋 ) ( ( 𝑙 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝐿 ) ‘ 𝑏 ) ) ) )
52 38 51 raleqbidva ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ) → ( ∀ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ∃! 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) 𝑎 = ( 𝐴 ( ⟨ ( 𝑙 ∘func 𝐹 ) , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ 𝑋 ) ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ) ↔ ∀ 𝑎 ∈ ( ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) 𝑁 𝑋 ) ∃! 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) 𝑎 = ( 𝐴 ( ⟨ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ 𝑋 ) ( ( 𝑙 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝐿 ) ‘ 𝑏 ) ) ) )
53 52 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ∃! 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) 𝑎 = ( 𝐴 ( ⟨ ( 𝑙 ∘func 𝐹 ) , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ 𝑋 ) ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ) ↔ ∀ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑎 ∈ ( ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) 𝑁 𝑋 ) ∃! 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) 𝑎 = ( 𝐴 ( ⟨ ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝑙 ) , ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ⟩ ∙ 𝑋 ) ( ( 𝑙 ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) 𝐿 ) ‘ 𝑏 ) ) ) )
54 30 33 53 3bitr4d ⊢ ( 𝜑 → ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) 𝐴 ↔ ∀ 𝑙 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑎 ∈ ( ( 𝑙 ∘func 𝐹 ) 𝑁 𝑋 ) ∃! 𝑏 ∈ ( 𝑙 𝑀 𝐿 ) 𝑎 = ( 𝐴 ( ⟨ ( 𝑙 ∘func 𝐹 ) , ( 𝐿 ∘func 𝐹 ) ⟩ ∙ 𝑋 ) ( 𝑏 ∘ ( 1st ‘ 𝐹 ) ) ) ) )