fpwrelmap

Description: Define a canonical mapping between functions from A into subsets of B and the relations with domain A and range within B . Note that the same relation is used in axdc2lem and marypha2lem1 . (Contributed by Thierry Arnoux, 28-Aug-2017)

	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))\})$
Assertion	fpwrelmap	$⊢ M : {𝒫 B}^{A} \underset{1-1 onto}{⟶} 𝒫 (A \times B)$

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	1	a1i	$⊢ ⊤ \to A \in V$
5		abid2	$⊢ \{y \| y \in f (x)\} = f (x)$
6	5	fvexi	$⊢ \{y \| y \in f (x)\} \in V$
7	6	a1i	$⊢ (⊤ \land x \in A) \to \{y \| y \in f (x)\} \in V$
8	4 7	opabex3d	$⊢ ⊤ \to \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \in V$
9	8	adantr	$⊢ (⊤ \land f \in ({𝒫 B}^{A})) \to \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \in V$
10	1	mptex	$⊢ (x \in A ⟼ \{y \in B \| x r y\}) \in V$
11	10	a1i	$⊢ (⊤ \land r \in 𝒫 (A \times B)) \to (x \in A ⟼ \{y \in B \| x r y\}) \in V$
12		simpr	$⊢ ((f \in ({𝒫 B}^{A}) \land x \in A) \land y \in f (x)) \to y \in f (x)$
13		elmapi	$⊢ f \in ({𝒫 B}^{A}) \to f : A ⟶ 𝒫 B$
14	13	ffvelcdmda	$⊢ (f \in ({𝒫 B}^{A}) \land x \in A) \to f (x) \in 𝒫 B$
15	14	adantr	$⊢ ((f \in ({𝒫 B}^{A}) \land x \in A) \land y \in f (x)) \to f (x) \in 𝒫 B$
16		elelpwi	$⊢ (y \in f (x) \land f (x) \in 𝒫 B) \to y \in B$
17	12 15 16	syl2anc	$⊢ ((f \in ({𝒫 B}^{A}) \land x \in A) \land y \in f (x)) \to y \in B$
18	17	ex	$⊢ (f \in ({𝒫 B}^{A}) \land x \in A) \to (y \in f (x) \to y \in B)$
19	18	imdistanda	$⊢ f \in ({𝒫 B}^{A}) \to ((x \in A \land y \in f (x)) \to (x \in A \land y \in B))$
20	19	ssopab2dv	$⊢ f \in ({𝒫 B}^{A}) \to \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \subseteq \{⟨x, y⟩ \| (x \in A \land y \in B)\}$
21	20	adantr	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \subseteq \{⟨x, y⟩ \| (x \in A \land y \in B)\}$
22		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))\}$
23		df-xp	$⊢ A \times B = \{⟨x, y⟩ \| (x \in A \land y \in B)\}$
24	23	a1i	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to A \times B = \{⟨x, y⟩ \| (x \in A \land y \in B)\}$
25	21 22 24	3sstr4d	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to r \subseteq A \times B$
26		velpw	$⊢ r \in 𝒫 (A \times B) \leftrightarrow r \subseteq A \times B$
27	25 26	sylibr	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to r \in 𝒫 (A \times B)$
28	13	feqmptd	$⊢ f \in ({𝒫 B}^{A}) \to f = (x \in A ⟼ f (x))$
29	28	adantr	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to f = (x \in A ⟼ f (x))$
30		nfv	$⊢ Ⅎ x f \in ({𝒫 B}^{A})$
31		nfopab1	$⊢ \underline{Ⅎ} x \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
32	31	nfeq2	$⊢ Ⅎ x r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
33	30 32	nfan	$⊢ Ⅎ x (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})$
34		df-rab	$⊢ \{y \in B \| x r y\} = \{y \| (y \in B \land x r y)\}$
35	34	a1i	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to \{y \in B \| x r y\} = \{y \| (y \in B \land x r y)\}$
36		nfv	$⊢ Ⅎ y f \in ({𝒫 B}^{A})$
37		nfopab2	$⊢ \underline{Ⅎ} y \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
38	37	nfeq2	$⊢ Ⅎ y r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
39	36 38	nfan	$⊢ Ⅎ y (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})$
40		nfv	$⊢ Ⅎ y x \in A$
41	39 40	nfan	$⊢ Ⅎ y ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A)$
42	17	adantllr	$⊢ (((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \land y \in f (x)) \to y \in B$
43		df-br	$⊢ x r y \leftrightarrow ⟨x, y⟩ \in r$
44		eleq2	$⊢ r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \to (⟨x, y⟩ \in r \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})$
45		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \leftrightarrow (x \in A \land y \in f (x))$
46	44 45	bitrdi	$⊢ r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \to (⟨x, y⟩ \in r \leftrightarrow (x \in A \land y \in f (x)))$
47	43 46	bitrid	$⊢ r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\} \to (x r y \leftrightarrow (x \in A \land y \in f (x)))$
48	47	ad2antlr	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to (x r y \leftrightarrow (x \in A \land y \in f (x)))$
49		elfvdm	$⊢ y \in f (x) \to x \in dom f$
50	49	adantl	$⊢ (f \in ({𝒫 B}^{A}) \land y \in f (x)) \to x \in dom f$
51	13	fdmd	$⊢ f \in ({𝒫 B}^{A}) \to dom f = A$
52	51	adantr	$⊢ (f \in ({𝒫 B}^{A}) \land y \in f (x)) \to dom f = A$
53	50 52	eleqtrd	$⊢ (f \in ({𝒫 B}^{A}) \land y \in f (x)) \to x \in A$
54	53	ex	$⊢ f \in ({𝒫 B}^{A}) \to (y \in f (x) \to x \in A)$
55	54	pm4.71rd	$⊢ f \in ({𝒫 B}^{A}) \to (y \in f (x) \leftrightarrow (x \in A \land y \in f (x)))$
56	55	ad2antrr	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to (y \in f (x) \leftrightarrow (x \in A \land y \in f (x)))$
57	48 56	bitr4d	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to (x r y \leftrightarrow y \in f (x))$
58	57	biimpar	$⊢ (((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \land y \in f (x)) \to x r y$
59	42 58	jca	$⊢ (((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \land y \in f (x)) \to (y \in B \land x r y)$
60	59	ex	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to (y \in f (x) \to (y \in B \land x r y))$
61	57	biimpd	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to (x r y \to y \in f (x))$
62	61	adantld	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to ((y \in B \land x r y) \to y \in f (x))$
63	60 62	impbid	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to (y \in f (x) \leftrightarrow (y \in B \land x r y))$
64	41 63	abbid	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to \{y \| y \in f (x)\} = \{y \| (y \in B \land x r y)\}$
65	5	a1i	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to \{y \| y \in f (x)\} = f (x)$
66	35 64 65	3eqtr2rd	$⊢ ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land x \in A) \to f (x) = \{y \in B \| x r y\}$
67	33 66	mpteq2da	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to (x \in A ⟼ f (x)) = (x \in A ⟼ \{y \in B \| x r y\})$
68	29 67	eqtrd	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to f = (x \in A ⟼ \{y \in B \| x r y\})$
69	27 68	jca	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \to (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\}))$
70		ssrab2	$⊢ \{y \in B \| x r y\} \subseteq B$
71	2 70	elpwi2	$⊢ \{y \in B \| x r y\} \in 𝒫 B$
72	71	a1i	$⊢ (r \in 𝒫 (A \times B) \land x \in A) \to \{y \in B \| x r y\} \in 𝒫 B$
73	72	fmpttd	$⊢ r \in 𝒫 (A \times B) \to (x \in A ⟼ \{y \in B \| x r y\}) : A ⟶ 𝒫 B$
74	73	adantr	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (x \in A ⟼ \{y \in B \| x r y\}) : A ⟶ 𝒫 B$
75		simpr	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to f = (x \in A ⟼ \{y \in B \| x r y\})$
76	75	feq1d	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (f : A ⟶ 𝒫 B \leftrightarrow (x \in A ⟼ \{y \in B \| x r y\}) : A ⟶ 𝒫 B)$
77	74 76	mpbird	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to f : A ⟶ 𝒫 B$
78	2	pwex	$⊢ 𝒫 B \in V$
79	78 1	elmap	$⊢ f \in ({𝒫 B}^{A}) \leftrightarrow f : A ⟶ 𝒫 B$
80	77 79	sylibr	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to f \in ({𝒫 B}^{A})$
81		elpwi	$⊢ r \in 𝒫 (A \times B) \to r \subseteq A \times B$
82	81	adantr	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to r \subseteq A \times B$
83		xpss	$⊢ A \times B \subseteq V \times V$
84	82 83	sstrdi	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to r \subseteq V \times V$
85		df-rel	$⊢ Rel r \leftrightarrow r \subseteq V \times V$
86	84 85	sylibr	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to Rel r$
87		relopabv	$⊢ Rel \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
88	87	a1i	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to Rel \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
89		id	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\}))$
90		nfv	$⊢ Ⅎ x r \in 𝒫 (A \times B)$
91		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ \{y \in B \| x r y\})$
92	91	nfeq2	$⊢ Ⅎ x f = (x \in A ⟼ \{y \in B \| x r y\})$
93	90 92	nfan	$⊢ Ⅎ x (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\}))$
94		nfv	$⊢ Ⅎ y r \in 𝒫 (A \times B)$
95	40	nfci	$⊢ \underline{Ⅎ} y A$
96		nfrab1	$⊢ \underline{Ⅎ} y \{y \in B \| x r y\}$
97	95 96	nfmpt	$⊢ \underline{Ⅎ} y (x \in A ⟼ \{y \in B \| x r y\})$
98	97	nfeq2	$⊢ Ⅎ y f = (x \in A ⟼ \{y \in B \| x r y\})$
99	94 98	nfan	$⊢ Ⅎ y (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\}))$
100		nfcv	$⊢ \underline{Ⅎ} x r$
101		nfcv	$⊢ \underline{Ⅎ} y r$
102		brelg	$⊢ (r \subseteq A \times B \land x r y) \to (x \in A \land y \in B)$
103	81 102	sylan	$⊢ (r \in 𝒫 (A \times B) \land x r y) \to (x \in A \land y \in B)$
104	103	adantlr	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x r y) \to (x \in A \land y \in B)$
105	104	simpld	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x r y) \to x \in A$
106	104	simprd	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x r y) \to y \in B$
107		simpr	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x r y) \to x r y$
108	75	fveq1d	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to f (x) = (x \in A ⟼ \{y \in B \| x r y\}) (x)$
109	2	rabex	$⊢ \{y \in B \| x r y\} \in V$
110		eqid	$⊢ (x \in A ⟼ \{y \in B \| x r y\}) = (x \in A ⟼ \{y \in B \| x r y\})$
111	110	fvmpt2	$⊢ (x \in A \land \{y \in B \| x r y\} \in V) \to (x \in A ⟼ \{y \in B \| x r y\}) (x) = \{y \in B \| x r y\}$
112	109 111	mpan2	$⊢ x \in A \to (x \in A ⟼ \{y \in B \| x r y\}) (x) = \{y \in B \| x r y\}$
113	108 112	sylan9eq	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x \in A) \to f (x) = \{y \in B \| x r y\}$
114	113	eleq2d	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x \in A) \to (y \in f (x) \leftrightarrow y \in \{y \in B \| x r y\})$
115		rabid	$⊢ y \in \{y \in B \| x r y\} \leftrightarrow (y \in B \land x r y)$
116	114 115	bitrdi	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x \in A) \to (y \in f (x) \leftrightarrow (y \in B \land x r y))$
117	105 116	syldan	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x r y) \to (y \in f (x) \leftrightarrow (y \in B \land x r y))$
118	106 107 117	mpbir2and	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x r y) \to y \in f (x)$
119	105 118	jca	$⊢ ((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x r y) \to (x \in A \land y \in f (x))$
120	119	ex	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (x r y \to (x \in A \land y \in f (x)))$
121	116	simplbda	$⊢ (((r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \land x \in A) \land y \in f (x)) \to x r y$
122	121	expl	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to ((x \in A \land y \in f (x)) \to x r y)$
123	120 122	impbid	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (x r y \leftrightarrow (x \in A \land y \in f (x)))$
124	43 123	bitr3id	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (⟨x, y⟩ \in r \leftrightarrow (x \in A \land y \in f (x)))$
125	124 45	bitr4di	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (⟨x, y⟩ \in r \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})$
126	93 99 100 101 31 37 125	eqrelrd2	$⊢ ((Rel r \land Rel \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \land (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\}))) \to r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
127	86 88 89 126	syl21anc	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}$
128	80 127	jca	$⊢ (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})) \to (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\})$
129	69 128	impbii	$⊢ (f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \leftrightarrow (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\}))$
130	129	a1i	$⊢ ⊤ \to ((f \in ({𝒫 B}^{A}) \land r = \{⟨x, y⟩ \| (x \in A \land y \in f (x))\}) \leftrightarrow (r \in 𝒫 (A \times B) \land f = (x \in A ⟼ \{y \in B \| x r y\})))$
131	3 9 11 130	f1od	$⊢ ⊤ \to M : {𝒫 B}^{A} \underset{1-1 onto}{⟶} 𝒫 (A \times B)$
132	131	mptru	$⊢ M : {𝒫 B}^{A} \underset{1-1 onto}{⟶} 𝒫 (A \times B)$

Metamath Proof Explorer

Theorem fpwrelmap

Proof