Metamath Proof Explorer

Theorem lanfn

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

Ref Expression
Assertion lanfn 
|- Lan Fn ( ( _V X. _V ) X. _V )

Proof

Step Hyp Ref Expression
1 df-lan 
 |-  Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( 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 ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) e. _V
5 4 csbex 
 |-  [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( 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 ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) e. _V
7 1 6 fnmpoi 
 |-  Lan Fn ( ( _V X. _V ) X. _V )