Metamath Proof Explorer

Theorem ranrcl

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

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

Proof

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