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 \in (B^{A}) \| {finSupp}_{Z} (x)\}$
	mapfien.t	$⊢ T = \{x \in (D^{C}) \| {finSupp}_{W} (x)\}$
	mapfien.w	$⊢ W = G (Z)$
	mapfien.f	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
	mapfien.g	$⊢ φ \to G : B \underset{1-1 onto}{⟶} D$
	mapfien.a	$⊢ φ \to A \in U$
	mapfien.b	$⊢ φ \to B \in V$
	mapfien.c	$⊢ φ \to C \in X$
	mapfien.d	$⊢ φ \to D \in Y$
	mapfien.z	$⊢ φ \to Z \in B$
Assertion	mapfienlem3	$⊢ (φ \land g \in T) \to (G^{-1} \circ g) \circ F^{-1} \in S$

Proof

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

Metamath Proof Explorer

Theorem mapfienlem3

Proof