Metamath Proof Explorer

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 X. _V ) X. _V )

Proof

Step Hyp Ref Expression
1 df-ran 
 |-  Ran = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) )
2 ovex 
 |-  ( c Func d ) e. _V
3 ovex 
 |-  ( c Func e ) e. _V
4 2 3 mpoex 
 |-  ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) e. _V
5 4 csbex 
 |-  [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) e. _V
6 5 csbex 
 |-  [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) e. _V
7 1 6 fnmpoi 
 |-  Ran Fn ( ( _V X. _V ) X. _V )