fsovcnvlem

Description: The O operator, which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-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$
	fsovfvd.g	$⊢ G = A O B$
	fsovcnvlem.h	$⊢ H = B O A$
Assertion	fsovcnvlem	$⊢ φ \to H \circ G = {I ↾}_{({𝒫 B}^{A})}$

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		fsovfvd.g	$⊢ G = A O B$
5		fsovcnvlem.h	$⊢ H = B O A$
6		ssrab2	$⊢ \{x \in A \| y \in f (x)\} \subseteq A$
7	6	a1i	$⊢ φ \to \{x \in A \| y \in f (x)\} \subseteq A$
8	2 7	sselpwd	$⊢ φ \to \{x \in A \| y \in f (x)\} \in 𝒫 A$
9	8	adantr	$⊢ (φ \land y \in B) \to \{x \in A \| y \in f (x)\} \in 𝒫 A$
10	9	fmpttd	$⊢ φ \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) : B ⟶ 𝒫 A$
11	2	pwexd	$⊢ φ \to 𝒫 A \in V$
12	11 3	elmapd	$⊢ φ \to ((y \in B ⟼ \{x \in A \| y \in f (x)\}) \in ({𝒫 A}^{B}) \leftrightarrow (y \in B ⟼ \{x \in A \| y \in f (x)\}) : B ⟶ 𝒫 A)$
13	10 12	mpbird	$⊢ φ \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) \in ({𝒫 A}^{B})$
14	13	adantr	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) \in ({𝒫 A}^{B})$
15	1 2 3	fsovd	$⊢ φ \to A O B = (f \in ({𝒫 B}^{A}) ⟼ (y \in B ⟼ \{x \in A \| y \in f (x)\}))$
16	4 15	syl5eq	$⊢ φ \to G = (f \in ({𝒫 B}^{A}) ⟼ (y \in B ⟼ \{x \in A \| y \in f (x)\}))$
17		oveq2	$⊢ a = d \to {𝒫 b}^{a} = {𝒫 b}^{d}$
18		rabeq	$⊢ a = d \to \{x \in a \| y \in f (x)\} = \{x \in d \| y \in f (x)\}$
19	18	mpteq2dv	$⊢ a = d \to (y \in b ⟼ \{x \in a \| y \in f (x)\}) = (y \in b ⟼ \{x \in d \| y \in f (x)\})$
20	17 19	mpteq12dv	$⊢ a = d \to (f \in ({𝒫 b}^{a}) ⟼ (y \in b ⟼ \{x \in a \| y \in f (x)\})) = (f \in ({𝒫 b}^{d}) ⟼ (y \in b ⟼ \{x \in d \| y \in f (x)\}))$
21		pweq	$⊢ b = c \to 𝒫 b = 𝒫 c$
22	21	oveq1d	$⊢ b = c \to {𝒫 b}^{d} = {𝒫 c}^{d}$
23		mpteq1	$⊢ b = c \to (y \in b ⟼ \{x \in d \| y \in f (x)\}) = (y \in c ⟼ \{x \in d \| y \in f (x)\})$
24	22 23	mpteq12dv	$⊢ b = c \to (f \in ({𝒫 b}^{d}) ⟼ (y \in b ⟼ \{x \in d \| y \in f (x)\})) = (f \in ({𝒫 c}^{d}) ⟼ (y \in c ⟼ \{x \in d \| y \in f (x)\}))$
25	20 24	cbvmpov	$⊢ (a \in V, b \in V ⟼ (f \in ({𝒫 b}^{a}) ⟼ (y \in b ⟼ \{x \in a \| y \in f (x)\}))) = (d \in V, c \in V ⟼ (f \in ({𝒫 c}^{d}) ⟼ (y \in c ⟼ \{x \in d \| y \in f (x)\})))$
26		eqid	$⊢ V = V$
27		fveq1	$⊢ f = g \to f (x) = g (x)$
28	27	eleq2d	$⊢ f = g \to (y \in f (x) \leftrightarrow y \in g (x))$
29	28	rabbidv	$⊢ f = g \to \{x \in d \| y \in f (x)\} = \{x \in d \| y \in g (x)\}$
30	29	mpteq2dv	$⊢ f = g \to (y \in c ⟼ \{x \in d \| y \in f (x)\}) = (y \in c ⟼ \{x \in d \| y \in g (x)\})$
31	30	cbvmptv	$⊢ (f \in ({𝒫 c}^{d}) ⟼ (y \in c ⟼ \{x \in d \| y \in f (x)\})) = (g \in ({𝒫 c}^{d}) ⟼ (y \in c ⟼ \{x \in d \| y \in g (x)\}))$
32		eleq1w	$⊢ y = u \to (y \in g (x) \leftrightarrow u \in g (x))$
33	32	rabbidv	$⊢ y = u \to \{x \in d \| y \in g (x)\} = \{x \in d \| u \in g (x)\}$
34	33	cbvmptv	$⊢ (y \in c ⟼ \{x \in d \| y \in g (x)\}) = (u \in c ⟼ \{x \in d \| u \in g (x)\})$
35		fveq2	$⊢ x = v \to g (x) = g (v)$
36	35	eleq2d	$⊢ x = v \to (u \in g (x) \leftrightarrow u \in g (v))$
37	36	cbvrabv	$⊢ \{x \in d \| u \in g (x)\} = \{v \in d \| u \in g (v)\}$
38	37	mpteq2i	$⊢ (u \in c ⟼ \{x \in d \| u \in g (x)\}) = (u \in c ⟼ \{v \in d \| u \in g (v)\})$
39	34 38	eqtri	$⊢ (y \in c ⟼ \{x \in d \| y \in g (x)\}) = (u \in c ⟼ \{v \in d \| u \in g (v)\})$
40	39	mpteq2i	$⊢ (g \in ({𝒫 c}^{d}) ⟼ (y \in c ⟼ \{x \in d \| y \in g (x)\})) = (g \in ({𝒫 c}^{d}) ⟼ (u \in c ⟼ \{v \in d \| u \in g (v)\}))$
41	31 40	eqtri	$⊢ (f \in ({𝒫 c}^{d}) ⟼ (y \in c ⟼ \{x \in d \| y \in f (x)\})) = (g \in ({𝒫 c}^{d}) ⟼ (u \in c ⟼ \{v \in d \| u \in g (v)\}))$
42	26 26 41	mpoeq123i	$⊢ (d \in V, c \in V ⟼ (f \in ({𝒫 c}^{d}) ⟼ (y \in c ⟼ \{x \in d \| y \in f (x)\}))) = (d \in V, c \in V ⟼ (g \in ({𝒫 c}^{d}) ⟼ (u \in c ⟼ \{v \in d \| u \in g (v)\})))$
43	1 25 42	3eqtri	$⊢ O = (d \in V, c \in V ⟼ (g \in ({𝒫 c}^{d}) ⟼ (u \in c ⟼ \{v \in d \| u \in g (v)\})))$
44	43 3 2	fsovd	$⊢ φ \to B O A = (g \in ({𝒫 A}^{B}) ⟼ (u \in A ⟼ \{v \in B \| u \in g (v)\}))$
45	5 44	syl5eq	$⊢ φ \to H = (g \in ({𝒫 A}^{B}) ⟼ (u \in A ⟼ \{v \in B \| u \in g (v)\}))$
46		fveq1	$⊢ g = (y \in B ⟼ \{x \in A \| y \in f (x)\}) \to g (v) = (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)$
47	46	eleq2d	$⊢ g = (y \in B ⟼ \{x \in A \| y \in f (x)\}) \to (u \in g (v) \leftrightarrow u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v))$
48	47	rabbidv	$⊢ g = (y \in B ⟼ \{x \in A \| y \in f (x)\}) \to \{v \in B \| u \in g (v)\} = \{v \in B \| u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)\}$
49	48	mpteq2dv	$⊢ g = (y \in B ⟼ \{x \in A \| y \in f (x)\}) \to (u \in A ⟼ \{v \in B \| u \in g (v)\}) = (u \in A ⟼ \{v \in B \| u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)\})$
50	14 16 45 49	fmptco	$⊢ φ \to H \circ G = (f \in ({𝒫 B}^{A}) ⟼ (u \in A ⟼ \{v \in B \| u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)\}))$
51		eqidd	$⊢ ((φ \land u \in A) \land v \in B) \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) = (y \in B ⟼ \{x \in A \| y \in f (x)\})$
52		eleq1w	$⊢ y = v \to (y \in f (x) \leftrightarrow v \in f (x))$
53	52	rabbidv	$⊢ y = v \to \{x \in A \| y \in f (x)\} = \{x \in A \| v \in f (x)\}$
54	53	adantl	$⊢ (((φ \land u \in A) \land v \in B) \land y = v) \to \{x \in A \| y \in f (x)\} = \{x \in A \| v \in f (x)\}$
55		simpr	$⊢ ((φ \land u \in A) \land v \in B) \to v \in B$
56		rabexg	$⊢ A \in V \to \{x \in A \| v \in f (x)\} \in V$
57	2 56	syl	$⊢ φ \to \{x \in A \| v \in f (x)\} \in V$
58	57	ad2antrr	$⊢ ((φ \land u \in A) \land v \in B) \to \{x \in A \| v \in f (x)\} \in V$
59	51 54 55 58	fvmptd	$⊢ ((φ \land u \in A) \land v \in B) \to (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v) = \{x \in A \| v \in f (x)\}$
60	59	eleq2d	$⊢ ((φ \land u \in A) \land v \in B) \to (u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v) \leftrightarrow u \in \{x \in A \| v \in f (x)\})$
61		fveq2	$⊢ x = u \to f (x) = f (u)$
62	61	eleq2d	$⊢ x = u \to (v \in f (x) \leftrightarrow v \in f (u))$
63	62	elrab3	$⊢ u \in A \to (u \in \{x \in A \| v \in f (x)\} \leftrightarrow v \in f (u))$
64	63	ad2antlr	$⊢ ((φ \land u \in A) \land v \in B) \to (u \in \{x \in A \| v \in f (x)\} \leftrightarrow v \in f (u))$
65	60 64	bitrd	$⊢ ((φ \land u \in A) \land v \in B) \to (u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v) \leftrightarrow v \in f (u))$
66	65	rabbidva	$⊢ (φ \land u \in A) \to \{v \in B \| u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)\} = \{v \in B \| v \in f (u)\}$
67	66	adantlr	$⊢ ((φ \land f \in ({𝒫 B}^{A})) \land u \in A) \to \{v \in B \| u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)\} = \{v \in B \| v \in f (u)\}$
68		dfin5	$⊢ B \cap f (u) = \{v \in B \| v \in f (u)\}$
69		elmapi	$⊢ f \in ({𝒫 B}^{A}) \to f : A ⟶ 𝒫 B$
70	69	ad2antlr	$⊢ ((φ \land f \in ({𝒫 B}^{A})) \land u \in A) \to f : A ⟶ 𝒫 B$
71		simpr	$⊢ ((φ \land f \in ({𝒫 B}^{A})) \land u \in A) \to u \in A$
72	70 71	ffvelrnd	$⊢ ((φ \land f \in ({𝒫 B}^{A})) \land u \in A) \to f (u) \in 𝒫 B$
73	72	elpwid	$⊢ ((φ \land f \in ({𝒫 B}^{A})) \land u \in A) \to f (u) \subseteq B$
74		sseqin2	$⊢ f (u) \subseteq B \leftrightarrow B \cap f (u) = f (u)$
75	73 74	sylib	$⊢ ((φ \land f \in ({𝒫 B}^{A})) \land u \in A) \to B \cap f (u) = f (u)$
76	68 75	syl5reqr	$⊢ ((φ \land f \in ({𝒫 B}^{A})) \land u \in A) \to f (u) = \{v \in B \| v \in f (u)\}$
77	67 76	eqtr4d	$⊢ ((φ \land f \in ({𝒫 B}^{A})) \land u \in A) \to \{v \in B \| u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)\} = f (u)$
78	77	mpteq2dva	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to (u \in A ⟼ \{v \in B \| u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)\}) = (u \in A ⟼ f (u))$
79	69	feqmptd	$⊢ f \in ({𝒫 B}^{A}) \to f = (u \in A ⟼ f (u))$
80	79	adantl	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to f = (u \in A ⟼ f (u))$
81	78 80	eqtr4d	$⊢ (φ \land f \in ({𝒫 B}^{A})) \to (u \in A ⟼ \{v \in B \| u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)\}) = f$
82	81	mpteq2dva	$⊢ φ \to (f \in ({𝒫 B}^{A}) ⟼ (u \in A ⟼ \{v \in B \| u \in (y \in B ⟼ \{x \in A \| y \in f (x)\}) (v)\})) = (f \in ({𝒫 B}^{A}) ⟼ f)$
83		mptresid	$⊢ {I ↾}_{({𝒫 B}^{A})} = (f \in ({𝒫 B}^{A}) ⟼ f)$
84	83	eqcomi	$⊢ (f \in ({𝒫 B}^{A}) ⟼ f) = {I ↾}_{({𝒫 B}^{A})}$
85	84	a1i	$⊢ φ \to (f \in ({𝒫 B}^{A}) ⟼ f) = {I ↾}_{({𝒫 B}^{A})}$
86	50 82 85	3eqtrd	$⊢ φ \to H \circ G = {I ↾}_{({𝒫 B}^{A})}$

Metamath Proof Explorer

Theorem fsovcnvlem

Proof