Theorem fsuppcolem

Description: Lemma for fsuppco . Formula building theorem for finite supports: rearranging the index set. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	fsuppcolem.f	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
	fsuppcolem.g	⊢ ( 𝜑 → 𝐺 : 𝑋 –1-1→ 𝑌 )
Assertion	fsuppcolem	⊢ ( 𝜑 → ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fsuppcolem.f	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
2		fsuppcolem.g	⊢ ( 𝜑 → 𝐺 : 𝑋 –1-1→ 𝑌 )
3		cnvco	⊢ ◡ ( 𝐹 ∘ 𝐺 ) = ( ◡ 𝐺 ∘ ◡ 𝐹 )
4	3	imaeq1i	⊢ ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐺 ∘ ◡ 𝐹 ) “ ( V ∖ { 𝑍 } ) )
5		imaco	⊢ ( ( ◡ 𝐺 ∘ ◡ 𝐹 ) “ ( V ∖ { 𝑍 } ) ) = ( ◡ 𝐺 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
6	4 5	eqtri	⊢ ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ◡ 𝐺 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
7		df-f1	⊢ ( 𝐺 : 𝑋 –1-1→ 𝑌 ↔ ( 𝐺 : 𝑋 ⟶ 𝑌 ∧ Fun ◡ 𝐺 ) )
8	7	simprbi	⊢ ( 𝐺 : 𝑋 –1-1→ 𝑌 → Fun ◡ 𝐺 )
9	2 8	syl	⊢ ( 𝜑 → Fun ◡ 𝐺 )
10		imafi	⊢ ( ( Fun ◡ 𝐺 ∧ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin ) → ( ◡ 𝐺 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
11	9 1 10	syl2anc	⊢ ( 𝜑 → ( ◡ 𝐺 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
12	6 11	eqeltrid	⊢ ( 𝜑 → ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ∈ Fin )