Theorem ranrcl4lem

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

	Ref	Expression
Hypothesis	ranrcl2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) 𝐴 )
Assertion	ranrcl4lem	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		ranrcl2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) 𝐴 )
2	1	ranrcl2	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		opex	⊢ ⟨ 𝐷 , 𝐸 ⟩ ∈ V
4	3	a1i	⊢ ( 𝜑 → ⟨ 𝐷 , 𝐸 ⟩ ∈ V )
5	2 4	prcofelvv	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( V × V ) )
6		1st2nd2	⊢ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( V × V ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )
7	5 6	syl	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )