Metamath Proof Explorer

Theorem rellan

Description: The set of left Kan extensions is a relation. (Contributed by Zhi Wang, 3-Nov-2025)

Ref Expression
Assertion rellan Rel ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 )

Proof

Step Hyp Ref Expression
1 rel0 ⊢ Rel ∅
2 releq ⊢ ( ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) = ∅ → ( Rel ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) ↔ Rel ∅ ) )
3 1 2 mpbiri ⊢ ( ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) = ∅ → Rel ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) )
4 n0 ⊢ ( ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) )
5 relup ⊢ Rel ( ( ⟨ ( 2nd ‘ 𝑃 ) , 𝐸 ⟩ −∘F 𝐹 ) ( ( ( 2nd ‘ 𝑃 ) FuncCat 𝐸 ) UP ( ( 1st ‘ 𝑃 ) FuncCat 𝐸 ) ) 𝑋 )
6 ne0i ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) ≠ ∅ )
7 oveq ⊢ ( ( 𝑃 Lan 𝐸 ) = ∅ → ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) = ( 𝐹 ∅ 𝑋 ) )
8 0ov ⊢ ( 𝐹 ∅ 𝑋 ) = ∅
9 7 8 eqtrdi ⊢ ( ( 𝑃 Lan 𝐸 ) = ∅ → ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) = ∅ )
10 9 necon3i ⊢ ( ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) ≠ ∅ → ( 𝑃 Lan 𝐸 ) ≠ ∅ )
11 n0 ⊢ ( ( 𝑃 Lan 𝐸 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑃 Lan 𝐸 ) )
12 df-lan ⊢ Lan = ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ( ( 𝑑 FuncCat 𝑒 ) UP ( 𝑐 FuncCat 𝑒 ) ) 𝑥 ) ) )
13 12 elmpocl1 ⊢ ( 𝑥 ∈ ( 𝑃 Lan 𝐸 ) → 𝑃 ∈ ( V × V ) )
14 1st2nd2 ⊢ ( 𝑃 ∈ ( V × V ) → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )
15 13 14 syl ⊢ ( 𝑥 ∈ ( 𝑃 Lan 𝐸 ) → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )
16 15 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝑃 Lan 𝐸 ) → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )
17 11 16 sylbi ⊢ ( ( 𝑃 Lan 𝐸 ) ≠ ∅ → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )
18 6 10 17 3syl ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )
19 18 oveq1d ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → ( 𝑃 Lan 𝐸 ) = ( ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ Lan 𝐸 ) )
20 19 oveqd ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) = ( 𝐹 ( ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ Lan 𝐸 ) 𝑋 ) )
21 eqid ⊢ ( ( 2nd ‘ 𝑃 ) FuncCat 𝐸 ) = ( ( 2nd ‘ 𝑃 ) FuncCat 𝐸 )
22 eqid ⊢ ( ( 1st ‘ 𝑃 ) FuncCat 𝐸 ) = ( ( 1st ‘ 𝑃 ) FuncCat 𝐸 )
23 id ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) )
24 23 20 eleqtrd ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → 𝑥 ∈ ( 𝐹 ( ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ Lan 𝐸 ) 𝑋 ) )
25 lanrcl ⊢ ( 𝑥 ∈ ( 𝐹 ( ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ Lan 𝐸 ) 𝑋 ) → ( 𝐹 ∈ ( ( 1st ‘ 𝑃 ) Func ( 2nd ‘ 𝑃 ) ) ∧ 𝑋 ∈ ( ( 1st ‘ 𝑃 ) Func 𝐸 ) ) )
26 24 25 syl ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → ( 𝐹 ∈ ( ( 1st ‘ 𝑃 ) Func ( 2nd ‘ 𝑃 ) ) ∧ 𝑋 ∈ ( ( 1st ‘ 𝑃 ) Func 𝐸 ) ) )
27 26 simpld ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → 𝐹 ∈ ( ( 1st ‘ 𝑃 ) Func ( 2nd ‘ 𝑃 ) ) )
28 26 simprd ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → 𝑋 ∈ ( ( 1st ‘ 𝑃 ) Func 𝐸 ) )
29 eqidd ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → ( ⟨ ( 2nd ‘ 𝑃 ) , 𝐸 ⟩ −∘F 𝐹 ) = ( ⟨ ( 2nd ‘ 𝑃 ) , 𝐸 ⟩ −∘F 𝐹 ) )
30 21 22 27 28 29 lanval ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → ( 𝐹 ( ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ Lan 𝐸 ) 𝑋 ) = ( ( ⟨ ( 2nd ‘ 𝑃 ) , 𝐸 ⟩ −∘F 𝐹 ) ( ( ( 2nd ‘ 𝑃 ) FuncCat 𝐸 ) UP ( ( 1st ‘ 𝑃 ) FuncCat 𝐸 ) ) 𝑋 ) )
31 20 30 eqtrd ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) = ( ( ⟨ ( 2nd ‘ 𝑃 ) , 𝐸 ⟩ −∘F 𝐹 ) ( ( ( 2nd ‘ 𝑃 ) FuncCat 𝐸 ) UP ( ( 1st ‘ 𝑃 ) FuncCat 𝐸 ) ) 𝑋 ) )
32 31 releqd ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → ( Rel ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) ↔ Rel ( ( ⟨ ( 2nd ‘ 𝑃 ) , 𝐸 ⟩ −∘F 𝐹 ) ( ( ( 2nd ‘ 𝑃 ) FuncCat 𝐸 ) UP ( ( 1st ‘ 𝑃 ) FuncCat 𝐸 ) ) 𝑋 ) ) )
33 5 32 mpbiri ⊢ ( 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → Rel ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) )
34 33 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) → Rel ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) )
35 4 34 sylbi ⊢ ( ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) ≠ ∅ → Rel ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 ) )
36 3 35 pm2.61ine ⊢ Rel ( 𝐹 ( 𝑃 Lan 𝐸 ) 𝑋 )