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		simpl	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to f \in ({𝒫 B}^{A})$
8	2	pwex	$⊢ 𝒫 B \in V$
9	8 1	elmap	$⊢ f \in ({𝒫 B}^{A}) \leftrightarrow f : A ⟶ 𝒫 B$
10	7 9	sylib	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to f : A ⟶ 𝒫 B$
11		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))\}$
12	1 2 10 11	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))$
13	12	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))$
14	3 6 13	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\}$
15	14	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\}$
16	1 8	maprnin	$⊢ {(𝒫 B \cap Fin)}^{A} = \{f \in ({𝒫 B}^{A}) \| ran f \subseteq Fin\}$
17		nfcv	$⊢ \underline{Ⅎ} f ({(𝒫 B \cap Fin)}^{A})$
18		nfrab1	$⊢ \underline{Ⅎ} f \{f \in ({𝒫 B}^{A}) \| ran f \subseteq Fin\}$
19	17 18	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\}$
20	16 19	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\}$
21		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)\}$
22	4 20 21	3eqtri	$⊢ S = \{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}$
23		dfin5	$⊢ 𝒫 (A \times B) \cap Fin = \{r \in 𝒫 (A \times B) \| r \in Fin\}$
24		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\})$
25	22 23 24	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\}$
26	22	reseq2i	$⊢ {M ↾}_{S} = {M ↾}_{\{f \in ({𝒫 B}^{A}) \| (ran f \subseteq Fin \land f supp \emptyset \in Fin)\}}$
27		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\})$
28	26 27	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\}$
29	25 28	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$
30	15 29	mpbi	$⊢ ({M ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 (A \times B) \cap Fin$

Metamath Proof Explorer

Theorem fpwrelmapffs

Proof