relran

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

		Ref	Expression
	Assertion	relran	⊢ Rel ( 𝐹 ( 𝑃 Ran 𝐸 ) 𝑋 )

Proof

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

Metamath Proof Explorer

Theorem relran

Proof