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 ⊢ φ → F -1 V ∖ Z ∈ Fin
fsuppcolem.g ⊢ φ → G : X ⟶ 1-1 Y
Assertion fsuppcolem ⊢ φ → F ∘ G -1 V ∖ Z ∈ Fin

Proof

Step Hyp Ref Expression
1 fsuppcolem.f ⊢ φ → F -1 V ∖ Z ∈ Fin
2 fsuppcolem.g ⊢ φ → G : X ⟶ 1-1 Y
3 cnvco ⊢ F ∘ G -1 = G -1 ∘ F -1
4 3 imaeq1i ⊢ F ∘ G -1 V ∖ Z = G -1 ∘ F -1 V ∖ Z
5 imaco ⊢ G -1 ∘ F -1 V ∖ Z = G -1 F -1 V ∖ Z
6 4 5 eqtri ⊢ F ∘ G -1 V ∖ Z = G -1 F -1 V ∖ Z
7 df-f1 ⊢ G : X ⟶ 1-1 Y ↔ G : X ⟶ Y ∧ Fun ⁡ G -1
8 7 simprbi ⊢ G : X ⟶ 1-1 Y → Fun ⁡ G -1
9 2 8 syl ⊢ φ → Fun ⁡ G -1
10 imafi ⊢ Fun ⁡ G -1 ∧ F -1 V ∖ Z ∈ Fin → G -1 F -1 V ∖ Z ∈ Fin
11 9 1 10 syl2anc ⊢ φ → G -1 F -1 V ∖ Z ∈ Fin
12 6 11 eqeltrid ⊢ φ → F ∘ G -1 V ∖ Z ∈ Fin