fpwrelmapffs

Description: Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

	Ref	Expression
Hypotheses	fpwrelmap.1	$⊢ A \in V$
	fpwrelmap.2	$⊢ B \in V$
	fpwrelmap.3	$⊢ M = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})$
	fpwrelmapffs.1	$⊢ S = \{f \in ({(𝒫 B \cap Fin)}^{A}) \| f supp \emptyset \in Fin\}$
Assertion	fpwrelmapffs	$⊢ ({M ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 (A \times B) \cap Fin$

Proof

Step	Hyp	Ref	Expression
1		fpwrelmap.1	$⊢ A \in V$
2		fpwrelmap.2	$⊢ B \in V$
3		fpwrelmap.3	$⊢ M = (f \in ({𝒫 B}^{A}) ⟼ \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})$
4		fpwrelmapffs.1	$⊢ S = \{f \in ({(𝒫 B \cap Fin)}^{A}) \| f supp \emptyset \in Fin\}$
5	1 2 3	fpwrelmap	$⊢ M : {𝒫 B}^{A} \underset{1-1 onto}{⟶} 𝒫 (A \times B)$
6	5	a1i	$⊢ ⊤ \to M : {𝒫 B}^{A} \underset{1-1 onto}{⟶} 𝒫 (A \times B)$
7	2	pwex	$⊢ 𝒫 B \in V$
8	7 1	elmap	$⊢ f \in ({𝒫 B}^{A}) \leftrightarrow f : A ⟶ 𝒫 B$
9	8	birani	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to f : A ⟶ 𝒫 B$
10		simpr	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
11	1 2 9 10	fpwrelmapffslem	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to (r \in Fin \leftrightarrow (ran f \subseteq Fin \land f supp \emptyset \in Fin))$
12	11	3adant1	$⊢ (⊤ \land f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to (r \in Fin \leftrightarrow (ran f \subseteq Fin \land f supp \emptyset \in Fin))$
13	3 6 12	f1oresrab	$⊢ ⊤ \to ({M ↾}_{\{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}}) : \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \underset{1-1 onto}{⟶} \{r \in 𝒫 (A \times B) \| r \in Fin\}$
14	13	mptru	$⊢ ({M ↾}_{\{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}}) : \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \underset{1-1 onto}{⟶} \{r \in 𝒫 (A \times B) \| r \in Fin\}$
15	1 7	maprnin	$⊢ {(𝒫 B \cap Fin)}^{A} = \{f \in ({𝒫 B}^{A}) \| ran f \subseteq Fin\}$
16		nfcv	$⊢ \underline{Ⅎ} f ({(𝒫 B \cap Fin)}^{A})$
17		nfrab1	$⊢ \underline{Ⅎ} f \{f \in ({𝒫 B}^{A}) \| ran f \subseteq Fin\}$
18	16 17	rabeqf	$⊢ {(𝒫 B \cap Fin)}^{A} = \{f \in ({𝒫 B}^{A}) \| ran f \subseteq Fin\} \to \{f \in ({(𝒫 B \cap Fin)}^{A}) \| f supp \emptyset \in Fin\} = \{f \in \{f \in ({𝒫 B}^{A}) \| ran f \subseteq Fin\} \| f supp \emptyset \in Fin\}$
19	15 18	ax-mp	$⊢ \{f \in ({(𝒫 B \cap Fin)}^{A}) \| f supp \emptyset \in Fin\} = \{f \in \{f \in ({𝒫 B}^{A}) \| ran f \subseteq Fin\} \| f supp \emptyset \in Fin\}$
20		rabrab	$⊢ \{f \in \{f \in ({𝒫 B}^{A}) \| ran f \subseteq Fin\} \| f supp \emptyset \in Fin\} = \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}$
21	4 19 20	3eqtri	$⊢ S = \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}$
22		dfin5	$⊢ 𝒫 (A \times B) \cap Fin = \{r \in 𝒫 (A \times B) \| r \in Fin\}$
23		f1oeq23	$⊢ (S = \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \land 𝒫 (A \times B) \cap Fin = \{r \in 𝒫 (A \times B) \| r \in Fin\}) \to (({M ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 (A \times B) \cap Fin \leftrightarrow ({M ↾}_{S}) : \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \underset{1-1 onto}{⟶} \{r \in 𝒫 (A \times B) \| r \in Fin\})$
24	21 22 23	mp2an	$⊢ ({M ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 (A \times B) \cap Fin \leftrightarrow ({M ↾}_{S}) : \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \underset{1-1 onto}{⟶} \{r \in 𝒫 (A \times B) \| r \in Fin\}$
25	21	reseq2i	$⊢ {M ↾}_{S} = {M ↾}_{\{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}}$
26		f1oeq1	$⊢ {M ↾}_{S} = {M ↾}_{\{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}} \to (({M ↾}_{S}) : \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \underset{1-1 onto}{⟶} \{r \in 𝒫 (A \times B) \| r \in Fin\} \leftrightarrow ({M ↾}_{\{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}}) : \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \underset{1-1 onto}{⟶} \{r \in 𝒫 (A \times B) \| r \in Fin\})$
27	25 26	ax-mp	$⊢ ({M ↾}_{S}) : \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \underset{1-1 onto}{⟶} \{r \in 𝒫 (A \times B) \| r \in Fin\} \leftrightarrow ({M ↾}_{\{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}}) : \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \underset{1-1 onto}{⟶} \{r \in 𝒫 (A \times B) \| r \in Fin\}$
28	24 27	bitr2i	$⊢ ({M ↾}_{\{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}}) : \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\} \underset{1-1 onto}{⟶} \{r \in 𝒫 (A \times B) \| r \in Fin\} \leftrightarrow ({M ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 (A \times B) \cap Fin$
29	14 28	mpbi	$⊢ ({M ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 (A \times B) \cap Fin$

Metamath Proof Explorer

Theorem fpwrelmapffs

Proof