Step 
Hyp 
Ref 
Expression 
1 

fvovco.1 
⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝑉 × 𝑊 ) ) 
2 

fvovco.2 
⊢ ( 𝜑 → 𝑌 ∈ 𝑋 ) 
3 
1 2

ffvelrnd 
⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝑉 × 𝑊 ) ) 
4 

1st2nd2 
⊢ ( ( 𝐹 ‘ 𝑌 ) ∈ ( 𝑉 × 𝑊 ) → ( 𝐹 ‘ 𝑌 ) = ⟨ ( 1^{st} ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 2^{nd} ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ) 
5 
3 4

syl 
⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = ⟨ ( 1^{st} ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 2^{nd} ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ) 
6 
5

fveq2d 
⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 ‘ 𝑌 ) ) = ( 𝑂 ‘ ⟨ ( 1^{st} ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 2^{nd} ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ) ) 
7 

fvco3 
⊢ ( ( 𝐹 : 𝑋 ⟶ ( 𝑉 × 𝑊 ) ∧ 𝑌 ∈ 𝑋 ) → ( ( 𝑂 ∘ 𝐹 ) ‘ 𝑌 ) = ( 𝑂 ‘ ( 𝐹 ‘ 𝑌 ) ) ) 
8 
1 2 7

syl2anc 
⊢ ( 𝜑 → ( ( 𝑂 ∘ 𝐹 ) ‘ 𝑌 ) = ( 𝑂 ‘ ( 𝐹 ‘ 𝑌 ) ) ) 
9 

dfov 
⊢ ( ( 1^{st} ‘ ( 𝐹 ‘ 𝑌 ) ) 𝑂 ( 2^{nd} ‘ ( 𝐹 ‘ 𝑌 ) ) ) = ( 𝑂 ‘ ⟨ ( 1^{st} ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 2^{nd} ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ) 
10 
9

a1i 
⊢ ( 𝜑 → ( ( 1^{st} ‘ ( 𝐹 ‘ 𝑌 ) ) 𝑂 ( 2^{nd} ‘ ( 𝐹 ‘ 𝑌 ) ) ) = ( 𝑂 ‘ ⟨ ( 1^{st} ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 2^{nd} ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ) ) 
11 
6 8 10

3eqtr4d 
⊢ ( 𝜑 → ( ( 𝑂 ∘ 𝐹 ) ‘ 𝑌 ) = ( ( 1^{st} ‘ ( 𝐹 ‘ 𝑌 ) ) 𝑂 ( 2^{nd} ‘ ( 𝐹 ‘ 𝑌 ) ) ) ) 