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

Metamath Proof Explorer

Theorem fpwrelmap

Proof