Metamath Proof Explorer

Theorem mapfienlem3

Description: Lemma 3 for mapfien . (Contributed by AV, 3-Jul-2019) (Revised by AV, 28-Jul-2024)

Ref Expression
Hypotheses mapfien.s ⊢ S = x ∈ B A | finSupp Z⁡ x
mapfien.t ⊢ T = x ∈ D C | finSupp W⁡ x
mapfien.w ⊢ W = G ⁡ Z
mapfien.f ⊢ φ → F : C ⟶ 1-1 onto A
mapfien.g ⊢ φ → G : B ⟶ 1-1 onto D
mapfien.a ⊢ φ → A ∈ U
mapfien.b ⊢ φ → B ∈ V
mapfien.c ⊢ φ → C ∈ X
mapfien.d ⊢ φ → D ∈ Y
mapfien.z ⊢ φ → Z ∈ B
Assertion mapfienlem3 ⊢ φ ∧ g ∈ T → G -1 ∘ g ∘ F -1 ∈ S

Proof

Step Hyp Ref Expression
1 mapfien.s ⊢ S = x ∈ B A | finSupp Z⁡ x
2 mapfien.t ⊢ T = x ∈ D C | finSupp W⁡ x
3 mapfien.w ⊢ W = G ⁡ Z
4 mapfien.f ⊢ φ → F : C ⟶ 1-1 onto A
5 mapfien.g ⊢ φ → G : B ⟶ 1-1 onto D
6 mapfien.a ⊢ φ → A ∈ U
7 mapfien.b ⊢ φ → B ∈ V
8 mapfien.c ⊢ φ → C ∈ X
9 mapfien.d ⊢ φ → D ∈ Y
10 mapfien.z ⊢ φ → Z ∈ B
11 f1ocnv ⊢ G : B ⟶ 1-1 onto D → G -1 : D ⟶ 1-1 onto B
12 f1of ⊢ G -1 : D ⟶ 1-1 onto B → G -1 : D ⟶ B
13 5 11 12 3syl ⊢ φ → G -1 : D ⟶ B
14 13 adantr ⊢ φ ∧ g ∈ T → G -1 : D ⟶ B
15 elrabi ⊢ g ∈ x ∈ D C | finSupp W⁡ x → g ∈ D C
16 15 2 eleq2s ⊢ g ∈ T → g ∈ D C
17 16 adantl ⊢ φ ∧ g ∈ T → g ∈ D C
18 elmapi ⊢ g ∈ D C → g : C ⟶ D
19 17 18 syl ⊢ φ ∧ g ∈ T → g : C ⟶ D
20 14 19 fcod ⊢ φ ∧ g ∈ T → G -1 ∘ g : C ⟶ B
21 f1ocnv ⊢ F : C ⟶ 1-1 onto A → F -1 : A ⟶ 1-1 onto C
22 f1of ⊢ F -1 : A ⟶ 1-1 onto C → F -1 : A ⟶ C
23 4 21 22 3syl ⊢ φ → F -1 : A ⟶ C
24 23 adantr ⊢ φ ∧ g ∈ T → F -1 : A ⟶ C
25 20 24 fcod ⊢ φ ∧ g ∈ T → G -1 ∘ g ∘ F -1 : A ⟶ B
26 7 6 elmapd ⊢ φ → G -1 ∘ g ∘ F -1 ∈ B A ↔ G -1 ∘ g ∘ F -1 : A ⟶ B
27 26 adantr ⊢ φ ∧ g ∈ T → G -1 ∘ g ∘ F -1 ∈ B A ↔ G -1 ∘ g ∘ F -1 : A ⟶ B
28 25 27 mpbird ⊢ φ ∧ g ∈ T → G -1 ∘ g ∘ F -1 ∈ B A
29 1 2 3 4 5 6 7 8 9 10 mapfienlem2 ⊢ φ ∧ g ∈ T → finSupp Z⁡ G -1 ∘ g ∘ F -1
30 breq1 ⊢ x = G -1 ∘ g ∘ F -1 → finSupp Z⁡ x ↔ finSupp Z⁡ G -1 ∘ g ∘ F -1
31 30 1 elrab2 ⊢ G -1 ∘ g ∘ F -1 ∈ S ↔ G -1 ∘ g ∘ F -1 ∈ B A ∧ finSupp Z⁡ G -1 ∘ g ∘ F -1
32 28 29 31 sylanbrc ⊢ φ ∧ g ∈ T → G -1 ∘ g ∘ F -1 ∈ S