# Metamath Proof Explorer

## Theorem 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}=\left({a}\in \mathrm{V},{b}\in \mathrm{V}⟼\left({f}\in \left({𝒫{b}}^{{a}}\right)⟼\left({y}\in {b}⟼\left\{{x}\in {a}|{y}\in {f}\left({x}\right)\right\}\right)\right)\right)$
fsovd.a ${⊢}{\phi }\to {A}\in {V}$
fsovd.b ${⊢}{\phi }\to {B}\in {W}$
fsovfvd.g ${⊢}{G}={A}{O}{B}$
fsovcnvlem.h ${⊢}{H}={B}{O}{A}$
Assertion fsovcnvlem ${⊢}{\phi }\to {H}\circ {G}={\mathrm{I}↾}_{\left({𝒫{B}}^{{A}}\right)}$

### Proof

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