fsovrfovd

Description: The operator which gives a 1-to-1 a mapping to a subset and a reverse mapping from elements can be composed from the operator which gives a 1-to-1 mapping between relations and functions to subsets and the converse operator. (Contributed by RP, 15-May-2021)

	Ref	Expression
Hypotheses	fsovd.fs	$⊢ O = (a \in V, b \in V ⟼ (f \in ({𝒫 b}^{a}) ⟼ (y \in b ⟼ \{x \in a \| y \in f (x)\})))$
	fsovd.a	$⊢ φ \to A \in V$
	fsovd.b	$⊢ φ \to B \in W$
	fsovd.rf	$⊢ R = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ (u \in a ⟼ \{v \in b \| u r v\})))$
	fsovd.cnv	$⊢ C = (a \in V, b \in V ⟼ (s \in 𝒫 (a \times b) ⟼ s^{-1}))$
Assertion	fsovrfovd	$⊢ φ \to A O B = (B R A) \circ ((A C B) \circ {(A R B)}^{-1})$

Proof

Step	Hyp	Ref	Expression
1		fsovd.fs	$⊢ O = (a \in V, b \in V ⟼ (f \in ({𝒫 b}^{a}) ⟼ (y \in b ⟼ \{x \in a \| y \in f (x)\})))$
2		fsovd.a	$⊢ φ \to A \in V$
3		fsovd.b	$⊢ φ \to B \in W$
4		fsovd.rf	$⊢ R = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ (u \in a ⟼ \{v \in b \| u r v\})))$
5		fsovd.cnv	$⊢ C = (a \in V, b \in V ⟼ (s \in 𝒫 (a \times b) ⟼ s^{-1}))$
6	3 2	xpexd	$⊢ φ \to B \times A \in V$
7	6	adantr	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to B \times A \in V$
8		elmapi	$⊢ f \in ({𝒫 B}^{A}) \to f : A ⟶ 𝒫 B$
9	8	ffvelcdmda	$⊢ (f \in ({𝒫 B}^{A}) \land u \in A) \to f (u) \in 𝒫 B$
10	9	elpwid	$⊢ (f \in ({𝒫 B}^{A}) \land u \in A) \to f (u) \subseteq B$
11	10	sseld	$⊢ (f \in ({𝒫 B}^{A}) \land u \in A) \to (v \in f (u) \to v \in B)$
12	11	impancom	$⊢ (f \in ({𝒫 B}^{A}) \land v \in f (u)) \to (u \in A \to v \in B)$
13	12	pm4.71d	$⊢ (f \in ({𝒫 B}^{A}) \land v \in f (u)) \to (u \in A \leftrightarrow (u \in A \land v \in B))$
14	13	ex	$⊢ f \in ({𝒫 B}^{A}) \to (v \in f (u) \to (u \in A \leftrightarrow (u \in A \land v \in B)))$
15	14	pm5.32rd	$⊢ f \in ({𝒫 B}^{A}) \to ((u \in A \land v \in f (u)) \leftrightarrow ((u \in A \land v \in B) \land v \in f (u)))$
16		ancom	$⊢ (u \in A \land v \in B) \leftrightarrow (v \in B \land u \in A)$
17	16	anbi1i	$⊢ ((u \in A \land v \in B) \land v \in f (u)) \leftrightarrow ((v \in B \land u \in A) \land v \in f (u))$
18	15 17	bitrdi	$⊢ f \in ({𝒫 B}^{A}) \to ((u \in A \land v \in f (u)) \leftrightarrow ((v \in B \land u \in A) \land v \in f (u)))$
19	18	opabbidv	$⊢ f \in ({𝒫 B}^{A}) \to \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} = \{⟨v, u⟩ \| ((v \in B \land u \in A) \land v \in f (u))\}$
20		opabssxp	$⊢ \{⟨v, u⟩ \| ((v \in B \land u \in A) \land v \in f (u))\} \subseteq B \times A$
21	19 20	eqsstrdi	$⊢ f \in ({𝒫 B}^{A}) \to \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} \subseteq B \times A$
22	21	adantl	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} \subseteq B \times A$
23	7 22	sselpwd	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} \in 𝒫 (B \times A)$
24		eqidd	$⊢ φ \to (f \in ({𝒫 B}^{A}) ⟼ \{⟨v, u⟩ \| (u \in A \land v \in f (u))\}) = (f \in ({𝒫 B}^{A}) ⟼ \{⟨v, u⟩ \| (u \in A \land v \in f (u))\})$
25	4 3 2	rfovd	$⊢ φ \to B R A = (r \in 𝒫 (B \times A) ⟼ (u \in B ⟼ \{v \in A \| u r v\}))$
26		breq	$⊢ r = t \to (u r v \leftrightarrow u t v)$
27	26	rabbidv	$⊢ r = t \to \{v \in A \| u r v\} = \{v \in A \| u t v\}$
28	27	mpteq2dv	$⊢ r = t \to (u \in B ⟼ \{v \in A \| u r v\}) = (u \in B ⟼ \{v \in A \| u t v\})$
29		breq1	$⊢ u = c \to (u t v \leftrightarrow c t v)$
30	29	rabbidv	$⊢ u = c \to \{v \in A \| u t v\} = \{v \in A \| c t v\}$
31		breq2	$⊢ v = d \to (c t v \leftrightarrow c t d)$
32	31	cbvrabv	$⊢ \{v \in A \| c t v\} = \{d \in A \| c t d\}$
33	30 32	eqtrdi	$⊢ u = c \to \{v \in A \| u t v\} = \{d \in A \| c t d\}$
34	33	cbvmptv	$⊢ (u \in B ⟼ \{v \in A \| u t v\}) = (c \in B ⟼ \{d \in A \| c t d\})$
35	28 34	eqtrdi	$⊢ r = t \to (u \in B ⟼ \{v \in A \| u r v\}) = (c \in B ⟼ \{d \in A \| c t d\})$
36	35	cbvmptv	$⊢ (r \in 𝒫 (B \times A) ⟼ (u \in B ⟼ \{v \in A \| u r v\})) = (t \in 𝒫 (B \times A) ⟼ (c \in B ⟼ \{d \in A \| c t d\}))$
37	25 36	eqtrdi	$⊢ φ \to B R A = (t \in 𝒫 (B \times A) ⟼ (c \in B ⟼ \{d \in A \| c t d\}))$
38		breq	$⊢ t = \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} \to (c t d \leftrightarrow c \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} d)$
39		df-br	$⊢ c \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} d \leftrightarrow ⟨c, d⟩ \in \{⟨v, u⟩ \| (u \in A \land v \in f (u))\}$
40		vex	$⊢ c \in V$
41		vex	$⊢ d \in V$
42		eleq1w	$⊢ v = c \to (v \in f (u) \leftrightarrow c \in f (u))$
43	42	anbi2d	$⊢ v = c \to ((u \in A \land v \in f (u)) \leftrightarrow (u \in A \land c \in f (u)))$
44		eleq1w	$⊢ u = d \to (u \in A \leftrightarrow d \in A)$
45		fveq2	$⊢ u = d \to f (u) = f (d)$
46	45	eleq2d	$⊢ u = d \to (c \in f (u) \leftrightarrow c \in f (d))$
47	44 46	anbi12d	$⊢ u = d \to ((u \in A \land c \in f (u)) \leftrightarrow (d \in A \land c \in f (d)))$
48	40 41 43 47	opelopab	$⊢ ⟨c, d⟩ \in \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} \leftrightarrow (d \in A \land c \in f (d))$
49	39 48	bitri	$⊢ c \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} d \leftrightarrow (d \in A \land c \in f (d))$
50	38 49	bitrdi	$⊢ t = \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} \to (c t d \leftrightarrow (d \in A \land c \in f (d)))$
51	50	rabbidv	$⊢ t = \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} \to \{d \in A \| c t d\} = \{d \in A \| (d \in A \land c \in f (d))\}$
52	51	mpteq2dv	$⊢ t = \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} \to (c \in B ⟼ \{d \in A \| c t d\}) = (c \in B ⟼ \{d \in A \| (d \in A \land c \in f (d))\})$
53		ibar	$⊢ d \in A \to (c \in f (d) \leftrightarrow (d \in A \land c \in f (d)))$
54	53	bicomd	$⊢ d \in A \to ((d \in A \land c \in f (d)) \leftrightarrow c \in f (d))$
55	54	rabbiia	$⊢ \{d \in A \| (d \in A \land c \in f (d))\} = \{d \in A \| c \in f (d)\}$
56		fveq2	$⊢ d = x \to f (d) = f (x)$
57	56	eleq2d	$⊢ d = x \to (c \in f (d) \leftrightarrow c \in f (x))$
58	57	cbvrabv	$⊢ \{d \in A \| c \in f (d)\} = \{x \in A \| c \in f (x)\}$
59	55 58	eqtri	$⊢ \{d \in A \| (d \in A \land c \in f (d))\} = \{x \in A \| c \in f (x)\}$
60	59	mpteq2i	$⊢ (c \in B ⟼ \{d \in A \| (d \in A \land c \in f (d))\}) = (c \in B ⟼ \{x \in A \| c \in f (x)\})$
61		eleq1w	$⊢ c = y \to (c \in f (x) \leftrightarrow y \in f (x))$
62	61	rabbidv	$⊢ c = y \to \{x \in A \| c \in f (x)\} = \{x \in A \| y \in f (x)\}$
63	62	cbvmptv	$⊢ (c \in B ⟼ \{x \in A \| c \in f (x)\}) = (y \in B ⟼ \{x \in A \| y \in f (x)\})$
64	60 63	eqtri	$⊢ (c \in B ⟼ \{d \in A \| (d \in A \land c \in f (d))\}) = (y \in B ⟼ \{x \in A \| y \in f (x)\})$
65	52 64	eqtrdi	$⊢ t = \{⟨v, u⟩ \| (u \in A \land v \in f (u))\} \to (c \in B ⟼ \{d \in A \| c t d\}) = (y \in B ⟼ \{x \in A \| y \in f (x)\})$
66	23 24 37 65	fmptco	$⊢ φ \to (B R A) \circ (f \in ({𝒫 B}^{A}) ⟼ \{⟨v, u⟩ \| (u \in A \land v \in f (u))\}) = (f \in ({𝒫 B}^{A}) ⟼ (y \in B ⟼ \{x \in A \| y \in f (x)\}))$
67	2 3	xpexd	$⊢ φ \to A \times B \in V$
68	67	adantr	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to A \times B \in V$
69	15	opabbidv	$⊢ f \in ({𝒫 B}^{A}) \to \{⟨u, v⟩ \| (u \in A \land v \in f (u))\} = \{⟨u, v⟩ \| ((u \in A \land v \in B) \land v \in f (u))\}$
70		opabssxp	$⊢ \{⟨u, v⟩ \| ((u \in A \land v \in B) \land v \in f (u))\} \subseteq A \times B$
71	69 70	eqsstrdi	$⊢ f \in ({𝒫 B}^{A}) \to \{⟨u, v⟩ \| (u \in A \land v \in f (u))\} \subseteq A \times B$
72	71	adantl	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to \{⟨u, v⟩ \| (u \in A \land v \in f (u))\} \subseteq A \times B$
73	68 72	sselpwd	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to \{⟨u, v⟩ \| (u \in A \land v \in f (u))\} \in 𝒫 (A \times B)$
74		eqid	$⊢ A R B = A R B$
75	4 2 3 74	rfovcnvd	$⊢ φ \to {(A R B)}^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨u, v⟩ \| (u \in A \land v \in f (u))\})$
76	5	a1i	$⊢ φ \to C = (a \in V, b \in V ⟼ (s \in 𝒫 (a \times b) ⟼ s^{-1}))$
77		xpeq12	$⊢ (a = A \land b = B) \to a \times b = A \times B$
78	77	pweqd	$⊢ (a = A \land b = B) \to 𝒫 (a \times b) = 𝒫 (A \times B)$
79	78	mpteq1d	$⊢ (a = A \land b = B) \to (s \in 𝒫 (a \times b) ⟼ s^{-1}) = (s \in 𝒫 (A \times B) ⟼ s^{-1})$
80	79	adantl	$⊢ (φ \land (a = A \land b = B)) \to (s \in 𝒫 (a \times b) ⟼ s^{-1}) = (s \in 𝒫 (A \times B) ⟼ s^{-1})$
81	2	elexd	$⊢ φ \to A \in V$
82	3	elexd	$⊢ φ \to B \in V$
83		pwexg	$⊢ A \times B \in V \to 𝒫 (A \times B) \in V$
84		mptexg	$⊢ 𝒫 (A \times B) \in V \to (s \in 𝒫 (A \times B) ⟼ s^{-1}) \in V$
85	67 83 84	3syl	$⊢ φ \to (s \in 𝒫 (A \times B) ⟼ s^{-1}) \in V$
86	76 80 81 82 85	ovmpod	$⊢ φ \to A C B = (s \in 𝒫 (A \times B) ⟼ s^{-1})$
87		cnveq	$⊢ s = \{⟨u, v⟩ \| (u \in A \land v \in f (u))\} \to s^{-1} = {\{⟨u, v⟩ \| (u \in A \land v \in f (u))\}}^{-1}$
88		cnvopab	$⊢ {\{⟨u, v⟩ \| (u \in A \land v \in f (u))\}}^{-1} = \{⟨v, u⟩ \| (u \in A \land v \in f (u))\}$
89	87 88	eqtrdi	$⊢ s = \{⟨u, v⟩ \| (u \in A \land v \in f (u))\} \to s^{-1} = \{⟨v, u⟩ \| (u \in A \land v \in f (u))\}$
90	73 75 86 89	fmptco	$⊢ φ \to (A C B) \circ {(A R B)}^{-1} = (f \in ({𝒫 B}^{A}) ⟼ \{⟨v, u⟩ \| (u \in A \land v \in f (u))\})$
91	90	coeq2d	$⊢ φ \to (B R A) \circ ((A C B) \circ {(A R B)}^{-1}) = (B R A) \circ (f \in ({𝒫 B}^{A}) ⟼ \{⟨v, u⟩ \| (u \in A \land v \in f (u))\})$
92	1 2 3	fsovd	$⊢ φ \to A O B = (f \in ({𝒫 B}^{A}) ⟼ (y \in B ⟼ \{x \in A \| y \in f (x)\}))$
93	66 91 92	3eqtr4rd	$⊢ φ \to A O B = (B R A) \circ ((A C B) \circ {(A R B)}^{-1})$

Metamath Proof Explorer

Theorem fsovrfovd

Proof