This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )