Metamath Proof Explorer


Theorem fsovf1od

Description: The value of ( A O B ) is a bijection, where O is the 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. (Contributed by RP, 27-Apr-2021)

Ref Expression
Hypotheses fsovd.fs O=aV,bVf𝒫baybxa|yfx
fsovd.a φAV
fsovd.b φBW
fsovfvd.g G=AOB
Assertion fsovf1od φG:𝒫BA1-1 onto𝒫AB

Proof

Step Hyp Ref Expression
1 fsovd.fs O=aV,bVf𝒫baybxa|yfx
2 fsovd.a φAV
3 fsovd.b φBW
4 fsovfvd.g G=AOB
5 1 2 3 4 fsovfd φG:𝒫BA𝒫AB
6 5 ffnd φGFn𝒫BA
7 eqid BOA=BOA
8 1 3 2 7 fsovfd φBOA:𝒫AB𝒫BA
9 8 ffnd φBOAFn𝒫AB
10 1 2 3 4 7 fsovcnvd φG-1=BOA
11 10 fneq1d φG-1Fn𝒫ABBOAFn𝒫AB
12 9 11 mpbird φG-1Fn𝒫AB
13 dff1o4 G:𝒫BA1-1 onto𝒫ABGFn𝒫BAG-1Fn𝒫AB
14 6 12 13 sylanbrc φG:𝒫BA1-1 onto𝒫AB