Metamath Proof Explorer

Theorem ranrcl4lem

Description: Lemma for ranrcl4 and ranrcl5 . (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypothesis ranrcl2.l 
|- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
Assertion ranrcl4lem 
|- ( ph -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. )

Proof

Step Hyp Ref Expression
1 ranrcl2.l 
 |-  ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
2 1 ranrcl2 
 |-  ( ph -> F e. ( C Func D ) )
3 opex 
 |-  <. D , E >. e. _V
4 3 a1i 
 |-  ( ph -> <. D , E >. e. _V )
5 2 4 prcofelvv 
 |-  ( ph -> ( <. D , E >. -o.F F ) e. ( _V X. _V ) )
6 1st2nd2 
 |-  ( ( <. D , E >. -o.F F ) e. ( _V X. _V ) -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. )
7 5 6 syl 
 |-  ( ph -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. )