Metamath Proof Explorer

Theorem lanrcl

Description: Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025)

Ref Expression
Assertion lanrcl ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) )
2 ne0i ⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) ≠ ∅ )
3 eqid ⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
4 eqid ⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
5 df-ov ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) = ( Lan ‘ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ )
6 5 eqeq1i ⊢ ( ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) = ∅ ↔ ( Lan ‘ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ) = ∅ )
7 oveq ⊢ ( ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) = ∅ → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ( 𝐹 ∅ 𝑋 ) )
8 0ov ⊢ ( 𝐹 ∅ 𝑋 ) = ∅
9 7 8 eqtrdi ⊢ ( ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) = ∅ → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ∅ )
10 6 9 sylbir ⊢ ( ( Lan ‘ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ) = ∅ → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ∅ )
11 10 necon3i ⊢ ( ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) ≠ ∅ → ( Lan ‘ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ) ≠ ∅ )
12 fvfundmfvn0 ⊢ ( ( Lan ‘ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ) ≠ ∅ → ( ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ∈ dom Lan ∧ Fun ( Lan ↾ { ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ } ) ) )
13 12 simpld ⊢ ( ( Lan ‘ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ) ≠ ∅ → ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ∈ dom Lan )
14 lanfn ⊢ Lan Fn ( ( V × V ) × V )
15 14 fndmi ⊢ dom Lan = ( ( V × V ) × V )
16 13 15 eleqtrdi ⊢ ( ( Lan ‘ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ) ≠ ∅ → ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ∈ ( ( V × V ) × V ) )
17 opelxp1 ⊢ ( ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ∈ ( ( V × V ) × V ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( V × V ) )
18 opelxp1 ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( V × V ) → 𝐶 ∈ V )
19 11 16 17 18 4syl ⊢ ( ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) ≠ ∅ → 𝐶 ∈ V )
20 opelxp2 ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( V × V ) → 𝐷 ∈ V )
21 11 16 17 20 4syl ⊢ ( ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) ≠ ∅ → 𝐷 ∈ V )
22 opelxp2 ⊢ ( ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝐸 ⟩ ∈ ( ( V × V ) × V ) → 𝐸 ∈ V )
23 11 16 22 3syl ⊢ ( ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) ≠ ∅ → 𝐸 ∈ V )
24 3 4 19 21 23 lanfval ⊢ ( ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) ≠ ∅ → ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑥 ) ) )
25 2 24 syl ⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑥 ) ) )
26 25 oveqd ⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ( 𝐹 ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑥 ) ) 𝑋 ) )
27 1 26 eleqtrd ⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → 𝐿 ∈ ( 𝐹 ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑥 ) ) 𝑋 ) )
28 eqid ⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑥 ) ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑥 ) )
29 28 elmpocl ⊢ ( 𝐿 ∈ ( 𝐹 ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑥 ) ) 𝑋 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
30 27 29 syl ⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )