Step 
Hyp 
Ref 
Expression 
1 

dfinr 
 inr = ( x e. _V > <. 1o , x >. ) 
2 

opeq2 
 ( x = X > <. 1o , x >. = <. 1o , X >. ) 
3 

elex 
 ( X e. V > X e. _V ) 
4 

opex 
 <. 1o , X >. e. _V 
5 
4

a1i 
 ( X e. V > <. 1o , X >. e. _V ) 
6 
1 2 3 5

fvmptd3 
 ( X e. V > ( inr ` X ) = <. 1o , X >. ) 
7 
6

fveq2d 
 ( X e. V > ( 2nd ` ( inr ` X ) ) = ( 2nd ` <. 1o , X >. ) ) 
8 

1oex 
 1o e. _V 
9 

op2ndg 
 ( ( 1o e. _V /\ X e. V ) > ( 2nd ` <. 1o , X >. ) = X ) 
10 
8 9

mpan 
 ( X e. V > ( 2nd ` <. 1o , X >. ) = X ) 
11 
7 10

eqtrd 
 ( X e. V > ( 2nd ` ( inr ` X ) ) = X ) 