Theorem algrflem

Description: Lemma for algrf and related theorems. (Contributed by Mario Carneiro, 28-May-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	algrflem.1	⊢ 𝐵 ∈ V
	algrflem.2	⊢ 𝐶 ∈ V
Assertion	algrflem	⊢ ( 𝐵 ( 𝐹 ∘ 1st ) 𝐶 ) = ( 𝐹 ‘ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		algrflem.1	⊢ 𝐵 ∈ V
2		algrflem.2	⊢ 𝐶 ∈ V
3		df-ov	⊢ ( 𝐵 ( 𝐹 ∘ 1st ) 𝐶 ) = ( ( 𝐹 ∘ 1st ) ‘ ⟨ 𝐵 , 𝐶 ⟩ )
4		fo1st	⊢ 1st : V –onto→ V
5		fof	⊢ ( 1st : V –onto→ V → 1st : V ⟶ V )
6	4 5	ax-mp	⊢ 1st : V ⟶ V
7		opex	⊢ ⟨ 𝐵 , 𝐶 ⟩ ∈ V
8		fvco3	⊢ ( ( 1st : V ⟶ V ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ V ) → ( ( 𝐹 ∘ 1st ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = ( 𝐹 ‘ ( 1st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) )
9	6 7 8	mp2an	⊢ ( ( 𝐹 ∘ 1st ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = ( 𝐹 ‘ ( 1st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) )
10	1 2	op1st	⊢ ( 1st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = 𝐵
11	10	fveq2i	⊢ ( 𝐹 ‘ ( 1st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = ( 𝐹 ‘ 𝐵 )
12	3 9 11	3eqtri	⊢ ( 𝐵 ( 𝐹 ∘ 1st ) 𝐶 ) = ( 𝐹 ‘ 𝐵 )