mapfien2

Description: Equinumerousity relation for sets of finitely supported functions. (Contributed by Stefan O'Rear, 9-Jul-2015) (Revised by AV, 7-Jul-2019)

	Ref	Expression
Hypotheses	mapfien2.s	$⊢ S = \{x \in (B^{A}) \| {finSupp}_{\underset{˙}{0}} (x)\}$
	mapfien2.t	$⊢ T = \{x \in (D^{C}) \| {finSupp}_{W} (x)\}$
	mapfien2.ac	$⊢ φ \to A \approx C$
	mapfien2.bd	$⊢ φ \to B \approx D$
	mapfien2.z	$⊢ φ \to \underset{˙}{0} \in B$
	mapfien2.w	$⊢ φ \to W \in D$
Assertion	mapfien2	$⊢ φ \to S \approx T$

Proof

Step	Hyp	Ref	Expression
1		mapfien2.s	$⊢ S = \{x \in (B^{A}) \| {finSupp}_{\underset{˙}{0}} (x)\}$
2		mapfien2.t	$⊢ T = \{x \in (D^{C}) \| {finSupp}_{W} (x)\}$
3		mapfien2.ac	$⊢ φ \to A \approx C$
4		mapfien2.bd	$⊢ φ \to B \approx D$
5		mapfien2.z	$⊢ φ \to \underset{˙}{0} \in B$
6		mapfien2.w	$⊢ φ \to W \in D$
7		enfixsn	$⊢ (\underset{˙}{0} \in B \land W \in D \land B \approx D) \to \exists y (y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W)$
8	5 6 4 7	syl3anc	$⊢ φ \to \exists y (y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W)$
9		bren	$⊢ A \approx C \leftrightarrow \exists z z : A \underset{1-1 onto}{⟶} C$
10	3 9	sylib	$⊢ φ \to \exists z z : A \underset{1-1 onto}{⟶} C$
11		eqid	$⊢ \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\} = \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\}$
12		eqid	$⊢ y (\underset{˙}{0}) = y (\underset{˙}{0})$
13		f1ocnv	$⊢ z : A \underset{1-1 onto}{⟶} C \to z^{-1} : C \underset{1-1 onto}{⟶} A$
14	13	3ad2ant2	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to z^{-1} : C \underset{1-1 onto}{⟶} A$
15		simp3	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to y : B \underset{1-1 onto}{⟶} D$
16	3	3ad2ant1	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to A \approx C$
17		relen	$⊢ Rel \approx$
18	17	brrelex1i	$⊢ A \approx C \to A \in V$
19	16 18	syl	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to A \in V$
20	4	3ad2ant1	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to B \approx D$
21	17	brrelex1i	$⊢ B \approx D \to B \in V$
22	20 21	syl	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to B \in V$
23	17	brrelex2i	$⊢ A \approx C \to C \in V$
24	16 23	syl	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to C \in V$
25	17	brrelex2i	$⊢ B \approx D \to D \in V$
26	20 25	syl	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to D \in V$
27	5	3ad2ant1	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to \underset{˙}{0} \in B$
28	1 11 12 14 15 19 22 24 26 27	mapfien	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to (w \in S ⟼ y \circ (w \circ z^{-1})) : S \underset{1-1 onto}{⟶} \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\}$
29		ovex	$⊢ B^{A} \in V$
30	1 29	rabex2	$⊢ S \in V$
31	30	f1oen	$⊢ (w \in S ⟼ y \circ (w \circ z^{-1})) : S \underset{1-1 onto}{⟶} \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\} \to S \approx \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\}$
32	28 31	syl	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land y : B \underset{1-1 onto}{⟶} D) \to S \approx \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\}$
33	32	3adant3r	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land (y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W)) \to S \approx \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\}$
34		breq2	$⊢ y (\underset{˙}{0}) = W \to ({finSupp}_{y (\underset{˙}{0})} (x) \leftrightarrow {finSupp}_{W} (x))$
35	34	rabbidv	$⊢ y (\underset{˙}{0}) = W \to \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\} = \{x \in (D^{C}) \| {finSupp}_{W} (x)\}$
36	35 2	eqtr4di	$⊢ y (\underset{˙}{0}) = W \to \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\} = T$
37	36	adantl	$⊢ (y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W) \to \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\} = T$
38	37	3ad2ant3	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land (y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W)) \to \{x \in (D^{C}) \| {finSupp}_{y (\underset{˙}{0})} (x)\} = T$
39	33 38	breqtrd	$⊢ (φ \land z : A \underset{1-1 onto}{⟶} C \land (y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W)) \to S \approx T$
40	39	3exp	$⊢ φ \to (z : A \underset{1-1 onto}{⟶} C \to ((y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W) \to S \approx T))$
41	40	exlimdv	$⊢ φ \to (\exists z z : A \underset{1-1 onto}{⟶} C \to ((y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W) \to S \approx T))$
42	10 41	mpd	$⊢ φ \to ((y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W) \to S \approx T)$
43	42	exlimdv	$⊢ φ \to (\exists y (y : B \underset{1-1 onto}{⟶} D \land y (\underset{˙}{0}) = W) \to S \approx T)$
44	8 43	mpd	$⊢ φ \to S \approx T$

Metamath Proof Explorer

Theorem mapfien2

Proof