Theorem ranfn

Description: Ran is a function on ( (V X. V ) X. _V ) . (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Assertion	ranfn	⊢ Ran Fn ( ( V × V ) × V )

Proof

Step	Hyp	Ref	Expression
1		df-ran	⊢ Ran = ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) )
2		ovex	⊢ ( 𝑐 Func 𝑑 ) ∈ V
3		ovex	⊢ ( 𝑐 Func 𝑒 ) ∈ V
4	2 3	mpoex	⊢ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) ∈ V
5	4	csbex	⊢ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) ∈ V
6	5	csbex	⊢ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) ∈ V
7	1 6	fnmpoi	⊢ Ran Fn ( ( V × V ) × V )